SPIN is a general tool for verifying the correctness of
concurrent software models in a rigorous and mostly automated fashion. It was written by
Gerard J. Holzmann
Gerard J. Holzmann (born 1951) is a Dutch-American computer scientist and researcher at Bell Labs and NASA, best known as the developer of the SPIN model checker.
Biography
Holzmann was born in Amsterdam, Netherlands and received an Engineer ...
and others in the original Unix group of the Computing Sciences Research Center at
Bell Labs
Nokia Bell Labs, originally named Bell Telephone Laboratories (1925–1984),
then AT&T Bell Laboratories (1984–1996)
and Bell Labs Innovations (1996–2007),
is an American industrial research and scientific development company owned by mult ...
, beginning in 1980. The software has been available freely since 1991, and continues to evolve to keep pace with new developments in the field.
Tool
Systems to be verified are described in
Promela (Process Meta Language), which supports modeling of
asynchronous distributed algorithms as
non-deterministic automata
An automaton (; plural: automata or automatons) is a relatively self-operating machine, or control mechanism designed to automatically follow a sequence of operations, or respond to predetermined instructions.Automaton – Definition and Mor ...
(''SPIN'' stands for "Simple Promela Interpreter"). Properties to be verified are expressed as
Linear Temporal Logic (LTL) formulas, which are negated and then converted into
Büchi automata as part of the model-checking algorithm. In addition to model-checking, SPIN can also operate as a simulator, following one possible execution path through the system and presenting the resulting execution trace to the user.
Unlike many model-checkers, SPIN does not actually perform model-checking itself, but instead generates
C sources for a problem-specific model checker. This technique saves memory and improves performance, while also allowing the direct insertion of chunks of C code into the model. SPIN also offers a large number of options to further speed up the model-checking process and save memory, such as:
*
partial order reduction;
*state
compression;
*
bitstate hashing (instead of storing whole states, only their hash code is remembered in a bitfield; this saves a lot of memory but voids
completeness);
*weak fairness enforcement.
Since 1995, (approximately) annual SPIN workshops have been held for SPIN users, researchers, and those generally interested in
model checking.
In 2001, the
Association for Computing Machinery
The Association for Computing Machinery (ACM) is a US-based international learned society for computing. It was founded in 1947 and is the world's largest scientific and educational computing society. The ACM is a non-profit professional member ...
awarded SPIN its System Software Award.
Software System Award: ACM CITES TOOL TO DETECT SOFTWARE "BUGS" FOR PRESTIGIOUS AWARD. Bell Labs Researcher Developed "SPIN" to Make Computers More Reliable
// ACM Press-Release
See also
* NuSMV
* Uppaal Model Checker
References
Further reading
*Holzmann, G. J., ''The SPIN Model Checker: Primer and Reference Manual''. Addison-Wesley
Addison-Wesley is an American publisher of textbooks and computer literature. It is an imprint of Pearson PLC, a global publishing and education company. In addition to publishing books, Addison-Wesley also distributes its technical titles throug ...
, 2004. {{ISBN, 0-321-22862-6.
External links
SPIN website
Model checkers