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.

- Gerard J. Holzmann,
*The Model Checker SPIN*. IEEE Transactions on Software Engineering - Special issue on Formal Methods in Software Practice 23, 5 (1997), 279-295. - Gerard J. Holzmann,
*The Spin Model Checker - Primer and Reference Manual*. Addison-Wesley, 2003.

- Moshe Y. Vardi and P. Wolper, Reasoning about Infinite Computations. Information and Computation 115, 1 (1994), 1-37.
- Moshe Y. Vardi,
An
Automata-Theoretic Approach to Linear Temporal Logic. In
*Logics for Concurrency - Structure versus Automata. Proceedings of the 8th Banff Higher Order Workshop, 1995*(Faron Moller and Graham M. Birtwistle, eds.),*Lecture Notes in Computer Science*1043, Springer-Verlag, Berlin, 1996, 238-266.

- Maurice H. ter Beek, Mieke Massink, Diego Latella, Stefania Gnesi,
Alessandro Forghieri, and Maurizio Sebastianis, Model
Checking Publish/Subscribe Notification for
**thinkteam**. To appear in*Proceedings of the Ninth International Workshop on Formal Methods for Industrial Critical Systems (FMICS'04) - Affiliated to ASE'04, Linz, Austria*(Alvaro Arenas, Juan Bicarregui, and Andrew Butterfield, eds.),*Electronic Notes in Theoretical Computer Science*, Elsevier Science Publishers, 2005. - Maurice H. ter Beek, Mieke Massink, Diego Latella, Stefania Gnesi,
Alessandro Forghieri, and Maurizio Sebastianis, A
Case Study on the Automated Verification of Groupware Protocols. To
appear in
*Proceedings of the 27th International Conference on Software Engineering (ICSE'05) - Experience Reports Track, St. Louis, MO, U.S.A.*(Connie Heitmeyer and Klaus Pohl, eds.), ACM Press, New York, 2005.