SPIN

aus Wikipedia, der freien Enzyklopädie
Wechseln zu: Navigation, Suche
Der Titel dieses Artikels ist mehrdeutig. Für andere Bedeutungen siehe Spin (Begriffsklärung)

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

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]

Siehe auch[Bearbeiten]

Literatur und Weblinks[Bearbeiten]

Einzelnachweise[Bearbeiten]

  1. Lizenz von SPIN
  2. Vergangene SPIN-Workshops auf der SPIN-Website
  3. Software System Award auf acm.org