The probabilistic model checker Storm : symbolic methods for probabilistic model checking

Hensel, Hans Christian; Parker, David; Katoen, Joost-Pieter

doi:HT019926716

The probabilistic model checker Storm : symbolic methods for probabilistic model checking = Der Probabilistische Model Checker Storm - Symbolische Methoden für Probabilistisches Model Checking

Hensel, Hans Christian^RWTH*

2018 & 2019

VerantwortlichkeitsangabeChristian Hensel

ImpressumAachen : RWTH Aachen University, Department of Computer Science 2018

Umfang1 Online-Ressource (vii, 331 Seiten) : Illustrationen

ReiheAachener Informatik-Berichte ; 2018-06

Dissertation, RWTH Aachen University, 2018

Veröffentlicht auf dem Publikationsserver der RWTH Aachen 2019

Genehmigende Fakultät
Fak01

Hauptberichter/Gutachter
Katoen, Joost-Pieter (Thesis advisor)^RWTH* ; Parker, David (Thesis advisor)

Tag der mündlichen Prüfung/Habilitation
2018-12-03

Online
DOI: 10.18154/RWTH-2018-231803
URL: http://publications.rwth-aachen.de/record/752011/files/%20752011.pdf

Einrichtungen

Inhaltliche Beschreibung (Schlagwörter)
Markov Models (frei) ; Model Checking (frei) ; Probabilistic Analysis (frei) ; Storm (frei) ; Symbolic Methods (frei)

Thematische Einordnung (Klassifikation)
DDC: 004

Kurzfassung
In einer Welt, in der wir zusehends von sicherheitskritischen Systemen abhängen, die zeitgleich immer komplexer werden, bieten formale Methoden eine Möglichkeit, die Korrektheit von Systemen mathematisch rigoros zu beweisen. Model Checking ist eine vollautomatisierte Technik, die bereits erfolgreich zur Verifikation von Soft- und Hardware eingesetzt wird. Interessante Systeme weisen oft stochastisches Verhalten auf, beispielsweise wenn Komponenten potentiell ausfallen oder Randomisierung als Schlüssel zur Effizienzsteigerung benutzt wird. Probabilistisches Model Checking erweitert das traditionelle (qualitative) Model Checking um die Analyse solcher Systeme. Da Model Checking vereinfacht als vollständige Untersuchung des Zustandsraums des betreffenden Modells betrachtet werden kann, leidet es am Fluch der Dimensionalität: Zustandsräume wachsen exponentiell in der Anzahl der Komponenten und Variablen und werden schnell zu groß für eine Analyse - ein Problem, das auch Zustandsraumexplosion genannt wird. Symbolische Methoden haben entscheidend dazu beigetragen, diesen Effekt abzuschwächen. Anstatt Zustände und Übergänge des Systems separat zu betrachten, versuchen sie, die Struktur des Modells auszunutzen und Mengen von Zuständen und Transitionen gleichzeitig zu behandeln. Im Bereich des traditionellen Model Checking dominieren Werkzeuge, die auf symbolischen Methoden basieren. Im probabilistischen Kontext zeigen symbolische Methoden ebenfalls Potential, sind aber in der Regel nicht auf Augenhöhe mit ihren qualitativen Gegenstücken. Diese Arbeit beschäftigt sich mit Fortschritten auf dem Gebiet der symbolischen Methoden im probabilistischen Model Checking. Die fünf wesentlichen Beiträge sind die Folgenden: (1) Wir schlagen die JANI-Modellierungssprache vor, um die Vielzahl verschiedener Eingabesprachen von probabilistischen Model Checkern zu vereinheitlichen. Sie deckt eine große Bandbreite von Modellen ab, die Randomisierung oder Zeitaspekte beinhalten, und bietet wohldefinierte Stellen für zukünftige Erweiterungen. (2) Wir zeigen, wie Gegenbeispiele auf der Ebene von JANI-Spezifikationen synthetisiert werden können. Dazu kombinieren wir gewöhnliches probabilistisches Model Checking mit einer geschickten Aufzählung der Lösungen eines Erfüllbarkeitsproblems. (3) Wir vereinen die Stärken von Entscheidungsdiagrammen zur Darstellung von riesigen Systemen und Bisimulationsminimierung, die Zustandsräume durch die Faktorisierung von Symmetrien reduziert. Unsere Experimente zeigen, dass Modelle, die Wahrscheinlichkeiten, kontinuierliche Zeit und Kosten umfassen, drastisch verkleinert werden können. (4) Wir resümieren, erweitern und implementieren ein Framework zur spielbasierten Abstraktion, das unendliche probabilistische Automaten behandeln kann. Im Gegensatz zu anderen Implementierungen ist unsere öffentlich verfügbar und berechnet korrekte Schranken durch die Benutzung rationaler Arithmetik. (5) Wir präsentieren Storm, einen neuen, hochperformanten probabilistischen Model Checker, der zahlreiche Funktionen bietet, die über die gewöhnlichen Verifikationsaufgaben hinausgehen, und insbesondere (1) bis (4) vereint. Wir zeigen, dass Storm viele Instanzen der PRISM-Benchmarksammlung schneller löst als konkurrierende Werkzeuge.

In a world in which we increasingly rely on safety critical systems that simultaneously are becoming ever more complex, formal methods provide a means to mathematically rigorously prove systems correct. Model checking is a fully automated technique that is successfully applied in the verification of software and hardware circuits. However, in practice many systems exhibit stochastic behavior, for instance when components may fail or randomization is used as a key element to improve efficiency. Probabilistic model checking extends traditional (qualitative) model checking to deal with such systems. As model checking can be (simplistically) viewed as an exhaustive exploration of the state space of the model under consideration, it suffers from the curse of dimensionality: State spaces grow exponentially in the number of components and variables and they quickly become too large to be effectively manageable, a problem that is typically referred to as state space explosion. Symbolic methods have helped to alleviate this problem substantially. Rather than considering states and transitions of the system individually, they instead exploit structure in the model and treat sets of states and transitions simultaneously. Model checkers based on symbolic techniques dominate the landscape of hardware and software model checking. In the probabilistic setting, symbolic methods too show potential but are arguably not on par with their qualitative counterparts. This thesis is concerned with advances in the field of symbolic techniques in the context of probabilistic model checking. The major contributions are fivefold: (1) We propose the JANI modeling language to unify the multitude of input languages of probabilistic model checkers. It covers a large range of models involving randomization and timing aspects and offers well-defined points for future extensions. (2) We show how counterexamples on the level of JANI specifications can be synthesized. For this, we develop a method based on the connection of standard probabilistic model checking and a smart enumeration of the solutions of a satisfiability problem. (3) We combine the strengths of decision diagrams for the representation of gigantic systems and bisimulation minimization, a technique that reduces systems by factoring out symmetry. Our implementation is shown to drastically reduce the sizes of models involving probabilities, continuous time, nondeterminism and rewards. (4) We summarize, extend and implement a game-based abstraction-refinement framework that is able to treat infinite-state probabilistic automata. In contrast to other implementations, ours is openly available and computes strictly sound bounds through the use of rational arithmetic. (5) We present Storm, a new high-performance probabilistic model checker. It goes beyond the standard verification tasks through numerous features and in particular integrates the items (1) to (4) above. We show that it outperforms other state-of-the-art model checkers on the majority of instances of the PRISM benchmark suite.

OpenAccess:
PDF
(additional files)