Symbolic Model Verifier
Der Symbolic Model Verifier (SMV) ist ein Werkzeug zur Modellprüfung (englisch Model Checking). Dieser Model Checker prüft endliche Zustandsautomaten (engl. finite state machines) mit der temporalen Logik CTL. SMV wurde von Kenneth L. McMillan im Rahmen seiner Doktorarbeit[1] an der Carnegie Mellon University entwickelt.
Technologie[Bearbeiten | Quelltext bearbeiten]
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[Bearbeiten | Quelltext bearbeiten]
Die Eingabedatei enthält die Beschreibung des Zustandsautomaten und die Anforderungsspezifikation in der Eingabesprache von SMV.
Darstellung von Zuständen[Bearbeiten | Quelltext bearbeiten]
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[Bearbeiten | Quelltext bearbeiten]
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[Bearbeiten | Quelltext bearbeiten]
Das letzte Release von SMV ist Version 2.5 für Windows NT aus dem Jahr 1998. Der Model Checker läuft auf SunOS 5, Solaris, Linux, Ultrix.
NuSMV[Bearbeiten | Quelltext bearbeiten]
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 ist Version 2.6.0[2] NuSMV-2 kann unter den meisten gängigen Betriebssystemen, die den POSIX-Standard unterstützen, kompiliert werden. Auf der Website wird auch ein Windows-Installer angeboten.
Literatur[Bearbeiten | Quelltext bearbeiten]
- Kenneth Mc Millan: Symbolic Model Checking. Kluwer, 1993, ISBN 0-7923-9380-5.
- Edmund M. Clarke, Orna Grumberg, Doron A. Peled: Model Checking. The MIT Press, 1999, ISBN 0-262-03270-8.
- Béatrice Bérard, Michel Bidoit, Alain Finkel: Systems and Software Verification: Model-Checking Techniques and Tools. Springer, 2001, ISBN 3-540-41523-8.
Weblinks[Bearbeiten | Quelltext bearbeiten]
Einzelnachweise[Bearbeiten | Quelltext bearbeiten]
- ↑ Kenneth McMillan: Symbolic Model Checking. Kluwer, 1993.
- ↑ NuSMV: a new symbolic model checker