| Opracowany przez | Gerard Holzmann |
|---|---|
| Pierwsza wersja | 1989 |
| Ostatnia wersja | 6.5.2 (6 grudnia 2019 r) |
| Kaucja | github.com/nimble-code/Spin |
| Napisane w | VS |
| System operacyjny | Linux , Microsoft Windows i macOS |
| Licencja | 3-klauzule BSD ( d ) |
| Stronie internetowej | spinroot.com |
SPIN to ogólne narzędzie do sprawdzania poprawności konkurencyjnych modeli oprogramowania w rygorystyczny i ogólnie zautomatyzowany sposób. Został napisany na początku 1980 roku przez Gerarda J. Holzmanna i innych członków grupy Unix z Computing Sciences Research Center w Bell Labs . Oprogramowanie jest dostępne bezpłatnie od 1991 roku i nadal ewoluuje, aby nadążać za nowymi osiągnięciami w tej dziedzinie.
Systemy, by sprawdzić opisane są w języku Promela (skrót Pro cesu mnie twój The nguage) języka, który wspomaga modelowanie rozproszonych algorytmów asynchronicznych, opisanych jako non-deterministycznych automatów (spin oznacza «Single Promela Tłumaczka»). Właściwości, które mają być sprawdzane, są wyrażane w postaci formuł liniowej logiki czasowej (LTL), które są negowane, a następnie konwertowane na automaty Büchi . Oprócz funkcji sprawdzania modeli , SPIN może również działać jako symulator, podążając dowolną możliwą ścieżką wykonania w systemie i przedstawiając użytkownikowi wynikowy ślad wykonania.
W przeciwieństwie do wielu programów do sprawdzania modeli, SPIN nie wykonuje samego sprawdzenia modelu, ale zamiast tego generuje źródła w języku C dla określonego narzędzia do sprawdzania modelu, odpowiedniego dla problemu. Technika ta oszczędza pamięć i poprawia wydajność, jednocześnie umożliwiając bezpośrednie wstawianie fragmentów kodu C do modelu. SPIN oferuje również dużą liczbę opcji, które dodatkowo przyspieszają proces weryfikacji i oszczędzają pamięć, takie jak:
Od około 1995 roku corocznie organizowane są warsztaty SPIN dla użytkowników SPIN, badaczy i ogólnie zainteresowanych weryfikacją modeli . 26 th Warsztaty odbyły się w Pekinie w 2019 roku .
W 2001 roku Stowarzyszenie na rzecz Maszyn Komputerowych przyznało firmie SPIN nagrodę ACM Software System Award .