Spinroot

A forum for Spin users

You are not logged in.

#1 2012-04-20 13:28:25

Gordon
Member
Registered: 2011-07-12
Posts: 6

How to verify a simple safety property?

Hi,

I'am using spin version 6.1.0 on Windows and tried to verify a simple safety property. Therefore I run spin with the -a flag and compile the generated pan.c file with the switches -DBITSTATE -DSAFETY. When I run the verification of the example below, the result (if an counter example was found or not) depends on several settings.

- If the compile switch SAFETY is used or not
- if the variable 'r1' is at the global scope or in the scope of process 'all'
- the data type of the variable 'NR1' (bool or int)

I'am a bit confused about this. It seems to me that in some settings a full verifaction is not done although I run the verifier in this mode (I do not use any options when running the generated verifier).

Could you please have a look at my small piece of promela code and give me some hints what I'am doing wrong here?


Here is the promela code:


int REG_2;
hidden int TMP_VALUE;
byte MEMORY[2];
int NR1 = 0;
byte r1;

init
{
  atomic {
    run all();
  }
}

inline write() {
  select(r1: 0..255);
  MEMORY[0] = r1;

  select(r1: 0..255);
  MEMORY[1] = r1;
}


proctype all()
{
  write();
  d_step {
    TMP_VALUE = (MEMORY[0] << 8);
    TMP_VALUE = (TMP_VALUE | MEMORY[1]);
    REG_2 = TMP_VALUE;
  }
  write();
  if
    ::(REG_2 != 42) ->   goto BB0_2;
    ::else -> skip
  fi;

  NR1 = 1;

BB0_2:
    skip;
}

never {
    do
       ::skip
       ::NR1 == 1 -> break;
    od;
}

Offline

#2 2012-04-20 19:09:05

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

Re: How to verify a simple safety property?

you've defined a very large model -- most of the complexity comes from the two 'select' statements you use
i would proposa changing both to a much smaller range, e.g., select(r1: 0..8)
and then check to see if you can do an exhaustive verification (with or without bitstate)

Offline

#3 2012-04-23 08:11:25

Gordon
Member
Registered: 2011-07-12
Posts: 6

Re: How to verify a simple safety property?

Ok, thank you. I have reduced my example like you proposed (I compare with 7 then) and then the verification works with and without -DBITSTATE but I still have a question. Refering to my initial example:

How can the verification result depend on the complexity of the problem (assuming unlimited memory and time)? I have not limited the search depth or time (at least not explicitely) so I think I'am doing an exhaustive verification. I don't see any spin output indicating a limited search. Do I have to trigger an exhaustive search explictely or is it a feature of -DBITSTATE not to be exhaustive?

Offline

#4 2012-04-23 15:59:27

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

Re: How to verify a simple safety property?

the complexity of the problem is determined by the number of system states that
the verifier has to explore before reaching a verdict: more states = more complex
at some point there will be more states to store than you have memory available.
at that point you can switch to the bitstate mode, which is more approximate but
can substanially increas the nr of states that can be stored and explored...
you can read up more about all this in the papers, or in the textbooks on Spin

Offline

Board footer

Powered by FluxBB