Download Formal Methods for System Development

Chapter 4. Spin introduction and tutorial
Whenever possible, deterministic sequences in processes should be enclosed in a d_step declaration. This helps the partial order reduction technique. A caveat with d_step as opposed to atomic is that no statements
except the first may block, else the determinism is broken.
A tip for reducing the number of processes is to drop the init process.
The init process is really just an active process that is started first. Any
processes may be started from an other active process, so by moving the
run-statements from the init process we reduce the state vector by four
bytes. Note that a more powerful pre-processor such as m4 enables us to
programmatically create processes with arguments as active processes.
Optionally Spin has several optimisations built-in. These are enabled
or disabled with compiler flags. Generally the optimisations are directed
towards memory usage, and will increase verification time. Optimisations
include state vector collapse compression (-DCOLLAPSE) and state vector
coding as minimised deterministic automaton (-DMA=n). Many optimisations
may be combined, but the benefits are highly problem specific.
The reference manual [14] and Theo Ruys’ Ph.D. thesis [22] provide
information on more advanced optimisations.
4.3
Semaphores—deadlocks and temporal claims
We start with modelling semaphores. Semaphores are common and their
usage error prone. In short, they are a very good candidate for verification.
The examples have been taken from The Little Book of Semaphores [8], with
the exception of the last one which is from [4].
4.3.1
Busy waiting, weak and strong semaphores
Busy waiting resembles the wait()/notifyAll() pattern from Java. Strong
semaphores have an associated queue. This queue is modelled using an
asynchronous channel. Waiting on a weak semaphore does not preserve
order. All a weak semaphore guarantees is that some waiting process will
be awaken at a signal-operation.
The naı̈ve model of a busy waiting semaphore is
wait:
if
:: atomic { sem > 0; sem-- }
:: else -> goto wait
fi
However, this will make the model actually loop, which is not needed.
A better model, that uses the fact that a Promela process is blocked until a
statement is executable, removes the loop. The wait-operation will then be
36