- Symbolic Model Verifier
-
Der SMV (Symbolic Model Verifier) ist ein Werkzeug zur Modellprüfung (engl. Model Checking). Dieser Model Checker prüft endliche Zustandsautomaten (engl. Finite State Machines) mit der temporalen Logik CTL.
Inhaltsverzeichnis
Technologie
Die Eingabesprache erlaubt es, einen Automaten synchron, asynchron, detailliert oder abstrakt zu beschreiben. In der Sprache gibt es nur finite Datentypen, also boolesche Variablen, skalare Variablen und feste Arrays. Statische, strukturierte Datentypen können jedoch erstellt werden.
CTL unterstützt die präzise Definition von zeitlichen Eigenschaften wie Safety, Lebendigkeit, Fairness oder Deadlock-Freiheit. Um die Modelle zu prüfen verwendet SMV einen symbolischen Algorithmus, der auf geordneten binären Entscheidungsdiagrammen (OBDD) basiert.
Eingabedatei
Die Eingabedatei enthält die Beschreibung des Zustandsautomaten und die Anforderungsspezifikation in der Eingabesprache von SMV.
Darstellung von Zuständen
Die Zustände werden durch Enumerationen dargestellt. Das Verhalten kann nicht-deterministisch spezifiziert werden. Nicht initialisierte Variablen entsprechen (externen) Ereignissen. Sie können während des Model-Checkings geprüft werden. Mit SMV kann das Systemmodell in mehrere Module aufgeteilt werden. Diese Module dienen der besseren Verständlichkeit und dem Modellieren von Interaktionen zwischen Systemkomponenten.
Interaktionen zwischen Systemkomponenten
Die Interaktion zwischen den Systemkomponenten kann synchron oder asynchron erfolgen. Synchron bedeutet beispielsweise, dass alle Module nebenläufig an einem Takt orientiert sind. Bei einer asynchronen Ausführung haben die Prozesse unterschiedliche Ausführungszeiten.
Bei der Verifikation kann Fairness erzwungen werden, indem die Prüfung sich auf bestimmte Ausführungspfade beschränken lässt, längs derer eine Formel unendlich oft wahr ist. Somit kann ein fairer Zugriff auf Betriebsmittel erzwungen werden. Keinem der Prozesse wird ein Betriebsmittel für immer entzogen.
Aktuelle Version
Das letzte Release von SMV ist Version 2.5 für Windows NT aus dem Jahre 1998. Der Model Checker läuft auf SunOS 5, Solaris, Linux, Ultrix.
NuSMV
NuSMV wurde in einem Gemeinschaftsprojekt vom ITC-IRST (Istituto Trentino di Cultura, Istituto per la Ricerca Scientifica e Tecnologica in Trient), der Carnegie Mellon University, der Universität Genua und der Universität Trient als aktualisierte Version von SMV entwickelt. Es handelt sich dabei um eine Neuimplementierung und Erweiterung von SMV. So unterstützt NuSMV Model Checking mittels eines SAT solvers. Es wurde als offene Architektur entworfen und findet rege Verwendung in anderen Projekten.
NuSMV-2 ist als quelloffene Software unter der LGPL veröffentlicht worden.
Die neueste Version von NuSMV (2.4.3) wurde am 22. Mai 2007 angekündigt[1]. NuSMV-2 kann unter den meisten gängigen Betriebssystemen, die den POSIX-Standard unterstützen, kompiliert werden. Auf der Homepage wird auch ein Windows-Installer angeboten.
Links
Literatur
- Béatrice Bérard, Michel Bidoit, Alain Finkel: Systems and Software Verification: Model-Checking Techniques and Tools. Springer, 2001, ISBN 3-540-41523-8
Wikimedia Foundation.
