| Entwickelt von | Gerard Holzmann |
|---|---|
| Erste Version | 1989 |
| Letzte Version | 6.5.2 (6. Dezember 2019) |
| Anzahlung | github.com/nimble-code/Spin |
| Geschrieben in | VS |
| Betriebssystem | Linux , Microsoft Windows und MacOS |
| Lizenz | BSD 3-Klauseln ( d ) |
| Webseite | spinroot.com |
SPIN ist ein allgemeines Tool zur strengen und allgemein automatisierten Überprüfung der Richtigkeit wettbewerbsfähiger Softwaremodelle. Es wurde ab 1980 von Gerard J. Holzmann und anderen Mitgliedern der Unix-Gruppe des Computing Sciences Research Center der Bell Labs geschrieben . Die Software ist seit 1991 kostenlos erhältlich und wird weiterentwickelt, um mit den neuen Entwicklungen auf diesem Gebiet Schritt zu halten.
Die Systeme zur Kontrolle sind in der Sprache beschrieben Promela (kurz für Pro cess mir deine The nguage) Sprache , die unterstützt die Modellierung von verteilten Algorithmen asynchron, beschrieben als nicht-deterministische Automaten (SPIN steht für ‚Single Promela Interpreter‘). Die zu überprüfenden Eigenschaften werden in Form von LTL- Formeln ( Linear Temporal Logic ) ausgedrückt , die negiert und dann in Büchi-Automaten konvertiert werden . Zusätzlich zu seiner Funktion als Modellprüfer kann SPIN auch als Simulator fungieren , der jedem möglichen Ausführungspfad durch das System folgt und dem Benutzer die resultierende Ausführungsablaufverfolgung präsentiert.
Im Gegensatz zu vielen Modellprüfern führt SPIN die Modellprüfung nicht selbst durch, sondern generiert C- Quellen für einen bestimmten Modellprüfer, der für das Problem geeignet ist. Diese Technik spart Speicher, verbessert die Leistung und ermöglicht gleichzeitig das direkte Einfügen von C-Code-Teilen in das Modell. SPIN bietet außerdem eine Vielzahl von Optionen, um den Überprüfungsprozess weiter zu beschleunigen und Speicherplatz zu sparen, z.
Seit etwa 1995 finden jährliche SPIN-Workshops für SPIN-Benutzer, Forscher und diejenigen statt, die allgemein an der Modellverifizierung interessiert sind . Der 26 th Workshop fand in Peking im Jahr 2019 .
Im Jahr 2001 verlieh die Association for Computing Machinery SPIN den ACM Software System Award .