| |
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.
-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 -x spec.pml
If, on the other hand, you don't feel very inquisitive and just want
to get a quick basic verification run going, use this command,
which will compile and run your verification immediately:
$ spin -run 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 -run -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 -run -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 -run -O2 -DMEMLIM=256 -DCOLLAPSE spec.pml # use compression
or, for a still more aggressive option, try:
$ spin -run -O2 -DMEMLIM=256 -DHC4 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 -run -O2 -DBITSTATE 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:
- Selecting the type of property to be verified (safety or liveness)
- Selecting the maximum search depth,
- If you use a Bitstate search: selecting the size of the hash-table
- Selecting the parameters for a replay of an error, if one is found.
We'll now explore each of these decisions in more detail.
-
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 -DSAFETY directive:
$ spin -run -DSAFETY spec.pml
plus of course any of the other arguments we discussed earlier, for instance:
$ spin -run -O2 -DBITSTATE -DSAFETY 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 -run -DBFS 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 -run argument
to Spin. For instance:
$ spin -run -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 directive -DNP and
run-time option -l, for instance as in:
$ spin -run -DNP -l spec.pml
plus any other runtime arguments you selected.
-
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 -run -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 -run -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 -DREACH argument,
and a runtime parameter -i to force a search for a short error.
For instance, to search for errors shorter than 100 steps:
$ spin -run O2 -DREACH -i -m100 spec.pml # iterative search for short errors
-
If you perform a Bitstate
verification (i.e., you used directive -DBITSTATE), 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.
-
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 -t (provided that
there are no embedded C code fragments in your model.
In that case you should use the verify replay script explained
here.
For instance:
$ spin -t -p spec.pml
or
$ spin -t -c spec.pml
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 --.)
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 -t -M spec.pml
For more detailed tracebacks you can use, for instance:
$ spin -t -r -s -l -g 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 -run ... -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 -run ... -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 -run ... -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 -t -k trailfilename -p 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 -run -d spec.pml # show optimized 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, but you need the executable
verifier for that. (It will exist if you've executed the above command
first):
$ spin -o3 -run -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.
| |