SPIN VERIFIER's ROADMAP:
BUILDING AND VERIFYING Spin MODELS

The following description provides a basic overview of the verification options that can be used with the Spin model checker. This description assumes that Spin has been installed and that you have a standard C compiler (such as gcc) as well. It also assumes that you are familiar with standard shell command use on a Unix-like system (e.g., Ubuntu Linux, MAC-OS-X, or Cygwin on a Windows-PC).

-0-

Verification begins with the specification of a prototype of the system to be studied in the specification language supported by Spin. This language is called ProMeLa (short for Process Meta Language), and the model is called a verification model, or a Spin model.
By convention, ProMeLa specification files have a .pml file extension.

Next you must consider how you can express the critical correctness requirements for your model. You can use assertions, end-state labels, progress-state labels, acceptance-state labels, or LTL properties. But don't worry, in most cases of practical interest you will only need assertions, and less frequently simple LTL properties.

-1-

For a quick checkout of the model you have just defined: do a simulation run to catch the simpler mistakes.
If no flags are provided, Spin performs a random simulation of the model. 
	$ spin spec.pml		# no options: only print statements produce output
It is often very helpful, especially at this stage in debugging the basic verification model, to add printf statements to the specification to make things more clear.

You can add more options to see useful things happening. Without additional flags, only print statements that you use in the model will produce output. If there are none, you may want to use some additional flags. 

	$ spin -p spec.pml	# simulation run, show all execution steps
	$ spin -c spec.pml	# columnated output for message i/o
You can use the command: 
	$ spin --
to see what other options are available for including additional information in the simulation runs.
An important one, in case your model can execute forever, is the ability to set an upper-limit on the number of execution steps performed in a simulation. For instance, to limit the simulation to the first 200 steps: 
	$ spin -u200 -p -l -g -v spec.pml
Check in the output of spin -- what the additional flags that are used here do.

When done debugging, you can perform a more thorough check of your model with this command: 

	$ spin -a spec.pml		# thorough check
This step can report syntax errors and impurities that the simulation commands don't catch. For feedback on possible redundancies in your specification, try also: 
	$ spin -A spec.pml		# check for redundancies
And, if you really want to get carried away, you can look at the automata descriptions that Spin generates for you for the verifier's use, by executing: 
	$ spin -search -dump spec.pml
or just
	$ spin -search -d spec.pml
If, on the other hand you just want to get a quick basic verification run going, use this command, which will compile and run your verification immediately: 
	$ spin -search spec.pml
And the rest, as they say, is just detail. We will indulge in some of that detail in the next few points.

-2-

The biggest decision to make is if the model you created is simple enough to perform a fully exhaustive verification on the machine that you are using. The limits, as always, are CPU-time and RAM memory. The good news is that even if you do not have enough time or memory, Spin can be configured to give you the best possible result within the constraints that you do have. We will first consider how you can setup a standard exhaustive verification run.
Exhaustive
For an exhaustive verification, you can compile the generated verification code as follows. 
	$ spin -search -O2 spec.pml            # use optimized compilation
It is always smart to use the -O2 flag to optimize the code: it can often reduce the runtime needed by about 50%.

If you know how much physical (not virtual) RAM memory your system has, you can use this to restrict the maximum amount that a verification can take to avoid unpleasant paging behavior, for instance, if you have 256 Megabyte available compile as follows. 

	$ spin -search -O2 -DMEMLIM=256 spec.pml   # set memory bound at 256MB
If the amount of memory you have is not sufficient to complete a verification, consider using one of the compression options that Spin supports. For instance: 
	$ spin -search -O2 -DMEMLIM=256 -collapse spec.pml # use compression
or, for a still more aggressive option, try: 
	$ spin -search -O2 -DMEMLIM=256 -hc spec.pml # use hash-compact compression
If also this is insufficient, and your verification still exceeds the memory bounds, switch to Bitstate verification run (also known as a Supertrace verification).

Bitstate
For a Bitstate verification run, compile as follows. 

	$ spin -search -O2 -bitstate spec.pml    # use bitstate search
This is often used as a method of last resort when a full verication is infeasible because of memory limitations or problem size. It can also be used as a fast prescan of a problem, to get an early and quick indication of the presence or absence of errors.

-3-

Up to this point we have ignored what type of property you are trying to verify, or what impact problem size may have on your chances of performing a successful verification. We will address these points now.

There are four more decisions you have to make to perform verifications optimally. These four decisions are:

  1. Selecting the type of property to be verified (safety or liveness)
  2. Selecting the maximum search depth,
  3. If you use a Bitstate search: selecting the size of the hash-table
  4. Selecting the parameters for a replay of an error, if one is found.
