SPIN VERIFIER's ROADMAP:
For routine use of Spin, the use Xspin, the graphical
interface to Spin, is recommended. Xspin 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 Xspin,
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.
BUILDING AND VERIFYING Spin MODELS
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
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,
In most cases you will only need the first two or three.
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
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
Full verification. Compile as follows.
$ cc -o pan pan.c # default compilation
or to decline partial order reduction (useful for tests only!)
The reduction preserves correctness properties.
$ cc -DNOREDUCE -o pan pan.c # rarely used
If you know an exact memory bound that you want to restrict
verification runs to (e.g., to avoid paging), find the nearest
power of 2 (e.g., 23 for the bound 223)
and compile as follows.
$ cc -DMEMCNT=23 -o pan pan.c # memory bound 223 bytes
If the verification runs out of memory increase the memory bound
or, if this is impossible, use compression:
$ cc -DMEMCNT=23 -DCOLLAPSE -o pan pan.c # memory bound 223
If also this is insufficient, and exceeds the memory bounds,
switch to supertrace.
Supertrace verification. Compile as follows.
$ cc -DBITSTATE -o pan pan.c # supertrace algorithm
This is typically used as the method of last resort when a full
verication turns out to be infeasible because of memory limitations.
It can also be used as a fast prescan of the problem, to get an
early and quick indication of the presence or absence of errors.
Assuming you have compiled an executable verifier in the
file 'pan' (short for 'protocol analyzer'),
there are four more decisions you have to make to
perform verifications optimally.
The decisions are:
We look at each of these last decisions below.
- selecting a good size of the hashtable, which is in effect
an estimate of the number of reachable states,
- selecting the type of property to be verified (safety or
- selecting the maximum search depth,
- selecting the parameters for an inspection of the error
that is found, if so.
For a full verification (i.e., if you compiled without the -DBITSTATE
option), set the size of the hashtable with runtime option -w.
$ pan -w23
The argument defines the number of states you expect as a power of 2.
Don't worry if you set the argument too low or too high:
setting it too high merely wastes some memory, too low wastes some
cpu-time, but both will complete correctly.
For a supertrace run (i.e., you compiled with -DBITSTATE),
the hashtable is the memory arena,
so set it to the maximum size of memory you can grab without
making the system page (i.e., set it to the
amount of real physical memory you can use).
The -w argument should again equal at least the nearest
power of 2 of the total number of reachable system states you expect.
For instance, use 26 if you expect 8 million reachable states
and can use 8 million bits of memory
(i.e., 226 bits is 8 million bits,
which requires 2 23 or 1 Megabyte of RAM).
It's also no problem her if you set the number too high or too low.
Too low will not fully utilize available memory, and give you lower
coverage than possible. Too high means asking for more memory than
your system has available -- the system will complain.
The second runtime decision is to decide if you want to check the model
for non-progress cycles (and only non-progress cycles),
acceptance cycles (and only acceptance cycles), or safety properties.
For acceptance cycles use option -a:
$ pan -a
For non-progress cycles you must add the directive -DNP when
compiling Spin. After that, you can use run-time option -l
(Spin will warn you if you forget -DNP):
$ cc -DNP -o pan pan.c
$ cc -DNP -DBITSTATE -o pan pan.c
$ pan -l
If you don't use options -l or -a, only basic safety properties
are checked (assertion violations, unreachable code, etc).
In that case, you can obtain a faster verifier by compiling:
$ cc -DSAFETY -o pan pan.c
$ cc -DSAFETY -DBITSTATE -o pan pan.c
The next decision has to do with the search depth.
By default the verifiers have a search depth restriction of 10,000 steps.
If this isn't enough, the search will truncate at 9,999 steps (watch for
it in the printout).
You can define a different searchdepth with the -m flag.
$ pan -m100000
If you find a particularly nasty error that takes a large number of steps
to hit, you may also set lower search depths to find the shortest variant
of an error sequence.
$ pan -m40
Or you can ask Spin to iterative home in on shorter versions of the
error. In that case, add the compile time directive -DREACH when
you compile pan.c, and use either the -i or the -I runtime flag:
$ cc -DREACH -o pan pan.c
$ pan -m100000 -I # iterative search for short errors
You can now do a first verification run.
If you see that any of the verification parameters you chose earlier was
wrong (e.g., amount of memory available, or number of reachable states)
adjust and repeat.
If you find an error, any error, Spin dumps an error-trail into the
file `spec.trail', where `spec' is the name of your PROMELA input.
To inspect the trail, and examine the cause of the error, use a
guided simulation with option -t:
$ spin -t -p spec
Add as many extra or different options as you need to pin down the error.
(You can check Spin's available options by typing: "spin --" .)
One option is to convert the trail into a Postscript represetation of
a message sequence chart of send and receive actions:
$ spin -t -M spec
Or a rough approximation of this in plain ASCII:
$ spin -t -c spec
For more detailed tracebacks use, for instance:
$ spin -t -r -s -l -g spec
Make sure the file `spec' didn't change since you generated the verifier.
(Spin will warn if you did.)
If you find non-progress cycles: add or delete progress labels
and repeat the verifications until you're content that you found what
you're looking for.
If you're not interested in the first error you see, use option -c to print
others into the trail
$ pan -c3
prints the third error into the trail.
If you just want to count all errors and not see them, use
$ pan -c0
By default, the argument is 1.
If you want to obtain a trail for each and every error, use:
$ pan -e -c0
This creates a series of error trails in files numbers spec.trail,
spec2.trail, spec3.trail, ...etc., where "spec" is the name of the
file from which you created the verifier.
To trace back a specific one of these trails, you must specify the
appropriate number with the -t option:
$ pan -e -c0
$ spin -t6 -c spec
Internally Spin and pan deal with a formalization of
the model in terms of labeled transition systems.
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
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.