Please use this identifier to cite or link to this item: doi:10.22028/D291-26597
Title: On the analysis of stochastic timed systems
Authors: Hartmanns, Arnd
Language: English
Issue Date: 2015
SWD key words: Verifikation
Model Checking
Zeitbehafteter Automat
Markov-Entscheidungsprozess
Markov-Kette
Stochastischer Automat
Verteiltes System
Free key words: verification
model checking
Markov decision process
stochastic timed automaton
simulation
DDC groups: 004 Computer science, internet
Publikation type: Doctoral Thesis
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.
URI: urn:nbn:de:bsz:291-scidok-60545
hdl:20.500.11880/26653
http://dx.doi.org/10.22028/D291-26597
Advisor: Hermanns, Holger
Date of oral examination: 4-Feb-2015
Date issued: 31-Mar-2015
Faculty: MI - Fakultät für Mathematik und Informatik
Institute: MI - Informatik
Appears in Collections:SciDok - Der Wissenschaftsserver der Universität des Saarlandes

Files in This Item:
File Description SizeFormat 
Thesis_Final_Electronic.pdf11,07 MBAdobe PDFView/Open


Items in SciDok are protected by copyright, with all rights reserved, unless otherwise indicated.