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

Wu, Hao; Haverkort, Boudewijn; Katoen, Joost-Pieter

doi:36578

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

Wu, Hao

2017

Verantwortlichkeitsangabevorgelegt von Dipl.-Inform. Hao Wu

ImpressumAachen 2017

Umfang1 Online-Ressource (xvi, 174 Seiten) : Illustrationen, Diagramme

Dissertation, RWTH Aachen University, 2017

Veröffentlicht auf dem Publikationsserver der RWTH Aachen University

Genehmigende Fakultät
Fak01

Hauptberichter/Gutachter
Katoen, Joost-Pieter (Thesis advisor) ; Haverkort, Boudewijn (Thesis advisor)

Tag der mündlichen Prüfung/Habilitation
2017-07-04

Online
DOI: 10.18154/RWTH-2017-08297
URL: http://publications.rwth-aachen.de/record/699523/files/699523.pdf
URL: http://publications.rwth-aachen.de/record/699523/files/699523.pdf?subformat=pdfa

Einrichtungen

Inhaltliche Beschreibung (Schlagwörter)
Markov (Reward) Automata (frei) ; industrial applications (frei) ; probabilistic model checking (frei)

Thematische Einordnung (Klassifikation)
DDC: 004

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.

Nowadays, due to the rapid growth of complexity of hardware/software systems, designing such systems to meet critical requirements (e.g., performance, energy efficiency) becomes an increasingly challenging work. Performance evaluation and optimization becomes a mandatory routine in the system design. This is usually done based on running simulations of very detailed prototypes using specific simulation tools. However the results obtained by simulation usually lack the information of performance bounds caused by the best and worst-case scenarios. In this dissertation, we demonstrate industrial applications of probabilistic model checking -a model-based approach- to evaluate and optimize the performance of systems during design phase. Our applications cover systems from several, currently popular fields: embedded systems, computing servers, the next generation mobile networks and concurrent data structures. %We utilize the probabilistic model called Markov reward automata (MRA), which is capable of modeling and analyzing large systems. On the one hand, it is 1) compositional, 2) allows to be reduced effectively by confluence reduction --a novel on-the-fly reduction technique akin to partial order reduction--, and 3) can be efficiently analyzed. On the other hand, MRA have a rich expressiveness: the transitions equipped with either discrete probability distributions or the exponentially timed delays allow to describe the discrete and continuous stochastic phenomena in system behavior, which are crucial in today's systems due to various sources of uncertainty; the non-determinism allows to model conflicting activities (e.g., scheduling strategies) or underspecification due to unknown or unpredictable environment. Moreover, it also allows rewards to be attached to the states and transitions. Various performance metrics such as average energy consumption, and average throughput of the system can be derived from the quantitative analysis based on MRA. In the first part of the dissertation, we briefly give an overview of several common probabilistic models including Markov automata (MA) and Markov reward automata (MRA). We explain how to model check the quantitive properties on M(R)A and how the reduced state space can be directly generated on-the-fly by confluence reduction. In the end, we give a short introduction to two relevant probabilistic model checking tools we used throughout our applications, which support modeling, state space generation/optimization (e.g., confluence reduction for M(R)A), and analysis based on the probabilistic models. In the second part of the dissertation, we provide five applications of probabilistic model checking and show how the obtained results give us an informative insight of the system design. In each application, we begin with explaining how we model the system to be evaluated in detail and which performance metrics of interest can be derived from the quantitative properties based on probabilistic models. In the end, we analyze the obtained results from probabilistic model checking based on our observations. The first application focuses on a synthesis problem from software to hardware in automotive control systems to optimize the overall energy consumption using the information of driving scenarios as a probabilistic model. We provide a novel combination of two model-based approaches to optimize the energy consumption of automotive control systems rather than using simulation or analytical techniques. The second application considers performance evaluation of embedded systems, which are initially modeled by exponentially timed scenario-aware dataflow (eSADF). We give a formal definition of eSADF and hardware platform in terms of MRAs and various useful performance metrics including energy consumption are derived based on the resulting MRA. In the third application, we provide a first industrial case study to evaluate the performance of computing servers using the recent generalized stochastic Petri nets (GSPNs)-to-Markov automata semantics. In the fourth application, we compare the performance between different scheduling algorithms in long term evolution (LTE) networks through probabilistic model checking. The non-determinism allowed in MRA, which is used to model the decision alternatives (e.g, scheduling possibilities), yields bounds on performance metrics. These bounds provide us useful information about how far is a given scheduling algorithm away from the optimal one (w.r.t. a certain performance metric), which cannot be obtained by using simulation. The last application focuses on the performance comparison between lock-free and lock-based concurrent data structures of various types including stacks, queues, and lists. From these successful industrial applications in the dissertation, we conclude that probabilistic model checking is an effective model-based approach to evaluate the performance of various types of modern systems and provides a uniform and elegant framework from modeling to performance evaluation. Moreover, Markov (reward) automata, which is a rich expressive probabilistic model that can be efficiently analyzed, bridge the gap between an elegant theory and practical engineering needs.

OpenAccess:
PDF PDF (PDFA)
(additional files)