Statische und dynami... Studien- und Diploma... Statische und dynami...

Bachelorarbeit

Statische Analyse Erweiterter Endlicher Zustandsmaschinen zur Verifikation der Gültigkeit von CTL-Formeln

 

Zusammenfassung

Obwohl die Gültigkeit von CTL-Formeln für mit atomaren Aussagen annotierte erweiterte Zustandsmaschinen (sogenannte Kripke-Strukturen) im Allgemeinen nicht automatisiert entschieden werden kann, lassen sich jedoch je nach CTL-Formel-Typ Muster angeben, die statisch erkannt werden können, und deren Instanziierung in einer Kripke-Struktur hinreichende Bedingung für die Gültigkeit bzw. Nichtgültigkeit der CTL-Formel sind. Im Rahmen dieser Bachelorarbeit ist ein zweistufiges Verfahren zu entwickeln und zu implementieren, das für eine Kripke-Struktur und eine CTL-Formel als Eingabe in einer ersten Phase für eine vom Lehrstuhl zur Verfügung gestellte Menge von Mustern obiger Art alle Musterinstanzen in in der Kripke-Struktur erkennt. In einem zweiten Schritt ist die urprüngliche Kripke-Struktur zu einer neuen Kripke-Struktur zu erweitern, indem die Zustände mit allen Teilformeln der CTL-Formel annotiert werden, deren Gültigkeit/Nichtgültigket durch die erkannten Musterinstanzen gezeigt wurde. Das Verfahren ist anschließend anhand geeigneter Beispiele zu evaluieren.

Bearbeiter: Christian Regnet

Betreuer: Dipl.-Inf Marc Spisländer