| << Chapter < Page | Chapter >> Page > |
To verify with this formula is a two-step process. First, using the "Generate" button generates what is known as a never claim , shown in the window. This is more Promela code that is temporarilyadded to your program. This creates a special process that checks the LTL formula and isguaranteed to be executed after every normal step of your code. You don't need to understand the generated never claim, althoughSPIN presents it for advanced users. The never claim uses a couple syntactic features of Promela not covered in this module.Next, using the "Run Verification" button opens a small version of the verification options window that we're already familiar with.Running the verification puts any output in the LTL window.
never claim using
spin -f
formula .
For example,
prompt>spin -f '[] (p -><>(q || !r))' Be sure to quote the formula so the shell doesn't try to
interpret special characters.Next, take the output (which is Promela code for
a
never claim),
and paste it at the end of your Promela source file.Also add
#define s to the top of your file,
defining each propositional variable used in your LTL formula.Finally, verify the resulting code.Generate and verify the code from the previous example .
The automatically-generated
never claim is shown below.
It uses labels and
goto s which we haven't discussed,
but which will be familiar to many programmers.(This code represents a small automaton, in this case with
two states, which gets incorporated into the largerstate space automaton that we've described.)
The use of the constant
1 here
is equivalent to the more mnemonic
true .
never { /* !([]p) */T0_init:
if:: (! ((p))) ->goto accept_all
:: (1) ->goto T0_init
fi;accept_all
skip}
Running the verification, it does not report any errors.
However, note that verifying an LTL property automaticallyturns off deadlock checking:
Full statespace search for:invalid end states - (disabled by never claim) However, it still reports a
warning that the process never exits, in case we care:
unreached in proctype loop
line 27, "pan.___", state 11, "-end-"(1 of 11 states)
We want to accomplish the same goal as the previous example , but with a formula that should never hold. What's an appropriate formula?
Using the same definition of
p ,
we can simply use
<>!p .
p is false.
Now let's verify something that can't be done easily with just
assertions. We also want to make sure that
num_crit continually alternates between the values of 0 and 1, rather than
maintaining the same value. How can we do this?
Use the following symbol definitions:
#define p (num_crit == 0)
#define q (num_crit == 1) and verify that
([]<>p)&&([]<>q) always holds.
How could we use LTL to verify whether no process is starved? Of course, this verification should fail, generating a trailwhere at least one process is in fact starved.
In essence, we want to verify
([]<>(_pid == 0))&&([]<>(_pid == 1))&&([]<>(_pid == 2)) The problem is that
_pid is a local variable to each process,
but, unfortunately,
never claims are their own separate process,
and can't access those variables.One solution is to create an equivalent global variable:
pid running;
Inside the critical section code add the line
running = _pid; Use the following symbol definitions:
#define p (running == 0)
#define q (running == 1)#define r (running == 2) and verify whether
([]<>p)&&([]<>q)&&([]<>r) always holds.
active proctype .
So, in this case, its PID is 3.As expected, the verification fails, and a trail file is created. In the author's sample verification, thistrail has only processes 0 and 1 entering the critical section, although there are many possiblecounter-examples.
It turns out, SPIN has a special syntax to express
whether a certain process is at a certain label.So instead of defining a new variable,
we could alternately go to the critical sectionand add a new label (say ``
crit: '')
and then define:
#define p (loop[0]@crit) /* 0th 'loop' process is at crit. */#define q (loop[1]@crit) /* 1st 'loop' process is at crit. */#define r (loop[2]@crit) /* 2nd 'loop' process is at crit. */
Notification Switch
Would you like to follow the 'Model checking concurrent programs' conversation and receive update notifications?
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|