Homepage der Universität des Saarlandes
universaar Bücher Online
 

Bibliographische Angaben zum Volltext

Hinweis zum Urheberrecht

Buch (Monographie) zugänglich unter
URN: urn:nbn:de:bsz:291-universaar-1389
URL: http://universaar.uni-saarland.de/monographien/volltexte/2015/138/


On the analysis of stochastic timed systems

Hartmanns, Arnd

pdf-Format:
Dokument 1.pdf (4.133 KB)

Bookmark bei Connotea Bookmark bei del.icio.us
SWD-Schlagwörter: Verifikation , Model Checking , Zeitbehafteter Automat , Markov-Entscheidungsprozess , Markov-Kette , Stochastischer Automat , Verteiltes System
Institut: Fachrichtung 6.2 - Informatik
DDC-Sachgruppe: Informatik
Dokumentart: Buch (Monographie)
ISBN: 978-3-86223-182-9
Sprache: Englisch
Erstellungsjahr: 2015
Publikationsdatum: 24.07.2015
Bemerkung: Druckausgabe erhältlich über Monsenstein & Vannerdat
Kurzfassung auf Englisch: 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.