| << Chapter < Page | Chapter >> Page > |
Certainly this run-time check is helpful, but what about the promise of checkingwhether an assertion can fail? We will need to use SPIN as a verifier , rather than just a simulator .
As with simulation, before our first verification, we need to specify some parameters, even if only using the defaults.From the "Run" menu, select the "Set Verification Parameters" options.For this example, make sure that the "Assertions" option is marked. Use the "Run" button to start the verification.
spin by hand involves three steps:
we must first create a verifier (a C program) from our promela source;then compile the verifier, and then run the verifier:
prompt>spin -a
filename .pml
prompt>gcc pan.c -o
filename prompt>
filename The
-a flag tells SPIN to generate
a verifier, which it always names
pan.c .As desired, the verification finds a problem, as reported in
the "Verification Output" window.It also saves a description of the example run found where the
assertion fails.
pan: assertion violated (z==(old_z+1)) (at depth 11)
pan: wrote pan_in.trail The remainder of this window's output is not too important, as it
describes which verification options were used and how much workwas done in the verification.
pan is the standard SPIN
default name for files related to Promela verification.With
xspin , you'll see these
filenames reported, but you don't need to use or remember them.Now we can have SPIN show us the sample failed run it found. In the new "Suggested Action" window, select"Run Guided Simulation". This brings up the now-familiar simulation windows, which will show this particular run. This run is"guided" by a trace saved by the verification. (Alternatively, selecting "Setup Guided Simulation" allows youto change the display options first.)
-t flag to have SPIN use the pre-named trail file.
It's often handy to use the
-p flag to
have SPIN print each line it executes:
prompt>spin -t -p
filename .pml The trace found in our verification executed some of each thread.From our experience with this program, we know there are less complicated traces where the assertion fails. How can wefind them?
Again, in the "Run" menu, select "Set Verification Parameters". Now, select "Set Advanced Options", then"Find Shortest Trail", and "Set". Then run the verification again.
pan: assertion violated (z==(old_z+1)) (at depth 11)
pan: wrote pan_in.trailpan: reducing search depth to 10
pan: wrote pan_in.trailpan: reducing search depth to 5
new_z and
old_z for each process, respectively.
For the assertions, the relevant variables are underlined.
Notification Switch
Would you like to follow the 'Model checking concurrent programs' conversation and receive update notifications?
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|