A forum for Spin users
You are not logged in.
Pages: 1
I am not understanding the liveness verification in Section 4.3.2 of "The Model Checker SPIN" [1], It shows two properties that are verifiable. The first states "We would like to verify two properties. The first: a message can be lost. Violations of this requirement can be expressed in the formula:"
![](sr -> [] rr)
How many negations are there? There is one in the formula (!), and the generated never claim. I am struggling to understand:
* What this is proving. Is it stating:
** Sometimes a message is lost, and sometime it arrives?
** It is not true that always a message arrives? i.e. "The SPIN model checker verifies that it is not true that a message always arrives".
* Running the SPIN model checker on this property, is it verified if the verifier states:
** "pan:1: end state in claim reached (at..."
** "State-vector XXX byte, depth reached YYY, errors: 0"
Lastly, Section 4.3.2 doesn't describe the verification environment. While it does say that it is checking for liveness properties, it doesn't mention whether or not it is checking for non-progresss cycles or acceptance cycles (or whether weak fairness is enforced).
In an unrelated point - are there any visualisers freely available, that produce Buchi automata illustrations for LTL formula? e.g. Figure 4 of [1].
[1] - http://spinroot.com/gerard/pdf/inprint/ieee97.pdf
Last edited by robstewartuk (2013-06-27 19:59:02)
Offline
There is one negation only. The positive requirement is: [] (sr -> <> rr) so violations are then expressed as the same formula with a single negation sign in front of it. This is what is converted into a never claim.
If you specify this in the current version of Spin with an inline ltl property, you can leave off the negation -- it is added by default in that case. But if you generate the never claim yourself from the ltl formula given, then you have to also manually add that negation.
What spin will prove is that the positive requirement can be violated, by showing that the negated requirement can be satisfied. I know, it takes a bit of mental contortion to get this, but it is pretty straightforward (after a while :-)
The verification environment for this property is given in Figure 11, at the top of the same page.
When verifying a never claim (derived from an ltl formula) you always check for acceptance conditions, not non-progress cycles. And finally, enforcing weak fairness isn't necessary in this case.
There are lots of tools out there for producing nice graphs from automata/state machine descriptions. I often use graphviz.
Offline
Thank you.
I have a follow up question with respect to "What spin will prove is that the positive requirement can be violated, by showing that the negated requirement can be satisfied". Below is an example, a simple verification attempt based on '[] (sr -> <> rr)'. When you wanted to verify that messages may be lost, I want to verify that the boolean 'dead' may be true.
bool dead;
active proctype Foo(){
dead = false;
do
:: dead = true -> skip;
:: skip ->
progess: skip ;
od
}
#define alive ( !dead )
never { /* ! [] alive */
T0_init:
do
:: atomic { (! ((alive))) -> assert(!(! ((alive)))) }
:: (1) -> goto T0_init
od;
accept_all:
skip
}
My positive requirement is that the alive symbol is always true i.e. '[] alive' therefore dead always false, which is intuitively not verifiable. "What spin will prove is that the positive requirement can be violated, by showing that the negated requirement can be satisfied." So, I try and verify the negated claim '! [] alive'. When I attempt to validate this never claim, however, I cannot.
verification result:
spin -a test_negation.pml
gcc -DMEMLIM=1024 -O2 -DXUSAFE -w -o pan pan.c
./pan -m10000 -a -N never_0
Pid: 2039
warning: only one claim defined, -N ignored
warning: for p.o. reduction to be valid the never claim must be stutter-invariant
(never claims generated from LTL formulae are stutter-invariant)
pan:1: assertion violated !( !( !(dead))) (at depth 4)
pan: wrote test_negation.pml.trail
(Spin Version 6.2.5 -- 3 May 2013)
Warning: Search not completed
+ Partial Order Reduction
Full statespace search for:
never claim + (never_0)
assertion violations + (if within scope of claim)
acceptance cycles + (fairness disabled)
invalid end states - (disabled by never claim)
State-vector 28 byte, depth reached 4, errors: 1
3 states, stored
0 states, matched
3 transitions (= stored+matched)
0 atomic steps
hash conflicts: 0 (resolved)
Stats on memory usage (in Megabytes):
0.000 equivalent memory usage for states (stored*(State-vector + overhead))
0.291 actual memory usage for states
128.000 memory used for hash table (-w24)
0.534 memory used for DFS stack (-m10000)
128.730 total actual memory usage
This doesn't seem to follow with the description from Section 4.3.2 of "The Model Checker SPIN". I must still be missing something?
Offline
Think of the never claim as expressing behavior that should never occur.
If Spin can find an execution that matches the behavior anyway, it will report it.
Your example claim is: ![] alive -- which, with the macro definition given, really says ![]!dead
That implies that your requirement is that the property []!dead cannot be violated.
But, it can, and Spin shows that.
Offline
Perhaps it is better to state a property that I *do* want to verify with SPIN. I have revised my model:
bool alive;
active proctype Foo(){
alive = true;
do
:: alive = false -> skip;
:: skip ->
progess: skip ;
od
}
In my revised model, one can intuitively see that execution may switch 'alive' to be false. However, 'alive' may also be true forever. The key statement I would like to make is: "in SOME executions, 'alive' may be switched to false.".. or more succinctly " 'alive' may not always be forever true ". Is there an LTL formula that could be used with SPIN to verify this?
Offline
To prove that something *can* happen, you should claim that it cannot, and Spin will show the opposite (i.e., that it *can*).
To prove that "in *some* executions x, you're looking for *at least one example of an execution where x", so claim that it cannot exist, and spin will prove you wrong.
So to prove that "[] alive" is *not* an invariant, claim that it is, and you will get the counter-example you're looking for.
Offline
Pages: 1