Spinroot

A forum for Spin users

You are not logged in.

#1 2013-06-27 19:19:09

robstewartuk
Member
Registered: 2013-01-04
Posts: 8

Verifying properties that may hold

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

#2 2013-06-29 04:39:50

spinroot
forum
Registered: 2010-11-18
Posts: 695
Website

Re: Verifying properties that may hold

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

#3 2013-06-29 15:48:21

robstewartuk
Member
Registered: 2013-01-04
Posts: 8

Re: Verifying properties that may hold

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

#4 2013-06-29 17:58:47

spinroot
forum
Registered: 2010-11-18
Posts: 695
Website

Re: Verifying properties that may hold

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

#5 2013-06-29 18:42:25

robstewartuk
Member
Registered: 2013-01-04
Posts: 8

Re: Verifying properties that may hold

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

#6 2013-06-29 18:59:34

spinroot
forum
Registered: 2010-11-18
Posts: 695
Website

Re: Verifying properties that may hold

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

Board footer

Powered by FluxBB