Industrial Applications of Probabilistic Model Checking- A Model-based Approach for Embedded Networked Systems and Concurrent Data Structures -

Wu, Hao; Katoen, Joost-Pieter (Thesis advisor); Haverkort, Boudewijn (Thesis advisor)

Aachen (2017)
Doktorarbeit

Kurzfassung

Die zunehmende Komplexität von Hard- und Softwaresystemen stellt den Entwurfsprozess solcher Systeme vor große Herausforderungen, insbesondere wenn kritische Anforderungen wie Performanz, Energieeffizienz etc. zu berücksichtigen sind. Techniken wie Leistungsbewertung und -optimierung gewinnen daher zunehmend an Bedeutung und werden routinemäßig während der Systementwicklung angewendet. Hierfür werden vorwiegend spezifische Softwarewerkzeuge zur Simulation detaillierter Prototypen eingesetzt. Solche Simulationen liefern üblicherweise Durchschnittswerte und lassen keine verlässlichen Aussagen über das optimale oder ungünstigste Systemverhalten zu.Ziel dieser Dissertation ist es nachzuweisen, dass die modellbasierte Technik des probabilistischen Model Checking zur Leistungsbewertung und -optimierung industrieller Systeme während des Entwurfsprozesseseinsetzbar ist. Als Anwendungsbereiche werden eingebettete Systeme, Rechenserver, Next Generation Mobile Networks sowie nebenläufige Datenstrukturen betrachtet.Im ersten Teil der Dissertation werden verschiedene gebräuchliche probabilistische Berechnungsmodelle wie Markow-Automaten mit und ohne Rewards eingeführt. Es wird gezeigt, wie Model Checking als Technik zurAnalyse quantitativer Eigenschaften solcher Modelle eingesetzt und wie der zugehörige Zustandsraum mithilfe von Konfluenzreduktion effizient erzeugt werden kann. Den Abschluss dieses Teils bildet eine Vorstellung zweier verwendeter Softwarewerkzeuge für probabilistisches Model Checking, welche die Systemmodellierung, die Generierung und Optimierung des Zustandsraums sowie die Analyse quantitativer Systemeigenschaften unterstützen.Im zweiten Teil der Dissertation werden fünf Fallstudien zur Anwendung probabilistischer Model-Checking-Techniken untersucht und es wird gezeigt, dass die gewonnenen Resultate aufschlussreiche Einsichten ermöglichen. Für jede Fallstudie wird zunächst erläutert, wie das untersuchte System unter Berücksichtigung probabilistischer Effekte im Detail modelliert wird und welche Leistungsmerkmale aus den untersuchten quantitativen Eigenschaften abgeleitet werden können. Zum Abschluss werden die experimentellen Ergebnisse basierend auf unseren Beobachtungen analysiert.Die erste Anwendung beschäftigt sich mit dem Problem der Synthese von energieeffizienten Software/Hardware-Abbildungen in Steuerungssystemen für Kraftfahrzeuge unter Berücksichtigung verschiedener, probabilistisch modellierter Fahrszenarien. Hierbei wird anstelle der üblichen simulationsbasierten oder analytischen Methoden eine neuartige Kombination zweier modellbasierter Techniken zur Optimierung des Energieverbrauchs angewendet. Die zweite Anwendung befasst sich mit der Leistungsbewertung eingebetteter Systeme, welche als zeitbehaftete, Szenario-abhängige Datenflusssysteme modelliert werden. Es wird gezeigt, wie sich letztere als Markow-Automaten mit Rewards darstellen lassen, welche die Untersuchung verschiedener Leistungsparameter einschließlich des Energieverbrauchs ermöglichen. Als dritte Anwendung wird die erste industrielle Fallstudie vorgestellt, in der ein neu entwickelter Ansatz zur semantischen Interpretation generalisierter stochastischer Petrinetze als Markow-Automaten zum Einsatz kommt. In der vierten Anwendung steht der Leistungsvergleich zwischen verschiedenen Scheduling-Algorithmen für LTE-Netzwerke im Vordergrund. Hierbei werden Scheduling-Optionen durch nichtdeterministische Entscheidungen im entsprechenden Automatenmodell repräsentiert. Dies erlaubt die Bestimmung von Schranken für Leistungsmaße und damit - im Gegensatz zu simulationsbasierten Techniken - die Abschätzung der Güte von Scheduling-Algorithmen. Die letzte Anwendung befasst sich mit dem Leistungsvergleich zwischen Lock-freien und Lock-basierten nebenläufigen Datenstrukturen wieStacks, Warteschlangen und Listen.Diese erfolgreichen industriellen Anwendungen demonstrieren in überzeugender Weise, dass probabilistische Model-Checking-Techniken ein elegantes und effektives modellbasiertes Framework zur Leistungsbewertung verschiedener Arten moderner IT-Systeme bereitstellen. Darüber hinaus zeigen sie, dass mithilfe von Markow-Automaten, einer variantenreichen und ausdrucksstarken Klasse probabilistischer Modelle, die Brücke zwischen mathematischer Theorie und praktischer Entwicklung geschlagen werden kann.

Identifikationsnummern