SPIN model checker
Encyclopedia
SPIN is a general tool for verifying the correctness of distributed 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
, beginning in 1980. The software has been available freely since 1991, and continues to evolve to keep pace with new developments in the field.
Systems to be verified are described in Promela
(Process Meta Language), which supports modeling of asynchronous
distributed algorithms as non-deterministic automata
(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:
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
awarded SPIN its System Software Award.
Gerard J. Holzmann
Gerard J. Holzmann is an American computer scientist, best known as the developer of the SPIN model checker. Holzmann was born in Amsterdam, Netherlands and received an Engineer's degree in Electrical Engineering from the Delft University of Technology in 1976...
and others in the original Unix group of the Computing Sciences Research Center at Bell Labs
Bell Labs
Bell Laboratories is the research and development subsidiary of the French-owned Alcatel-Lucent and previously of the American Telephone & Telegraph Company , half-owned through its Western Electric manufacturing subsidiary.Bell Laboratories operates its...
, beginning in 1980. The software has been available freely since 1991, and continues to evolve to keep pace with new developments in the field.
Systems to be verified are described in Promela
Promela
PROMELA is a verification modeling language. The language allows for the dynamic creation of concurrent processes to model, for example, distributed systems. In PROMELA models, communication via message channels can be defined to be synchronous , or asynchronous...
(Process Meta Language), which supports modeling of asynchronous
Asynchrony
Asynchrony, in the general meaning, is the state of not being synchronized.* Asynchronous learning* Collaborative editing systemsIn specific terms of digital logic and physical layer of communication, an asynchronous process does not require a clock signal, in contrast with synchronous and...
distributed algorithms as non-deterministic automata
Automata theory
In theoretical computer science, automata theory is the study of abstract machines and the computational problems that can be solved using these machines. These abstract machines are called automata...
(SPIN stands for "Simple Promela Interpreter"). Properties to be verified are expressed as Linear Temporal Logic (LTL)
Linear temporal logic
In logic, Linear temporal logic is a modal temporal logic with modalities referring to time. In LTL, one can encode formulae about the future of paths such as that a condition will eventually be true, that a condition will be true until another fact becomes true, etc. It is a fragment of the more...
formulas, which are negated and then converted into Büchi automata
Büchi automaton
In computer science and automata theory, a Büchi automaton is a type of ω-automaton, which extends a finite automaton to infinite inputs. It accepts an infinite input sequence iff there exists a run of the automaton that visits one of the final states infinitely often. Büchi automata recognize the...
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
C (programming language)
C is a general-purpose computer programming language developed between 1969 and 1973 by Dennis Ritchie at the Bell Telephone Laboratories for use with the Unix operating system....
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 reductionPartial order reductionIn computer science, partial order reduction is a technique for reducing the size of the state-space to be searched by a model checking algorithm...
; - state compressionData compressionIn computer science and information theory, data compression, source coding or bit-rate reduction is the process of encoding information using fewer bits than the original representation would use....
; - bitstate hashingBitstate hashingBitstate hashing is a hashing method invented in 1968 by Morris. It is used for state hashing, where each state is represented by a number and it is passed to some hash function....
(instead of storing whole states, only their hash code is remembered in a bitfield; this saves a lot of memory but voids completenessCompletenessIn general, an object is complete if nothing needs to be added to it. This notion is made more specific in various fields.-Logical completeness:In logic, semantic completeness is the converse of soundness for formal systems...
); - weak fairness enforcement.
Since 1995, (approximately) annual SPIN workshops have been held for SPIN users, researchers, and those generally interested in model checking
Model checking
In computer science, model checking refers to the following problem:Given a model of a system, test automatically whether this model meets a given specification....
. In 2001, the Association for Computing Machinery
Association for Computing Machinery
The Association for Computing Machinery is a learned society for computing. It was founded in 1947 as the world's first scientific and educational computing society. Its membership is more than 92,000 as of 2009...
awarded SPIN its System Software Award.