SPIN
SPIN is essentially an implementation of the automata-theoretic1 approach (…), but with a number of enhancements and specializations, as follows.
- It uses on-the-fly Model Checking which effectively involves only constructing the full product, \(\texttt{B}_S \times \texttt{B}_{\lnot \phi}\), where necessary and keeping the \(\texttt{B}_S\) and \(\texttt{B}_{\lnot \phi}\) separate as much as possible.
- It uses partial-order reduction, a method for reducing the number of paths that must be examined during automata-based verification. Specifically, Spin uses the method described in.
- It uses a modified version of acceptance in product automata.
- It uses a particular high-level modelling language, called Promela, to describe both the system to be verified and the property to be checked.
- It is an explicit-state, rather than symbolic, model-checker; the latter being a popular trend.
(…)
SPIN was developed at Bell Labs during the late 1980s, and was initially aimed at verifying properties of communications protocols. However, it is now very popular and is used for checking temporal properties of a wide variety of applications involving concurrent processes.