Partial-Order Package for SPIN

SPIN is an automated validation system for communication protocols described in the PROMELA language. SPIN performs an exploration of the protocol state space by using a classical depth-first search algorithm. This algorithm recursively explores all successor states of all states encountered during the search, starting from the initial state, by executing all enabled transitions in each state. Of course, the number of visited states can be very large: this is the well-known state-explosion problem, which limits the applicability of state-space exploration techniques.

The Partial-Order Package implements a combination of several verification techniques that attempt to avoid the part of the state explosion due to the exploration of all possible interleavings of concurrent transitions. These techniques verify properties of systems by exploring as few interleavings as possible for each partial order execution that the system can perform. The other interleavings are not explored.

The Partial-Order Package includes algorithms for generating such reduced state spaces from any PROMELA program and for checking deadlocks, unreachable code and assertion violations.


You can obtain the Partial-Order Package from here.


The main reference describing the algorithms implemented in the Partial-Order Package and presenting results of experimentations is

Partial-order Methods for the Verification of Concurrent Systems -- An Approach to the State-Explosion Problem , Patrice Godefroid, volume 1032 of Lecture Notes in Computer Science, January 1996. (ISBN 3-540-60761-7)

Other related papers are