| Udviklet af | Gerard Holzmann |
|---|---|
| Første version | 1989 |
| Sidste version | 6.5.2 (6. december 2019) |
| Depositum | github.com/nimble-code/Spin |
| Skrevet i | VS |
| Operativ system | Linux , Microsoft Windows og macOS |
| Licens | BSD 3-klausuler ( d ) |
| Internet side | spinroot.com |
SPIN er et generelt værktøj til kontrol af rigtigheden af konkurrerende softwaremodeller på en streng og generelt automatiseret måde. Det blev skrevet, begyndende i 1980, af Gerard J. Holzmann og andre medlemmer af Unix-gruppen af Computing Sciences Research Center ved Bell Labs . Softwaren har været tilgængelig gratis siden 1991 og fortsætter med at udvikle sig for at holde trit med den nye udvikling inden for dette område.
Systemerne, der skal kontrolleres, er beskrevet på sprog Promela (forkortelse for Pro cess me thy The nguage) sprog, der understøtter modellering af distribuerede algoritmer asynkront, beskrevet som ' ikke-deterministisk automata (SPIN står for "Single Promela Interpreter"). De egenskaber, der skal kontrolleres, udtrykkes i form af lineære temporale logiske (LTL) formler , som negeres og derefter konverteres til Büchi automata . Ud over sin funktion som modelkontrol kan SPIN også fungere som en simulator, der følger enhver mulig eksekveringssti gennem systemet og præsenterer det resulterende eksekveringsspor for brugeren.
I modsætning til mange modelkontroller udfører SPIN ikke selve modelkontrollen, men genererer i stedet C- kilder til en bestemt modelkontrol, der passer til problemet. Denne teknik sparer hukommelse og forbedrer ydeevnen, samtidig med at den tillader direkte indsættelse af stykker C-kode i modellen. SPIN tilbyder også et stort antal muligheder for yderligere at fremskynde verificeringsprocessen og spare hukommelse, såsom:
Siden omkring 1995 er der afholdt årlige SPIN-workshops for SPIN-brugere, forskere og dem, der generelt er interesserede i modelverifikation . Den 26 th workshop fandt sted i Beijing i 2019 .
I 2001 tildelte Association for Computing Machinery SPIN sin ACM Software System Award .