SPIN Verifier's Roadmap: Xspin
SPIN VERIFIER's ROADMAP:
USING XSPIN
(updated for Spin/Xspin version 3.1.2)
The easiest way to get started with Spin is to
use the graphical interface Xspin.
The graphical interface runs independently
from Spin itself, and helps by generating the proper
Spin commands based on menu selections.
Xspin runs Spin in the background to obtain the desired
output, and wherever possible it will attempt to generate
a graphical representation of such output.
Xspin 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, Xspin, and an
ANSI-C compiler) are within your search path.
(If this is not the case, see the README
file first.)
One
To start a first session with Xspin,
use one of the example Promela specifications
from the Test directory of the Spin distribution.
For instance:
$ xspin leader
xspin: Spin Version 3.1.2 -- 14 March 1998
xspin: Xspin Version 3.1.2 -- 14 March 1998
xspin: TclTk Version 7.6/4.2
xspin: removing tmp files..
xspin: done..
xspin: .open leader.
. . .
The dollar above is the prompt of the command-shell.
The next two words are typed by the user.
The remainder (in regular font) is printed by Xspin onto
the stdout stream, as it starts up.
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 to view the available
help topics. Select one of the topics, and press Ok
when done, to return to the main window.
The main text window that you see offers some rudimentary
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. Use the Edit menu for
standard Copy, Cut, and Paste operations.
If you are more comfortable working with another text-editor,
a typical way of working with Xspin 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 File menu before
simulation or verification runs are performed.
Three
Next, press the Run.. button and then
select Set Simulation Parameters...
For now, just accept the default settings that are
shown, and press the Start button, to start a
first simulation run.
Four
A number of new windows appear.
The large panel to the right, labeled Message Sequence Chart
is empty at first, but it will display all messages sent and
received during the simulation that we are about to start.
The lower panel, labeled Variable Values, will print
the current values of all variables and channels that are used
during the simulation run.
The main panel that appears is labeled Simulation Output. It allows
you to perform either a single-step simulation, or a continuous random
simulation run. Choose the latter, by pressing the Run button.
Let the run proceed until completion.
The main panel will show the raw printout from Spin (which is running in the
background to perform the actual simulation), prefixed by a step-number
in the left margin.
Five
When the run completes, the main panel will print the number of processes
that has been created.
Note that the log window, at the bottom of the main text panel
now contains the lines:
xspin: .starting simulation.
xspin: spin -X -p -v -g -l -s -r -n1 -j0 pan_in
xspin: .at end of run.
It shows the commandd that Xspin synthesized to perform the
simulation run with the parameters that were selected.
The advantage of using Xspin is clearly 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
Make the main Spin control window that displays the Promela
text of the leader election protocol visible again (without closing any
of the panels that have been created for the simulation so far).
Move the mouse cursor over the boxes and arrows in the Message
Sequence Chart display on the right.
You will see that the main text window tracks the
movements of the mouse. When the mouse cursor is over a square box
in the message sequence chart, the corresponding Promela source line in
the text window is indicated, and the source text is shown in the
sequence chart.
The number that is shown in the square boxes if the mouse is not
hovering over them is a simulation step number, that matches the
numbers in the left margin of the Simulation Output panel.
Try the same experiment with the yellow rectangles in the message
sequence chart, and notice how their display in the message sequence
chart chart is triggered in the Promela source (i.e., a printf
statement that starts with the letters MSC:).
Seven
Make the Simulation Output panel visible again (it's likely
hidden behind the main Spin control panel now),
and press Cancel.
This removes all new panels that were generated.
The next time you press the Run.. button there will be an
extra selectable option, to repeat a simulation with the same
setting as you last selected. We'll skip that for now.
Next, select the Set Verification Parameters option
from the Run.. menu. Accept the default
settings of the parameters and press the Run button.
Notice again the commands that Xspin synthesizes, printed in the log.
This time, Spin is asked to generate a
verifier, the verifier is compiled and executed, and the results
are fed back to Xspin for display. If all is well, the results show
that there are no errors detected in the specification.
If in the verification run, Spin detects that some statements are
unreachable for the given parameters, those statements are highlighted
in the main Xspin control window with the text of the specification.
(The version of the leader election protocol that is being verified
contains a correctness requirement that was specified as the LTL
formula (<>[]oneLeader) in a separate file called leader.ltl
We'll return to this below to show how this is used.)
Close the verification output window.
Eight
Introduce an artificial error in the specification by adding an
assert(false);
statement (don't forget the semi-colon), for instance,
immediately following either one of the occurrences of:
:: Active ->
becomes:
:: Active -> assert(0);
Now repeat the verification run. (There is no need to save
the file. Xspin always works with the copy of the
specification that sits in its edit buffer.)
This time, the verification should come back with an error
sequence, and a small panel will ask you to either repeat
the run with different parameter settings, or to perform a
guided simulation.
Choose the Guided Simulation option.
This now returns you to a simulation parameters panel,
but one of the options has now been changed from what you
saw before: Xspin has preselected a Guided Simulation
instead of a Random Simulation.
(A guided simulation can only be done for an error sequence
that was produced earlier by the verifier.)
Nine
Select the Execution Bar Panel and change the
sub-option in the Time Sequence Panel to
One Window per Process, to
change the view on the simulation run a little from before.
Press the Start button in the parameters panel, and
then the Run button in the Simulation Output
window, to inspect the error trail.
This time, the trail ends at the assertion violation and not
in a state where all processes have reached the end of their
code. (You can in principle step either backwards or forwards
through the simulation trail, but the update of the displays
is not always intuitive, so defer playing with those options
for now.)
Ten
When done, close all the panels again (pressing Cancel
in the Simulation Output panel will clear up most of
them).
Next, select the LTL Property Manage.. option from the
Run menu .
By default this will read in a file with extension .ltl,
with the same name as the main specification: in this case it
should open leader.ltl and load the information from
within that file. You can also enter a different formula.
Let's try that first. Hit the Clear button and enter
in the Formula entry box the formula:
[] p
This formula expresses that the boolean condition that is
represented by the propositional symbol p is
invariantly true. Either this is an error or this is
the desired system behavior. In this first case,
the option This Property holds for All Execitions applies.
In the second case, the opposite choice This Property
holds for No Executions applies.
Either press the Generate button, or type a carriage
return in the Formula entry box.
The larger text window should now display the automaton
(a never claim in Promela terminology) that corresponds
to the LTL formula (either negated or not, depending on the
choice for the type of property made above).
In the symbol definition box a query will come up for the definition
of the propositional symbol p. (If you don't see it right
away, try the scroll bar. For safety, old definitions are not
removed from this panel on hitting the Clear button.)
Eleven
Adding the definition of the propositional symbol p,
is done with a standard macro definition, for instance as follows:
#define p (nr_leaders == 0 || nr_leaders == 1)
This definition is entered into the Symbol Definitions box
(check the top of the specification of the leader election
protocol for some other macro definitions of this type).
If you forget the macro definitions for the propositional
symbols, Spin will complain about syntax errors (undefined
identifiers) when it tries to parse the never claim
refers to these symbols.
Run the verification and see what happens. When done, revert to
the original never claim (reload it from the leader.ltl file) and
repeat a verification.