Bitte benutzen Sie diese Referenz, um auf diese Ressource zu verweisen: doi:10.22028/D291-26597
Titel: On the analysis of stochastic timed systems
Verfasser: Hartmanns, Arnd
Sprache: Englisch
Erscheinungsjahr: 2015
SWD-Schlagwörter: Verifikation
Model Checking
Zeitbehafteter Automat
Markov-Entscheidungsprozess
Markov-Kette
Stochastischer Automat
Verteiltes System
Freie Schlagwörter: verification
model checking
Markov decision process
stochastic timed automaton
simulation
DDC-Sachgruppe: 004 Informatik
Dokumentart : Dissertation
Kurzfassung: 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.
Link zu diesem Datensatz: urn:nbn:de:bsz:291-scidok-60545
hdl:20.500.11880/26653
http://dx.doi.org/10.22028/D291-26597
Erstgutachter: Hermanns, Holger
Tag der mündlichen Prüfung: 4-Feb-2015
SciDok-Publikation: 31-Mär-2015
Fakultät: Fakultät 6 - Naturwissenschaftlich-Technische Fakultät I
Fachrichtung: MI - Informatik
Fakultät / Institution:MI - Fakultät für Mathematik und Informatik

Dateien zu dieser Ressource:
Datei Beschreibung GrößeFormat 
Thesis_Final_Electronic.pdf11,07 MBAdobe PDFÖffnen/Anzeigen


Alle Ressourcen in diesem Repository sind urheberrechtlich geschützt.