SPIN Model Checker (tutored by "Jean Claude" Van Hung)

What is Model Checking?
“Model checking is an automated technique that, given a finite-state model of a system and a logical property, systematically checks whether this property holds for (a given initial state in) that model.”

What is SPIN?
Spin is a tool for analyzing the logical consistency of concurrent systems, specifically of data communication protocols. The system is described in a modeling language called Promela (Process Meta Language). The language allows for the dynamic creation of concurrent processes. Communication via message channels can be defined to be synchronous (i.e., rendezvous), or asynchronous (i.e., buffered).

Given a model system specified in Promela, Spin can either perform random simulations of the system's execution or it can generate a C program that performs an efficient online verification of the system's correctness properties. During simulation and verification Spin checks for the absence of deadlocks, unspecified receptions, and unexecutable code. The verifier can also be used to verify the correctness of system invariants, it can find non-progress execution cycles, and it can verify correctness properties expressed in next-time free linear temporal logic formulae.

The verifier is setup to be efficient and to use a minimal amount of memory. An exhaustive verification performed by Spin can establish with mathematical certainty whether or not a given behavior is error-free. Very large verification problems, that can ordinarily not be solved within the constraints of a given computer system, can be attacked with a frugal ``bit state storage'' technique, also known as supertrace. With this method the state space can be collapsed to a small number of bits per reachable system state, with minimal side-effects.

for reference : please open http://spinroot.com