We'll now explore each of these decisions in more detail.

  1. The first decision is to decide if you want to check the model for Safety properties or for Liveness properties.
    Safety
    Examples of safety properties are assertion violations, deadlocks (invalid end-states), etc.

    To check safety properties only (the most frequently used search mode), you can obtain a fast verifier by adding a -safety argument: 

    		$ spin -search -safety spec.pml
    plus of course any of the other arguments we discussed earlier, for instance: 
    		$ spin -search -O2 -bitstate -safety spec.pml
    In this case you can also use Spin's breadth-first search mode, which works only for safety properties but has the advantage of finding the shortest possible error traces: 
    		$ spin -search -bfs spec.pml
    again combined with any other options you need.

    Liveness
    Examples of liveness properties are non-progress or acceptance cycles. LTL properties can express both safety and liveness properties. In case of doubt: assume you have a liveness property.

    To perform a search for violations of general liveness properties you use the runtime parameter -a following the -search argument to Spin. For instance: 

    		$ spin -search -a spec.pml
    plus any other runtime arguments you selected.

    Non-Progress
    A non-progress cycle is an infinite execution that never passes through any state in the specification that is marked with a labelname that starts with the prefix "progress".

    To search for non-progress cycles you add run-time option -l, for instance as in: 

    		$ spin -search -l spec.pml
    plus any other runtime arguments you selected.

  2. By default the Spin verifiers enforce a search depth restrictionof 10,000 steps. In most cases this will suffice, but when it doesn't the search depth will artificially be truncated to 9,999 steps and become incomplete. You can define a different search-depth by adding a runtime parameter -m. For instance: 
    	$ spin -search -m100000 spec.pml
    (again, combined with any other options you select).

    You can also try to set a lower search depth to try to find a shorter variant of an error sequence. For instance 

    	$ spin -search -m40 spec.pml
    But in thise case there is no guarantee that if a shorter error sequence exists it will also be found. To get that guarantee you also have to instruct Spin to modify the search algorithm itself, with a runtime parameter -i to force a search for a short error. For instance, to search for errors shorter than 100 steps: 
    	$ spin -search O2 -i -m100 spec.pml	# iterative search for short errors
  3. If you perform a Bitstate verification (i.e., you used the search argument -bitstate), the size of the memory arena that is used to store states very compactly is determined by your choice of a -w parameter. By default, this parameter is set to -w27, which defines a memory arena of 227 bits, corresponding to a modest 16 MB of RAM.
    For maximum coverage you want to set the hash-array size to the maximum size of memory you can grab without making the system page (i.e., below the amount of real physical RAM memory that you can access).

    More specifically, for maximum coverage, the value you set with the -w parameter should at least be larger than the nearest power of 2 of the number of reachable system states that you expect, without exceeding your physical memory size. (And for obvious reasons, you cannot allocate more than about 2 GB of memory on a 32-bit system. For larger memory arenas you will have to use a 64-bit system.)

    For instance, use -w23 if you expect less than 8 million reachable states and can use 8 million bits of memory (i.e., 223 bits equals 8 million bits, which equals 220 bytes or 1 MB of RAM).

    A -w value lower than required for full coverage will give you a faster run, but less coverage. A value higher than needed, will give you a slower run, but it will also cover a larger fraction of the statespace.

  4. If the verifier finds an error, any error, it will write an error-trail into a file named spec.pml.trail, if spec.pml is the name of your Spin model. To inspect the trail, and examine the cause of the error, you can use Spin's guided simulation option -replay.
    For instance: 
    	$ spin -p -replay spec.pml
or
	$ spin -c -replay spec.pml
    Note that options to spin like -p and -c go before the -replay argument.
    If, however, a replay must be done with the executable verifier ./pan, which automatically happens for all models that contain embedded C code fragments in c_expr or c_code statements, then replay options to the executable verifier are placed after the -replay argument, for instance as in: spin -replay -P2 spec.pml. The executable verifier accepts different options for replay then spin itself, so it is good to keep these separate.
    Options placed after the -replay argument for a pure Promela model, and options placed before the -replay argument for a model with embedded C code, are politely ignored.

    Add as many extra or different options as you need to pin down the error. (Remember, you can check Spin's available options by executing: spin --, and options of the executable verifier with ./pan --.) One option is to convert the trail into a Tcl/Tk represetation of a message sequence chart of send and receive actions, which will then be displayed with the wish command (assuming wish is installed on your system): 
    	$ spin -M -replay spec.pml
    For more detailed tracebacks you can use, for instance: 
    	$ spin -r -s -l -g -replay spec.pml
    Make sure the file spec.pml didn't change since you generated the verifier. Spin will warn if you did.

    If you're not interested in the first error that is reported, add runtime option -c to select others: 

    	$ spin -search ... -c3 spec.html
    generates a counter-example trail for the third error found in the search. If you just want to count all errors and not see them, use 
    	$ spin -search ... -c0 spec.html
    By default, the argument to -c is 1.

    If you want to obtain a trail for each and every error found (usually not recommended, because there may be an overwhelming number of these), use: 

    	$ spin -search ... -c0 -e spec.html
    This creates a series of error trails in files numbers spec2.pml.trail, spec3.pml.trail, ...etc. To trace back a specific one of these trails, you can specify the specific trail file you want to see with a -k option: 
    	$ spin -k trailfilename -p -replay spec.pml

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: 
	$ spin -o3 -search -d spec.pml	# show optimized state machines
to print the optimized state machine assignments, as it is used during verification. (The -o3 argument turns off a default statement merging option that can sometimes make it harder to interpret the output.)
The unoptimized machine (used during random or guided simulations with spin -replay for instance) can also be printed, but you need the executable verifier for that. (It will exist if you've executed the above command first): 
	$ spin -o3 -search -d -d spec.pml	# show full, unoptimized state machines
These two options should also make it easier to understand and verify the working of Spin and pan in terms of the underlying automata theoretic foundation.

In very rare cases, when you need to debug the working of the verifier itself, you can also consider compiling the verifier with an additional compiler directive -DCHECK or -DVERBOSE.

Spin HomePage (Page Updated: 8 June 2014)