SPIN

Vorlage:Hinweisbaustein SPIN (ursprünglich ein Akronym für Simple PROMELA Interpreter) ist eines der bekanntesten Werkzeuge zur Modellprüfung (). SPIN prüft endliche Zustandsautomaten (engl. Finite State Machines) mit der temporalen Logik LTL. Zusätzlich bietet SPIN viele Optimierungsmethoden, zum Beispiel Partial Order Reduction, Komprimierungen und Bitstate Hashing.

Geschichte

SPIN wurde 1980 von Gerard J. Holzmann entwickelt, anfangs am Computing Sciences Research Center der Bell Labs. Der Quellcode zu SPIN wurde 1991 unter einer eigenen Lizenz offengelegt.<ref>Lizenz von SPIN</ref>

Der jährlich seit 1995 stattfindende SPIN Workshop behandelt mittlerweile nicht nur SPIN, sondern Modellprüfung im Allgemeinen.<ref>Vergangene SPIN-Workshops auf der SPIN-Website</ref> Im Jahre 2001 wurde Holzmann für seine Arbeit an SPIN mit dem ACM Software System Award der Association for Computing Machinery (ACM) ausgezeichnet.<ref>Software System Award (Memento des Vorlage:IconExternal vom 23. Dezember 2009 im Internet Archive) Datei:Pictogram voting info.svg Info: Der Archivlink wurde automatisch eingesetzt und noch nicht geprüft. Bitte prüfe Original- und Archivlink gemäß Anleitung und entferne dann diesen Hinweis.@1@2Vorlage:Webachiv/IABot/awards.acm.org auf acm.org</ref>

PROMELA und der Model Checker SPIN wurden u. a. bei der Software-Entwicklung für die Marssonde Curiosity eingesetzt.<ref name="Holzmann:2014:MC:2556647.2560218" />

Siehe auch

• Symbolic Model Verifier

Literatur

• Gerard J. Holzmann: The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley, 2004. ISBN 0-321-22862-6.

Weblinks

• Website von SPIN
• Literaturliste

Einzelnachweise

<references> <ref name="Holzmann:2014:MC:2556647.2560218">

</ref> </references>