| Vyvinul | Gerard Holzmann |
|---|---|
| První verze | 1989 |
| Poslední verze | 6.5.2 (6. prosince 2019) |
| Vklad | github.com/nimble-code/Spin |
| Napsáno | VS |
| Operační systém | Linux , Microsoft Windows a macOS |
| Licence | 3-věty BSD ( d ) |
| webová stránka | spinroot.com |
SPIN je obecný nástroj pro kontrolu správnosti konkurenčních softwarových modelů důsledným a obecně automatizovaným způsobem. To bylo napsáno počátkem roku 1980 Gerardem J. Holzmannem a dalšími členy skupiny Unix Výzkumného centra pro výpočetní vědy v Bell Labs . Software je k dispozici zdarma od roku 1991 a neustále se vyvíjí, aby držel krok s novým vývojem v této oblasti.
Systémy ke kontrole jsou popsány v jazyce PROMELA (zkratka pro Pro chu mě tvůj The nguage) jazyk, který podporuje modelování distribuovaných algoritmů asynchronních, popsané jako non-deterministický automatů (SPIN je zkratka pro ‚Single PROMELA Interpreter‘). Vlastnosti, které mají být zkontrolovány, jsou vyjádřeny ve formě vzorců lineární časové logiky (LTL), které jsou negovány a poté převedeny na Büchiho automaty . Kromě své funkce kontroly modelu může SPIN také fungovat jako simulátor, sledovat jakoukoli možnou cestu provádění v systému a prezentovat výslednou stopu spuštění uživateli.
Na rozdíl od mnoha kontrolních modelů SPIN neprovádí samotnou kontrolu modelu, ale místo toho generuje C zdroje pro konkrétní kontrolu modelu vhodnou pro daný problém. Tato technika šetří paměť a zlepšuje výkon a zároveň umožňuje přímé vkládání částí kódu C do modelu. SPIN také nabízí velké množství možností pro další zrychlení procesu ověřování a úsporu paměti, například:
Od roku 1995 se každoročně konají workshopy SPIN pro uživatele, výzkumníky a ty, kteří se obecně zajímají o ověření modelu . 26 th workshop se konal v Pekingu v roce 2019 .
V roce 2001 udělila Asociace pro výpočetní techniku společnosti SPIN cenu ACM Software System Award .