SPIN Verifier's Roadmap: Spin

`SPIN VERIFIER's ROADMAP: BUILDING AND VERIFYING Spin MODELS`

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, 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?

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 how much physical memory your system has, use this to restrict the maximum amount that verifications can take to avoid unpleasant paging behavior, for instance, if you have 256 Megabyte available compile as follows.
```
	$ cc -DMEMLIM=256 -o pan pan.c   # memory bound 256Mb
```
If the verification still runs out of memory, use compression instead of increasing the memory limit above what is available on your system, for instance:
```
	$ cc -DMEMLIM=256 -DCOLLAPSE -o pan pan.c # collapse compression
```
If also this is insufficient, and exceeds the memory bounds, switch to supertrace.
Supertrace verification. Compile as follows.
```
	$ cc -DMEMLIM=256 -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.

`Four`

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:

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 liveness properties),
selecting the maximum search depth,
selecting the parameters for an inspection of the error that is found, if so.

We look at each of these last decisions below.

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 23 if you expect 8 million reachable states and can use 8 million bits of memory (i.e., 2²³ bits is 8 million bits, which requires 2 ²⁰ or just 1 Megabyte of RAM).
It's also no problem here 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
or:
	$ cc -DNP -DBITSTATE -o pan pan.c
followed by:
	$ 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
or
	$ cc -DSAFETY -DBITSTATE -o pan pan.c
```
In this case you can also try Spin's breadth-first search mode, which works only for safety properties but has the advantage of finding short error traces:
```
	$ cc -DBFS -o pan pan.c
```
This search mode can be combined with all compression methods ( BITSTATE, COLLAPSE, MA, HC4, etc.).
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 -c 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
```

`And Finally`

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 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: 7 January 2003)