Directed Diagnostics of System Dependability Models

Abstract

Model-Checking ist ein formales Verifikationsverfahren, in dem das Hauptziel die Überprüfung der Korrektheit von Systemen bezüglich gegebener Anforderungen ist. Daneben wird Model-Checking häufig als ein Debugging-Werkzeug eingesetzt. Es wird zur Lokalisierung und Behebung von Fehlern verwendet, wenn das Modell eine gewünschte Eigenschaft verletzt. Aus diesem Grund ist die Möglichkeit, diagnostische Informationen zu liefern, entscheidend für die praktische Anwendbarkeit von Model-Checking-Techniken. Gegenbeispiele sind ein wichtiger Vertreter für solche diagnostische Informationen. Ein Gegenbeispiel besteht in der Regel aus Informationen über das Systemverhalten, welche die Eigenschaftsverletzung belegen und bei der Bestimmung der Ursache dieser Verletzung helfen.Stochastisches Model-Checking erweitert das konventionelle Model-Checking um die Verifikation quantitativer Leistungs- und Verlässlichkeitsanforderungen. Der Kern des stochastischen Model-Checking besteht aus einer Reihe numerischer Algorithmen. Diese Algorithmen berechnen die Wahrscheinlichkeitswerte, die über die Erfüllung der zu überprüfenden Anforderungen entscheiden. Aufgrund der numerischen Natur dieser Algorithmen liefern stochastische Model-Checker keine Gegenbeispiele. Diese Dissertation präsentiert unsere Forschung zur Lösung dieses Problems. Im Rahmen dieser Forschung ist es uns als erste gelungen, stochastisches Model-Checking um die Generierung und Analyse von Gegenbeispielen zu erweitern. Wir haben das Konzept der Gegenbeispiele in das stochastische Model-Checking eingeführt und die ersten Methoden zur Generierung und Analyse von Gegenbeispielen entwickelt.Wir beginnen diese Dissertation mit einer Einführung in das stochastische Model-Checking. Danach behandeln wir das Konzept von Gegenbeispielen in diesem Zusammenhang. Wir geben eine formale Definition von Gegenbeispielen bezüglich gängiger stochastischer Modelle. Wir diskutieren anschließend die Aussagefähigkeit von Gegenbeispielen bezüglich Debugging und erläutern die Kriterien von aussagefähigen Gegenbeispielen. Danach präsentieren wir eine Reihe von neuen Methoden zur Generierung von informativen Gegenbeispielen. Unsere Methoden basieren auf heuristischen, oder auch gerichteten, Suchalgorithmen. Wir untersuchen diese Methoden unter verschiedenen Bedingungen und betrachten deren Vor- und Nachteile. Wir untersuchen deren Anwendbarkeit in der Praxis für Modelle mit hoher Komplexität. Wir demonstrieren die Effizienz und Skalierbarkeit unserer Methoden anhand von ausführlichen Experimenten mit realistischen Fallstudien. Diese Experimente zeigen auch, dass die erzeugten Gegenbeispiele informativ und nützlich bei der Fehlerbehebung sind.Wie wir in dieser Dissertation zeigen werden, sind Gegenbeispiele im stochastischen Model-Checking in der Regel sehr komplex. Infolgedessen stellt die Analyse solcher Gegenbeispiele zu Debugging-Zwecken eine große Herausforderung für die Benutzer dar. Wir haben eine Methode zur Unterstützung des Benutzers bei der Analyse von Gegenbeispielen entwickelt. Diese Methode setzt interaktive Visualisierungstechniken ein, um kausale Faktoren, die die Eigenschaftsverletzung verursacht haben, zu bestimmen.Ein wichtiger Beitrag unserer Forschung ist die Entwicklung eines neuen gerichteten Suchalgorithmus K* zur Lösung des Problems der k-kürzesten-Pfade. Das Problem der k-kürzesten-Pfade ist ein allgemeines Problem mit vielen Anwendungsgebieten. Dabei handelt es sich um das Finden der k kürzesten Pfade von einem Start- zu einem Zielknoten in einem gerichteten Graphen, wobei k eine beliebige natürliche Zahl ist. Im Gegensatz zu existierenden Algorithmen ist K* auch auf sehr große und komplexe Graphen effizient anwendbar. Wir demonstrieren die Überlegenheit von K mit Hilfe von Experimenten im Bereich der Routenplanung im Straßennetz der USA.