Symbolic Semantics and Verification of Stochastic Process Algebras

Symbolische Semantik und Verifikation stochastischer Prozessalgebren

Please always quote using this URN: urn:nbn:de:bvb:29-opus-3329
  • In the realm of performance and reliability analysis, high-level specification languages like stochastic process algebras (SPA) or generalised stochastic Petri nets (GSPN) have turned out to be extremely useful. During the analysis of systems, being specified with either of the two methods, two main problems can be identified: - State space explosion: This problem occurs on generation and storage of the semantic models of complex systems on which analysis is carried out. This semantic model is normally some kind of a continuous time Markov chain (CTMC) or stochastic labelled transition system (SLTS). - The specification and automatic verification of complex system requirements This thesisIn the realm of performance and reliability analysis, high-level specification languages like stochastic process algebras (SPA) or generalised stochastic Petri nets (GSPN) have turned out to be extremely useful. During the analysis of systems, being specified with either of the two methods, two main problems can be identified: - State space explosion: This problem occurs on generation and storage of the semantic models of complex systems on which analysis is carried out. This semantic model is normally some kind of a continuous time Markov chain (CTMC) or stochastic labelled transition system (SLTS). - The specification and automatic verification of complex system requirements This thesis contributes to the alleviation of the state space explosion problem by devising a new denotational semantics for stochastic process algebras that relies on efficient data structures for the compact representation of even huge state spaces. The second problem is addressed by devising a new stochastic temporal logic and corresponding verification algorithms, that allow the sepcification and verification of complex system requirements.show moreshow less
  • Im Bereich der Leistungs- und Zuverlässigkeitsanalyse haben sich abstrakte Spezifikationssprachen wie stochastische Prozessalgebren (SPA) oder verallgemeinerte stochastische Petrinetze (engl. generalised stochastic Petri nets, GSPN) als sehr hilfreich erwiesen. Sollen Spezifikationen, die mit solchen Sprachen erzeugt wurden, analysiert werden, können zwei Hauptprobleme identifiziert werden: - Zustandsraumexplosion: Dieses Problem entsteht bei der Erzeugung und Abspeicherung der semantischen Modelle komplexer Systeme, auf deren Basis die Analyse der Spezifikation stattfinden soll. Die semantischen Modelle sind eine Art zeitkontinuierlicher Markovkette (engl. continuous-time Markov chains,Im Bereich der Leistungs- und Zuverlässigkeitsanalyse haben sich abstrakte Spezifikationssprachen wie stochastische Prozessalgebren (SPA) oder verallgemeinerte stochastische Petrinetze (engl. generalised stochastic Petri nets, GSPN) als sehr hilfreich erwiesen. Sollen Spezifikationen, die mit solchen Sprachen erzeugt wurden, analysiert werden, können zwei Hauptprobleme identifiziert werden: - Zustandsraumexplosion: Dieses Problem entsteht bei der Erzeugung und Abspeicherung der semantischen Modelle komplexer Systeme, auf deren Basis die Analyse der Spezifikation stattfinden soll. Die semantischen Modelle sind eine Art zeitkontinuierlicher Markovkette (engl. continuous-time Markov chains, CTMC) oder eines stochastischen beschrifteten Transitionssystems (engl. stochstastic labelled transitions systems, SLTS). - Die Spezifikation und automatische Überprüfung komplexer Systemeigenschaften Diese Arbeit trägt zur Lösung des Zustandsraumexplosionsproblem durch die Definition einer neuen denotationellen Semantik für stochastische Prozess- algebren bei. Diese Semantik beruht auf effizienten Datenstrukturen, die die kompakte Speicherung von sehr großen Zustandsräumen erlaubt.show moreshow less

Download full text files

Export metadata

Additional Services

Share in Twitter Search Google Scholar Statistics
Metadaten
Author:Georg Wolfgang Matthias Kuntz
URN:urn:nbn:de:bvb:29-opus-3329
Advisor:Markus Siegle
Document Type:Doctoral Thesis
Language:English
Year of Completion:2006
Publishing Institution:Friedrich-Alexander-Universität Erlangen-Nürnberg (FAU)
Granting Institution:Friedrich-Alexander-Universität Erlangen-Nürnberg (FAU), Technische Fakultät
Date of final exam:2006/02/02
Release Date:2006/03/10
Tag:Binary Decision Diagram; Formal Semantics; Model Checking; Performance Evaluation; Process Algebra
SWD-Keyword:Binäres Entscheidungsdiagramm; Model checking; Temporale Logik; Prozessalgebra; Datenverarbeitungssystem / Leistungsbewertung; Formale Semantik
Institutes:Technische Fakultät / Technische Fakultät -ohne weitere Spezifikation-
Dewey Decimal Classification:0 Informatik, Informationswissenschaft, allgemeine Werke / 00 Informatik, Wissen, Systeme / 004 Datenverarbeitung; Informatik
open_access (DINI-Set):open_access