Model checking is an automatic technique to verify whether or not a system design satisfies its specifications. Such a verification is moreover exhaustive, i.e. all possible input combinations and states are taken into account. To avoid running out of memory due to a state-space explosion - which would make an exhaustive verification impossible - often a simplified model is used that captures the core of the system design but abstracts from unnecessary details. One of the best known and most successful model checkers is SPIN, which was developed by Gerard Holzmann at Bell Labs during the last two decades. It is freely available through spinroot.com and it is very well documented.
SPIN's input language is Promela, a non-deterministic C-like specification language for modelling finite-state systems communicating through channels. Specifications in Promela can be fed to SPIN, together with a request to verify certain correctness properties. Spin then converts the Promela processes into finite-state automata and on-the-fly creates and traverses the state space of a product automaton over these finite-state automata, in order to verify the specified correctness properties. There are several ways of formalising correctness properties. One way is to add labels to the Promela specification to mark specific points in the specification, which can then be used to formulate LTL formulae and to test their validity by running SPIN. LTL stands for Linear Temporal Logic and it is an extension of predicate logic that allows one to express assertions about behaviour in time, without explicitly modelling time.
I will begin this talk by briefly introducing model checking and SPIN, as well as some of the underlying automata theory. Subsequently I will explain SPIN's input language Promela and LTL in more detail. Finally, I will show an application of model checking with SPIN to an industrial case study.