Using spin


Simulation mode

spin file.pml
allows us to run file.pml in simulation mode. The display output corresponds to the printf's in the code. Simulation can become an infinite loop, but if a blocking state is reached (there is no process with at least one executable statement) it will end printing "timeout". Similarly, if an assertion is violated, simulation ends showing the source code line of the violated property.

spin -u10000 file.pml
allows bounded execution for a maximum number 10000 state transitions. The limit N in -uN measures the overall number of state changes, not the instructions in a given process or loop.

spin -p file.pml
prints the complete trace of execution, and not only the printf standard output. It will show, at each transition, where did the execution place the program counter, that is, in which process and at which source code line number.

spin -i file.pml
allows interactive decision for non-deterministic choice points. Each time there is a non-deterministic decision, we can interactively choose which one we want to take, to force some execution path.

Verification of assertions and deadlocks

To check the absence of deadlocks and that assertions are always satisfied (in any execution path) use:
spin -a file.pml
gcc -o pan pan.c
pan

If pan informs about one or more errors, it will generate a new file called

file.pml.trail

with a counterexample execution (either leading to deadlock, or violating some assertion). To display the information in the counterexample, we should use

spin -t file.pml

Note that we do not include the extension .trail in this call, only the original source file. Usually, we will be interested in combining with -p to show the complete trace

spin -t -p file.pml

Verification of safety properties

We will use some LTL formula of the form []safe (we want that the program is always safe), where "safe" is some condition we are interested in. For instance, saying that two processes P and Q never reach a critical section we would write [](P@cs && Q@cs) where cs is an instruction label for each critical section. To check safety we use

spin -a -f '![]safe' file.pml
gcc -o pan -DSAFETY pan.c
pan

Note that we negate the formula to check using "!". Including the SAFETY flag when compiling "pan" is also recommendable.

When checking a safety property on a system that may lead to a deadlock, the verifier "pan" will primarily report about the deadlock problem, so that we will not actually know whether safety is satisfied. To disable the default deadlock check in pan we use the option

pan -E

In this way, if no errors are found, we know that the safety property is satisfied, although perhaps the system may reach a deadlock.

Verification of liveness/fairness properties

Checking that a process doesn't reach a state in which some part of its code (say, label cs) is never accessible can be done as follows

spin -a -f '!<>cs' file.pml
gcc -o pan pan.c
pan -a -f

Note that we disable flag SAFETY whereas pan usess flags "-a -f" to specify accepting conditions and weak fairness. This means that pan will look for counterexamples that are not finite executions, but loop insteads. When an error is reported, we use as before

spin -t -p file.pml

but this time the execution will show, at some point,

<<START OF CYCLE>>

meaning that the rest of transitions below actually form a cycle, not just a finite linear execution.

Sometimes, the cycle is too long. If we want "pan" to look for a short counterexample, we can use the options

pan -a -f -i

that use more resources in the search. We can use this once we know a counterexample (of any length) exists.

Similarly, checking that some program point cs is executed an infinite number of times can be done with

spin -a -f '![]<>cs' file.pml


Maintained by Pedro Cabalar. Last update Nov. 7, 2013