On the analysis of stochastic timed systems

Abstract

The formal methods approach to develop reliable and efficient safety- or performance-critical systems is to construct mathematically precise models of such systems on which properties of interest, such as safety guarantees or performance requirements, can be verified automatically. In this thesis, we present techniques that extend the reach of exhaustive and statistical model checking to verify reachability and reward-based properties of compositional behavioural models that support quantitative aspects such as real time and randomised decisions. We present two techniques that allow sound statistical model checking for the nondeterministic-randomised model of Markov decision processes. We investigate the relationship between two different definitions of the model of probabilistic timed automata, as well as potential ways to apply statistical model checking. Stochastic timed automata allow nondeterministic choices as well as nondeterministic and stochastic delays, and we present the first exhaustive model checking algorithm that allows their analysis. All the approaches introduced in this thesis are implemented as part of the Modest Toolset, which supports the construction and verification of models specified in the formal modelling language Modest. We conclude by applying this language and toolset to study novel distributed control strategies for photovoltaic microgenerators.

Formale Methoden erlauben die Entwicklung verlässlicher und performanter sicherheits- oder zeitkritischer Systeme, indem auf mathematisch präzisen Modellen relevante Eigenschaften wie Sicherheits- oder Performance-Garantien automatisch verifiziert werden. In dieser Dissertation stellen wir Methoden vor, mit denen die Anwendbarkeit der klassischen und statistischen Modellprüfung (model checking) zur Verifikation von Erreichbarkeits- und Nutzenseigenschaften auf kompositionellen Verhaltensmodellen, die quantitative Aspekte wie zufallsbasierte Entscheidungen und Echtzeitverhalten enthalten, erweitert wird. Wir zeigen zwei Methoden auf, die eine korrekte statistische Modellprüfung von Markov-Entscheidungsprozessen erlauben. Wir untersuchen den Zusammenhang zwischen zwei Definitionen des Modells des probabilistischen Zeitautomaten sowie mögliche Wege, die statistische Modellprüfung auf diese Art Modelle anzuwenden. Stochastische Zeitautomaten erlauben nichtdeterministische Entscheidungen sowie nichtdeterministische und stochastische Wartezeiten; wir stellen den ersten Algorithmus für die klassische Modellprüfung dieser Automaten vor. Alle Techniken, die wir in dieser Dissertation behandeln, sind als Teil des Modest Toolsets, welches die Erstellung und Verifikation von Modellen mittels der formalen Modellierungssprache Modest erlaubt, implementiert. Wir verwenden diese Sprache und Tools, um neuartige verteilte Steuerungsalgorithmen für Photovoltaikanlagen zu untersuchen.