SPIN Verifier's Roadmap: iSpin
SPIN VERIFIER's ROADMAP:
USING iSPIN
The easiest way to get started with Spin is to
use the graphical interface iSpin.
The graphical interface runs independently
from Spin itself, and helps by generating the proper
Spin commands based on menu selections.
iSpin runs Spin in the background to obtain the desired
output, and wherever possible it will attempt to generate
a graphical representation of such output.
iSpin knows when and how to compile code for the
model checkers that Spin can generate, and it knows
when and how to execute it, so there is less to remember.
For more information on running Spin directly,
see the companion document Roadmap.html.
This description assumes that the appropriate software
has been installed on your system and that all
relevant commands (such as wish, Spin, iSpin, and a
C compiler such as gcc) are within your search path.
If this is not the case, check the README
file first.
One
To start a first session with iSpin,
use one of the example Promela specifications
from the Test directory of the Spin distribution.
For instance:
$ ispin leader.pml
The dollar above is the prompt of the command-shell.
The next two words are typed by the user.
If all is well, after ispin starts up it will print something
like the following in its command-log at the bottom of the
main window:
SPIN LOG:
Spin Version 6.0.0 -- 3 December 2010
iSpin Version 1.0.0 -- 3 December 2010
TclTk Version 8.5/8.5
1 leader.pml:1
All further commands executed in the background, prompted by
user selections in the other windows, will appear here as well.
Two
You should now have the main Spin control window on the
display, with a Promela specification of the leader election
protocol loaded.
First, press the Help.. button in the top menu bar
to view the available help topics. Select one of the topics, and
simply close the window when done.
The main text window on the left offers some basic
edit and search capabilities. You can scroll through the
specification either with button-2 down (on a 3-button mouse),
or with the scroll-bar.
You can select text fragments by sweeping the mouse with
button-1 (the left-most button) down. Control-C (copy),
Control-V (past), and Control-Z (undo) are supported.
If you are more comfortable working with another text-editor,
a reasonable way of working with iSpin is also to have the text
of a specification open in your favorite editor; to update
the file being edited explicitly after changes; and then to
select ReOpen from the top menu bar to read in the new version.
Three
Still within this first view, you can perform a basic Syntax check,
and a basic check for Redundancies, by selecting the corresponding
buttons near the top of the screen. You can also get the symbol
table of the Promela spec printed out in the same way.
The Automata View panel on the right hand side of the screen relies
on the availability of the dot tool from the graphviz distribution.
If you have it installed, clicking on the automata view button can
display each proctype as a graph.
Next, move to the Simulate/Replay tab, where you can select
simulation parameters for a simulation run.
For now, just accept the default settings that are
shown, and press the Run button, to perform a
first simulation run.
Four
A Message Sequence Chart will be created in the right panel
(assuming your model includes message passing operations of course).
The lower panels, labeled Data Values and Queues
maintain the current values of all variables and channels used
during the simulation run.
For very large models, you may want to turn off data value tracking,
if it starts slowing down a simulation run.
The simulation output appears in the middle panel at the bottom.
Once a run is completed, or stopped, you can use the Rewind button
to go back to the start of the run, and step forwards or backwards
through it -- with all values and queue states updated appropriately.
You can also click in the message sequence chart or the output panel
to move to a specific point in the run.
Five
Note that a log window at the upper right shows precisely which
commands are generated by iSpin to let the main Spin tool perform
the desired simulation. For instance:
spin -X -p -v -g -l -s -r -n1 -j0 leader.pml
The advantage of using iSpin is that you
do not have to remember the meaning of all the options that
Spin recognizes. (Not all the the options used above are
critical though, so there's also not need for great concern
about using Spin without this interface. You can find out
what all the option flags to Spin mean by typing in a regular
shell window: "spin --".)
Six
By clicking in the boxes in the Message
Sequence Chart displayed on the right the text
window on the left should move to the corresponding points in the code.
Simularly, clicking on any filename:linenumber reference should bring
up the corresponding file, positioned at the linenumber given.
Seven
Next, move to the Verification tab.
There are again lots of choices that can be made about the type of verification
that can be done. The most common choices are on the left side in light blue.
The less frequently used, more advanced options are to the right in grey.
Accept the default settings of the parameters and press the Run button.
The commands that iSpin generates are printed in the log, which is now
in the right-hand side panel.
Spin first generates a verifier, then compiles and executes it, and
shows the results. If all is well, the results show
that there are no errors detected in the specification.
The version of the leader election protocol that is being verified
contains several correctness requirements specified as inline LTL formula.
By default, only a safety verification is performed. To check one of the
LTL properties select Liveness acceptance cycles and provide the name of
the ltl claim to be verified in the box just above the Run button,
for instance property p0 or p1.
Eight
Introduce an artificial error in the specification by adding an
assert(false);
statement (don't forget the semi-colon)
immediately following either one of the occurrences of:
:: Active ->
becomes:
:: Active -> assert(false);
Save the file (you have to move to the Edit/View panel to do that),
and repeat the verification run.
This time, the verification should come back with an error
sequence, and notice at the bottom of the output window recommends
to replay the error trail from the Simulate/Replay panel.
Bring up that tab and make sure a Guided simulation is selected.
(A guided simulation can only be done for an error sequence
that was produced earlier by the verifier.)
Perform the guided simulation, which will now replay the error sequence
found, ending in the assertion violation.
Nine
Bring up the Swarm Run panel. If you have swarm installed
(if not, see http://spinroot.com/swarm) you can now easily setup
a swarm run, using as many CPU cores as you have available.
(This option will become more attractive as standard PCs start
getting more and more CPU cores.) Don't select more cores than you
actually have on your system and don't select more memory than you
actually have. The options in the top right-panel show how Spin
will compile the verifier to create lots of different types of
verification runs. This method is especially useful for very
large verification models that cannot be exhaustively verified,
but where we still want to gain maximum confidence that we can
find the errors.
Ten
The final two tabs are to save or restore an entire verification
session, including all options selects and intermediate results
created. Useful to remember what precisely you did and how you
found counter-examples. It provides a small approximation of a
version management system for Spin verification runs.