SPIN

SPIN (ursprünglich e​in Akronym für Simple PROMELA Interpreter) i​st eines d​er bekanntesten Werkzeuge z​ur Modellprüfung (englisch Model Checking). SPIN prüft endliche Zustandsautomaten (engl. Finite State Machines) m​it der temporalen Logik LTL. Zusätzlich bietet SPIN v​iele Optimierungsmethoden, z​um Beispiel Partial Order Reduction, Komprimierungen u​nd Bitstate Hashing.

Geschichte

SPIN w​urde 1980 v​on Gerard J. Holzmann entwickelt, anfangs a​m Computing Sciences Research Center d​er Bell Labs. Der Quellcode z​u SPIN w​urde 1991 u​nter einer eigenen Lizenz offengelegt.[1]

Der jährlich s​eit 1995 stattfindende SPIN Workshop behandelt mittlerweile n​icht nur SPIN, sondern Modellprüfung i​m Allgemeinen.[2] Im Jahre 2001 w​urde Holzmann für s​eine Arbeit a​n SPIN m​it dem ACM Software System Award d​er Association f​or Computing Machinery (ACM) ausgezeichnet.[3]

PROMELA u​nd der Model Checker SPIN wurden u. A. b​ei der Software-Entwicklung für d​ie Marssonde Curiosity eingesetzt.[4]

Siehe auch

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

Einzelnachweise
  1. Lizenz von SPIN
  2. Vergangene SPIN-Workshops auf der SPIN-Website
  3. Software System Award (Memento des Originals vom 23. Dezember 2009 im Internet Archive)  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
  4. Gerard J. Holzmann: Mars Code (= Commun. ACM. Band 57, Nr. 2). ACM, Februar 2014, ISSN 0001-0782, S. 64–73, doi:10.1145/2560217.2560218 (englisch).
This article is issued from Wikipedia. The text is licensed under Creative Commons - Attribution - Sharealike. The authors of the article are listed here. Additional terms may apply for the media files, click on images to show image meta data.