Konferenzbeitrag
SMC und zeitlich begrenzte Erreichbarkeitsanalyse für HPnGs
Vorschaubild nicht verfügbar
Volltext URI
Dokumententyp
Text/Conference Paper
Zusatzinformation
Datum
2022
Autor:innen
Zeitschriftentitel
ISSN der Zeitschrift
Bandtitel
Quelle
Verlag
Köllen Druck + Verlag GmbH
Zusammenfassung
Sicherheitskritische Systeme stellen einen wichtigen Teil des heutigen Lebens dar. Modellierung und formale Verifikation bieten Ansätze zur Analyse solcher Systeme im Hinblick auf Systemeigenschaften wie beispielsweise Zuverlässigkeit. In meiner Dissertation [Pi21] wird eine Unterklasse stochastischer hybrider Systeme betrachtet, die diskrete, kontinuierliche und stochastische Variablen kombiniert. Es werden neuartige Ansätze für die Evaluation von hybriden Petri-Netzen mit allgemeinen Transitionen (HPnGs) vorgestellt. Diese umfassen statistisches Model Checking für Modelle mit linearen und nichtlinearen kontinuierlichen Verläufen sowie die (zeitlich begrenzte) Erreichbarkeitsanalyse für nichtdeterministische Modelle. Darüber hinaus stellt die Dissertation einen Ansatz für eine Transformation von HPnGs in eine Unterklasse der stochastischen hybriden Automaten vor, die die Anwendung bestehender, für hybride Automaten entwickelter Methoden auf stochastische hybride Modelle ermöglicht. Der resultierende Fehler der vorgestellten Ansätze kann dabei genau charakterisiert werden.