Kontrola modelu SPIN - SPIN model checker
 | Tento článek má několik problémů. Prosím pomozte vylepši to nebo diskutovat o těchto otázkách na internetu diskusní stránka. (Zjistěte, jak a kdy tyto zprávy ze šablony odebrat) (Zjistěte, jak a kdy odstranit tuto zprávu šablony)
|
| Vývojáři | Gerard J. Holzmann |
|---|---|
| První vydání | 1989 |
| Stabilní uvolnění | 6.5.2 / 6. prosince 2019 |
| Úložiště |  |
| Napsáno | C |
| Operační systém | Linux Microsoft Windows Mac OS X |
| K dispozici v | Angličtina |
| Typ | Kontrola modelu |
| Licence |
|
| webová stránka | http://spinroot.com/ |
ROZTOČIT je obecný nástroj pro ověřování správnosti souběžný software modely důsledně a většinou automatizovaným způsobem. Napsal to Gerard J. Holzmann a další v původní unixové skupině Výzkumného centra pro výpočetní vědy v Bell Labs, počínaje rokem 1980. Software je volně dostupný od roku 1991 a neustále se vyvíjí, aby držel krok s novým vývojem v této oblasti.
Nářadí
Systémy, které mají být ověřeny, jsou popsány v Promela (Process Meta Language), který podporuje modelování asynchronní distribuované algoritmy tak jako nedeterministický automaty (ROZTOČIT znamená „Simple Promela Interpreter“). Vlastnosti, které mají být ověřeny, jsou vyjádřeny jako Lineární dočasná logika (LTL) vzorce, které jsou negovány a poté převedeny na Büchi automaty jako součást algoritmu kontroly modelu. Kromě kontroly modelu může SPIN také fungovat jako simulátor, sledovat jednu 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 ve skutečnosti neprovádí samotnou kontrolu modelu, ale generuje C zdroje pro kontrolu modelu konkrétního problému. Tato technika šetří paměť a zlepšuje výkon a zároveň umožňuje přímé vkládání bloků kódu C do modelu. SPIN také nabízí velké množství možností, jak dále urychlit proces kontroly modelu a ušetřit paměť, například:
- částečné snížení objednávky;
- Stát komprese;
- bitstate hash (namísto ukládání celých států je v bitfieldu zapamatován pouze jejich hash kód; to šetří spoustu paměti, ale neplatí úplnost );
- slabé prosazování spravedlnosti.
Od roku 1995 se konají (přibližně) každoroční workshopy SPIN pro uživatele, výzkumníky a ty, kteří se o SPIN obecně zajímají kontrola modelu.
V roce 2001 Sdružení pro výpočetní techniku udělil společnosti SPIN cenu System Software Award.[1]
Viz také
Reference
Další čtení
- Holzmann, G. J., Kontrola modelu SPIN: Primer a referenční příručka. Addison-Wesley, 2004. ISBN 0-321-22862-6.