[Back]

A. Plaickner:
"Symbolic Model Checking using NUSMV";
Supervisor: H. Veith; Institut für Informationssysteme, 2003.

Model Checking ist eine Methode zur formalen Verifikation von Systemen mit entlich vielen Zuständen. Ein Model Checking Algorithmus prüft, ob gewünschte Eigenschaften in einem System erfüllt sind. In Symbolic Model Checking wird das System symbolisch als binäres Entscheidungsdiagramm repräsentiert. Der Vorteil dieses Ansatzes ist, dass komplexere Systeme verifiziert werden können. NUSMV ist ein Model Checker, der die Symbolic Model Checking Algorithmen implementiert. Diese Arbeit beschreibt den NUSMV Model Checker. Es wird beschrieben, wie Systeme und Eigenschaften in NUSMV ausgedrückt werden können und welche Möglichkeiten der interaktion mit NUSMV es gibt. Der Hauptbeitrag dieser Arbeit besteht in einer Beschreibung, wei eine BDD Repräsentation eines Systems generiert wird. Weiters zeigen wir, wie die Symbolic Model Checking Algorithmen in NUSMV implementiert sind.