Utviklet av | Gerard Holzmann |
---|---|
Første versjon | 1989 |
Siste versjon | 6.5.2 (6. desember 2019) |
Innskudd | github.com/nimble-code/Spin |
Skrevet i | VS |
Operativsystem | Linux , Microsoft Windows og macOS |
Tillatelse | BSD 3-ledd ( d ) |
Nettsted | spinroot.com |
SPIN er et generelt verktøy for å kontrollere riktigheten av konkurrerende programvaremodeller på en streng og generelt automatisert måte. Den ble skrevet, begynner i 1980, av Gerard J. Holzmann og andre medlemmer av Unix-gruppen av Computing Sciences Research Center ved Bell Labs . Programvaren har vært tilgjengelig gratis siden 1991 og fortsetter å utvikle seg for å holde tritt med ny utvikling innen dette feltet.
Systemene som skal kontrolleres er beskrevet på språket Promela (forkortelse for Pro cess me thy The nguage) språk som støtter modellering av distribuerte algoritmer asynkrone, beskrevet som ' ikke-deterministisk automata (SPIN står for "Single Promela Interpreter"). Egenskapene som skal kontrolleres uttrykkes i form av lineære temporale logiske (LTL) formler , som negeres og deretter konverteres til Büchi automata . I tillegg til sin modellkontrollfunksjon , kan SPIN også fungere som en simulator, følge en mulig kjøringsbane gjennom systemet og presentere det resulterende kjøringssporet for brukeren.
I motsetning til mange modellbrikker utfører SPIN ikke selve modellkontrollen, men genererer i stedet C- kilder for en spesifikk modellkontroll som passer til problemet. Denne teknikken sparer minne og forbedrer ytelsen, samtidig som det tillates direkte innsetting av stykker C-kode i modellen. SPIN tilbyr også et stort antall alternativer for å øke hastigheten på bekreftelsesprosessen og lagre minne, for eksempel:
Siden 1995 har det blitt holdt årlige SPIN-workshops for SPIN-brukere, forskere og de som generelt er interessert i modellverifisering . Den 26 th workshop fant sted i Beijing i 2019 .
I 2001 tildelte Association for Computing Machinery SPIN sin ACM Software System Award .