SPIN

SPIN (ursprünglich ein Akronym für Simple PROMELA Interpreter) ist eines der bekanntesten Werkzeuge zur Modellprüfung (englisch Model Checking). 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.[1]

Der jährlich seit 1995 stattfindende SPIN Workshop behandelt mittlerweile nicht nur SPIN, sondern Modellprüfung im Allgemeinen.[2] Im Jahre 2001 wurde Holzmann für seine Arbeit an SPIN mit dem ACM Software System Award der Association for Computing Machinery (ACM) ausgezeichnet.[3]

PROMELA und der Model Checker SPIN wurden u. a. bei der Software-Entwicklung für die 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).

Content Disclaimer

Informasi ini disarikan dari Wikipedia dan disajikan kembali untuk tujuan edukasi. Konten tersedia di bawah lisensi CC BY-SA 3.0. Kami tidak bertanggung jawab atas ketidakakuratan data yang bersumber dari kontribusi publik tersebut.

  1. The information displayed on this website is sourced in part or in whole from Wikipedia and has been adapted for the purpose of restating it. We strive to provide accurate and relevant information, however:
  2. There is no guarantee of absolute accuracy. Wikipedia is an open, collaborative project that can be edited by anyone, so information is subject to change.
  3. It is not intended to constitute professional advice. The content displayed is for informational and educational purposes only. For important decisions (e.g., medical, legal, or financial), please consult a professional.
  4. Content copyright. Wikipedia is licensed under the Creative Commons Attribution-ShareAlike License (CC BY-SA). This means that content may be reused with appropriate attribution and shared under a similar license.
  5. Responsible use. Any risk arising from the use of information from this website is entirely the responsibility of the user.