Using spin
Installation
Alternative instructions for installing
spin in ubuntu.
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
|