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 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
PROMELA (Process or Protocol Meta Language) is a verification modeling language introduced by Gerard J. Holzmann. The language allows for the dynamic creation of concurrent processes to model, for example, distributed systems. In PROMELA models, c ...
(Process Meta Language), which supports modeling of
asynchronous distributed algorithm A distributed algorithm is an algorithm designed to run on computer hardware constructed from interconnected processors. Distributed algorithms are used in different application areas of distributed computing, such as telecommunications, scientific ...
s 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 More ...
(''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 Buchi can mean:
__NOTOC__
Items
*Bachi, special Japanese drumsticks
*Butsi, the Hispanised term for jin deui (pastry made from glutinous rice) in the Philippines
*Büchi automaton, finite state automata extended to infinite inputs
* Büchi arithmet ...
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 In computer science, partial order reduction is a technique for reducing the size of the state-space to be searched by a model checking or automated planning and scheduling algorithm. It exploits the commutativity of concurrently executed transit ...
;
*state
compression
Compression may refer to:
Physical science
*Compression (physics), size reduction due to forces
*Compression member, a structural element such as a column
*Compressibility, susceptibility to compression
* Gas compression
*Compression ratio, of a ...
;
*
bitstate hashing Bitstate hashing is a hash function, hashing method invented in 1968 by Morris. It is used for state hashing, where each state (e.g. of an automaton) is represented by a number and it is passed to some hash function.
The result of the function is t ...
(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 computer science, model checking or property checking is a method for checking whether a finite-state model of a system meets a given specification (also known as correctness). This is typically associated with hardware or software systems ...
.
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
NuSMV is a reimplementation and extension of SMV symbolic model checker, the first model checking tool based on Binary Decision Diagrams (BDDs).K.L. McMillan. Symbolic model checking. In Kluwer Academic Publ.,1993.
The tool has been designed as a ...
* Uppaal Model Checker
UPPAAL is an integrated tool environment for modeling, validation and verification of real-time systems modeled as networks of timed automata, extended with data types (bounded integers, arrays etc.).
It has been used in at least 17 case studies ...
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 through ...
, 2004. {{ISBN, 0-321-22862-6.
External links
SPIN website
Model checkers