Spinroot

A forum for Spin users

You are not logged in.

#1 2016-06-01 13:51:03

Schachtschabel
Member
Registered: 2015-08-28
Posts: 15

Detecting a counter-overflow with Spin

Greetings to all,

this time, I have a rather explicit problem with the following model scenario:
Consider a software routine that reads in a clock signal and takes action once a positive flank was registered (incrementing an arbitrary variable in this simple case). Additionally, there is a counter running that is able to detect a static clock signal after a short time. Once this counter runs over multiple times, the routine reports a failure in the underlying hardware and quits.
The model code is strongly based on the real software and currently looks like this: 

bool hw_clock_fail = true;
bit hw_clock = 0;

inline clk_update () 
{
	if
	:: hw_clock_fail -> hw_clock = hw_clock;
	:: else -> hw_clock =  (hw_clock + 1)%2;
	fi;
}

active proctype A () 
{
	chan ret = [0] of  {int};
	int errorcount;
	int status;

	do
	:: (errorcount<2000) ->
		run B(ret);
		ret?status;
		if
		:: (status==1) -> break;
		:: else -> errorcount = errorcount + 1;
		fi;
	:: else -> assert(false); //HW failure occured! 
	od;
}

proctype B ( chan callback )
{
	int time;
	int i;
	bit old_flank;
	bit new_flank;

	do
	:: ((time<5000) && (i<100)) -> 
		clk_update();
		new_flank = hw_clock;
		if
		:: (new_flank != old_flank) && (new_flank != 0) ->
			new_flank = old_flank;
			i = i + 1;
		:: else -> skip;
		fi;
		time = time + 1; 
	:: else -> break;
	od;

	if 
	:: time == 5000 -> callback!0;
	:: else -> callback!1;
	fi;
}	

The boolean variable "hw_clock_fail" is hereby indicating the presence of a clock failure and is set manually. Once I want to see if the routine is really able to detect the named error and set the variable to "true", the verification folds up a state space of 60.000.000 states due to the high threshold values "a" and "time".  I can see that this was to be expected, since every single value of these variables has to be tracked by the model checker to cover the entire state space; however, these upper bounds of those two variables are not that high in terms of software running on an embedded system.
To really be able to talk about the underlying software, I want to stick to the routines that were used there; on the other side, I cannot work with such a state space for such a small model.

Is there a way to either configure Spin or to alter the model in such a way that the main aspects of the software are still present and the verification comes to the correct result without having to deal with the entire depth of the state space?  Or is this just a type of problem that cannot be covered by model checking techniques like this?

So long,
Max

Last edited by Schachtschabel (2016-06-01 13:51:45)

Offline

#2 2016-06-02 03:22:27

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

Re: Detecting a counter-overflow with Spin

the only way i see would be to use abstraction techniques -- that would lead to a version of the model though that is not identical to the code anymore, but equivalent to it with respect to the property you're trying to verify.
that is a standard approach in verification (and in mathematics), so i'm afraid that there's no way around that
(maybe at some point the tools can figure out these types of abstractions mechanically, but that's not the case yet)

Offline

#3 2016-06-02 07:55:03

Schachtschabel
Member
Registered: 2015-08-28
Posts: 15

Re: Detecting a counter-overflow with Spin

I was afraid so.
I am now wondering what kind of (manual) abstraction can be used here to reduce the state space? I can't think of any way besides reducing the threshold values of the named iteration variables. Do you have any ideas regarding this specific example?
In the end, I want to try to find a way of abstracting this scenario that can also be used on similar cases. You could say, I am looking for an abstract abstraction big_smile

- Max

Offline

Board footer

Powered by FluxBB