Techniken zur effizienten Verifikation von Echtzeitsystemen durch Model-Checking

Für den Entwurf sicherheitskritischer Echtzeitsysteme spielt der Korrektheitsnachweis und die Möglichkeit einen System- oder Softwareentwurf schon vor dessen Umsetzung zu prüfen eine wichtige Rolle. Für die Analyse kommen heutzutage meist Simulationen zum Einsatz. Diese liefern jedoch nur statistische Ergebnisse. Wenn also das Systemverhalten eindeutig nachzuweisen ist, sollten formale Methoden wie Model-Checking zum Einsatz kommen. Eine nachteilige Eigenschaft von Model-Checking ist das Problem der ZustandsraumExplosion, das zur Folge hat, dass sich solche Modelle für industrielle Fälle in der Regel nicht mehr berechnen lassen. In dieser Arbeit werden Modellierungstechniken und Berechnungsstrategien vorgestellt, die helfen, dieses Problem für den Model-Checker Uppaal zu lindern.      «

Für den Entwurf sicherheitskritischer Echtzeitsysteme spielt der Korrektheitsnachweis und die Möglichkeit einen System- oder Softwareentwurf schon vor dessen Umsetzung zu prüfen eine wichtige Rolle. Für die Analyse kommen heutzutage meist Simulationen zum Einsatz. Diese liefern jedoch nur statistische Ergebnisse. Wenn also das Systemverhalten eindeutig nachzuweisen ist, sollten formale Methoden wie Model-Checking zum Einsatz kommen. Eine nachteilige Eigenschaft von Model-Checking ist das Problem...     »