Zeitbewertete Prädikat/Transitions-Netze zur Modellierung, Simulation und Analyse sicherheitskritischer Echtzeitsysteme
- Im Rahmen dieser Arbeit wurden die zeitbewerteten Prädikat/Transitions-Netze (Z-Pr/T-Netze) zur Modellierung, Simulation und Verifikation sicherheitskritischer Echtzeitsysteme entwickelt. Z-Pr/T-Netze integrieren Konzepte zur Modellierung temporärer Zusammenhänge und sind darüber hinaus mittels der Berechnung von S- und T-Invarianten sowie der Identifikation von Traps und Co-Traps strukturell analysierbar. Die Eignung von Z-Pr/T-Netzen zur Modellierung, Simulation und Verifikation komplexer Systeme aus dem Anwendungsbereich sicherheitskritischer Echtzeitsysteme wird anhand des Earliest-Deadline-First-Protokolls (EDF) und des Priority-Inheritance-Protokolls (PIP) belegt. Es erfolgt daher eine Modellierung des EDF und PIP mittels Z-Pr/T-Netzen sowie eine Verifikation für das EDF und PIP basierend auf der strukturellen Analyse der korrespondierenden Z-Pr/T-Netze. Die Anwendbarkeit struktureller Analyseverfahren zur Verifikation des EDF und PIP in Verbindung mit der nicht zu unterschätzenden Komplexität eben dieser belegen die Anwendbarkeit von Z-Pr/T-Netzen zur Modellierung, Simulation und Verifikation komplexer Systeme aus dem Anwendungsbereich sicherheitskritischer Echtzeitsysteme.
- Within this thesis time evaluated predicate/transition nets (t-pr/t-nets) have been developed for the purpose to model, simulate and verify complex real-time systems. Therefore, t-pr/t-nets integrate concepts to model timing constraints and can be analysed by the means of structural analysis such as the calculation of s- and t-invariants as well as the identification of traps and co-traps. The applicability of t-pr/t-nets to model, simulate and verify complex systems in the domain of safety-critical real-time systems is proven by the Earliest-Deadline-First-Protocol (EDF) and the Priority-Inheritance-Protocol (PIP). Therefore, the EDF and PIP are modeled by means of t-pr/t-nets. The resulting t-pr/t-nets are verified using structural analysis methods. Due to the enormous complexity and the applicability of structural analysis methods for the verification of the EDF and PIP, it can be shown that t-pr/t-nets are appropriate to model, simulate and verify complex systems in the field of safety-critical real-time systems.
Author: | Katharina Hupf |
---|---|
URN: | urn:nbn:de:hbz:kob7-4287 |
Title Additional (English): | Time Evaluated Predicate/Transition Nets to Model, Simulate and Analyse Safety Critical Real Time Systems |
Advisor: | Kurt Lautenbach |
Document Type: | Doctoral Thesis |
Language: | German |
Date of completion: | 2009/09/07 |
Date of publication: | 2009/09/07 |
Publishing institution: | Universität Koblenz, Universitätsbibliothek |
Granting institution: | Universität Koblenz, Fachbereich 4 |
Date of final exam: | 2009/06/23 |
Release Date: | 2009/09/07 |
GND Keyword: | Echtzeitsystem; Petri-Netz |
Number of pages: | xii, 136 |
Institutes: | Fachbereich 4 / Institut für Softwaretechnik |
Dewey Decimal Classification: | 0 Informatik, Informationswissenschaft, allgemeine Werke / 00 Informatik, Wissen, Systeme / 004 Datenverarbeitung; Informatik |
Licence (German): | Es gilt das deutsche Urheberrecht: § 53 UrhG |