https://wiki-de.moshellshocker.dns64.de/index.php?action=history&feed=atom&title=Symbolic_Model_VerifierSymbolic Model Verifier - Versionsgeschichte2026-05-26T19:11:55ZVersionsgeschichte dieser Seite in Wikipedia (Deutsch) – Lokale KopieMediaWiki 1.43.8https://wiki-de.moshellshocker.dns64.de/index.php?title=Symbolic_Model_Verifier&diff=984963&oldid=previmported>Invisigoth67: typo2024-08-10T08:40:07Z<p>typo</p>
<p><b>Neue Seite</b></p><div>Der '''Symbolic Model Verifier''' ('''SMV''') ist ein Werkzeug zur [[Modellprüfung]] ({{enS|Model Checking}}). Dieser Model Checker prüft [[Endlicher Automat|endliche Zustandsautomaten]] (engl. {{lang|en|''finite state machines''}}) mit der temporalen Logik [[Computation Tree Logic|CTL]]. SMV wurde von [[Kenneth L. McMillan]] im Rahmen seiner Doktorarbeit<ref>Kenneth McMillan: ''Symbolic Model Checking.'' Kluwer, 1993.</ref> an der [[Carnegie Mellon University]] entwickelt.<br />
<br />
== Technologie ==<br />
<br />
Die Eingabesprache erlaubt es, einen Automaten synchron, asynchron, detailliert oder abstrakt zu beschreiben. In der Sprache gibt es nur finite [[Datentyp]]en, also [[boolesche Variable]]n, [[skalare Variable]]n und feste [[Feld (Datentyp)|Arrays]]. Statische, strukturierte Datentypen können jedoch erstellt werden.<br />
<br />
CTL unterstützt die präzise Definition von zeitlichen Eigenschaften wie Safety, Lebendigkeit, [[Fairness]] oder [[Deadlock (Informatik)|Deadlock]]-Freiheit. Um die Modelle zu prüfen, verwendet SMV einen symbolischen Algorithmus, der auf geordneten [[Binäres Entscheidungsdiagramm|binären Entscheidungsdiagrammen]] (OBDD) basiert.<br />
<br />
=== Eingabedatei ===<br />
<br />
Die Eingabedatei enthält die Beschreibung des Zustandsautomaten und die Anforderungsspezifikation in der Eingabesprache von SMV.<br />
<br />
=== Darstellung von Zuständen ===<br />
<br />
Die Zustände werden durch [[Aufzählungstyp|Enumerationen]] dargestellt. Das Verhalten kann [[Nichtdeterminismus|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 [[Interaktion]]en zwischen Systemkomponenten.<br />
<br />
=== Interaktionen zwischen Systemkomponenten ===<br />
<br />
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.<br />
<br />
Bei der [[Verifizierung|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.<br />
<br />
== Aktuelle Version ==<br />
<br />
Das letzte [[Entwicklungsstadium (Software)#Release|Release]] von SMV ist Version 2.5 für [[Windows NT]] aus dem Jahr 1998. Der ''Model Checker'' läuft auf SunOS 5, [[Solaris (Betriebssystem)|Solaris]], [[Linux]], [[Ultrix]].<br />
<br />
=== NuSMV ===<br />
<br />
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 [[Erfüllbarkeitsproblem der Aussagenlogik|SAT solvers]]. Es wurde als offene Architektur entworfen und findet rege Verwendung in anderen Projekten.<br />
<br />
NuSMV-2 ist als [[Open Source|quelloffene Software]] unter der [[LGPL]] veröffentlicht worden.<br />
<br />
Die neueste Version von NuSMV ist Version 2.6.0<ref>[https://nusmv.fbk.eu/ NuSMV: a new symbolic model checker]</ref> NuSMV-2 kann unter den meisten gängigen [[Betriebssystem]]en, die den [[POSIX]]-Standard unterstützen, [[Kompilierung|kompiliert]] werden. Auf der Website wird auch ein [[Windows]]-Installer angeboten.<br />
<br />
== Literatur ==<br />
<br />
* [[Kenneth L. McMillan|Kenneth Mc Millan]]: ''Symbolic Model Checking''. Kluwer, 1993, ISBN 0-7923-9380-5.<br />
* [[Edmund M. Clarke]], [[Orna Grumberg]], Doron A. Peled: ''Model Checking''. The MIT Press, 1999, ISBN 0-262-03270-8.<br />
* Béatrice Bérard, Michel Bidoit, Alain Finkel: ''Systems and Software Verification: Model-Checking Techniques and Tools''. Springer, 2001, ISBN 3-540-41523-8.<br />
<br />
== Weblinks ==<br />
* [http://www.cs.cmu.edu/~modelcheck/smv.html SMV-Seite der Carnegie Mellon University]<br />
* [http://nusmv.irst.itc.it/ NuSMV Quellcode und Binaries]<br />
<br />
== Einzelnachweise ==<br />
<references /><br />
<br />
[[Kategorie:Automatentheorie]]</div>imported>Invisigoth67