Ermittlung des Testa... Examensarbeiten Schutzzielanalyse an...

Diplomarbeit

Bewertung und Vergleich von Verfahren zur Analyse der Aussagekraft von Model-Checking-Nachweisen

 

Zusammenfassung

Model-Checking ist eine nützliche Verifikationsmethode, die inzwischen auch in der industriellen Praxis Verbreitung gefunden hat. Dies liegt nicht zuletzt daran, dass es mit Model-Checking möglich ist zu überprüfen, ob eine bestimmte Eigenschaft in einem Modell unter allen möglichen Eingaben erfüllt ist. Für diese Überprüfung wird eine Reihe von zu überprüfenden Eigenschaften formuliert und diese Eigenschaften werden dann einzeln durch den Model-Checker überprüft. Bei der praktischen Anwendung des Model-Checking hat sich aber gezeigt, dass die Qualität der Ergebnisse des Model-Checkers stark von der Qualität der spezifizierten Eigenschaften abhängt. Um möglichst aussagekräftige Ergebnisse zu erhalten, wurden deshalb verschiedene Verfahren entwickelt, die dazu dienen, die Qualität der spezifizierten Eigenschaften zu beurteilen und es dem Benutzer so erlauben, seine Spezifikationsformeln zu verbessern. Diese Ansätze sind die Entdeckung von trivialer Erfüllung, die Generierung eines interessanten Zeugen und die Berechnung der Überdeckung. Bei der Entdeckung von trivialer Erfüllung wird die Qualität einer einzelnen Spezifikationsformel bewertet, indem untersucht wird, ob alle Teile der Formel einen Einfluss auf das Ergebnis des Model-Checkers haben. Die Generierung eines interessanten Zeugen erstellt ein Beispiel einer interessanten Ausführung des modellierten Systems und gibt dieses Beispiel an den Benutzer weiter, damit dieser überprüfen kann, wie sich sein System verhält. Bei der Berechnung von Überdeckung wird dagegen die Gesamtheit aller formulierten Eigenschaften daraufhin untersucht, ob es mit ihnen möglich ist, alle Teile des Modells zu überprüfen. Inzwischen gibt es für jedes dieser Verfahren verschiedene Algorithmen, die sich aber in ihrer Anwendbarkeit und in ihrer Aussagekraft stark unterscheiden. In dieser Arbeit werden die wichtigsten dieser Verfahren und Algorithmen vorgestellt und bewertet und es wird ein Vergleich der Verfahren durchgeführt. Anschließend wird ein selbstentwickeltes Tool vorgestellt, welches es basierend auf dem Model-Checker NuSMV erlaubt, einige der vorgestellten Verfahren dazu zu verwenden, das Ergebnis eines Model- Checking-Durchlaufs realistischer zu beurteilen.

Bearbeiter: Claudia Schieber

Betreuer: Dipl.-Inf. Johannes Drexler