SMC und zeitlich begrenzte Erreichbarkeitsanalyse für HPnGs

Abstract

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.