SPIN Verifier's Roadmap: Spin

SPIN VERIFIER's ROADMAP:
BUILDING AND VERIFYING Spin MODELS

For routine use of Spin, the use iSpin, the graphical interface to Spin, is recommended. iSpin will synthesize all appropriate compile-time and runtime flags, based on menu choices. Spin itself, however, may be used in any environment, independent of the availability of a graphical user interface. For a quick introduction of how to use iSpin, see GettingStarted.html. The following description assumes only the availability of Spin itself, and provides a quick guide through the various verification options that are available. This basic information can be useful to get an initial understanding of Spin's options.
This description assumes that the appropriate software has been installed on your system and that Spin and an ANSI-C compiler are within your search path. If this is not the case, see the README file first.

One

Begin by defining a prototype (a verification model) of the system to be studied in Promela. Consider how you will express the correctness requirements. You can use inline assertions, end-state labels, progress-state labels, acceptance-state labels, LTL properties, or never-claims. In most cases you will only need the first two or three.

Two

For quick debugging of the model: do a simulation run to catch syntax errors and major goofs.
If no flags are provided, Spin performs a random simulation of the model. Add a few options to see useful things happening.
	$ spin -c spec		# simulation run, columnated output
	$ spin -p spec		# simulation run, process moves
(Use "spin --" to see what other options are available at this point.)
You can also add printf statements to the specification to make things more clear.

When done debugging, generate a verifier as follows:

	$ spin -a spec		# generate verifier

Three

Compile the verifier. The biggest decision to make at this point is: can you afford a full verification (CPU-time and memory) or only an approximate supertrace analysis?

Four

Assuming you have compiled an executable verifier in the file 'pan' (short for 'process analyzer'), there are three more decisions you have to make to perform verifications optimally. The decisions are: We look at each of these last decisions below.

And Finally

Internally Spin and pan deal with a formalization of the model in terms of automata. Spin assigns numbers to all statements in the input. These state numbers are listed in all output so that you can, if you want, use that information to track down what happens. To see the state assignments use the runtime option -d for the executable verifier pan:
	$ pan -d	# print state machines
to print the optimized state machine assignments, as it is used during verification. The unoptimized machine (used during random or guided simulations with spin -t for instance) can also be printed, using:
	$ pan -d -d	# print full, unoptimized state machines
These two options should also make it easier to understand and verify the working of Spin/pan in terms of automata theory.

When needed, you can also compile the verifier with -DCHECK, to get verbose printouts from the progress of the search itself.


Spin HomePage (Page Updated: 3 December 2010)