Spinroot

A forum for Spin users

You are not logged in.

#1 2015-09-18 13:12:52

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

Verification with infinite loops

Greetings again,

while I was busy continuing the modelling and verification of a small software project, I came across an issue regarding the handling of infinite loops and the way SPIN analyses them during a verification run:

Imagine there is an active proctype within a model that simulates an Interrupt service routine which is called by an overflowing hardware timer. This process looks pretty simple in Promela:

active proctype p_SysTick_Handler()
{
     do
     :: true -> c_code { now.countslices++; };
     od;
}

This endless loop should indicate that this global timer (which is used by a small process scheduler) could be incremented at any time during execution. Without the timer changing, the scheduler will not call any more processes and the whole program halts.
In reality, the timer would just be incremented sporadically in between the other software process, while they continue or wait for the next time slice . This is the behaviour i would like to apply to the model, since the way it is now the following issue occurs: If I now want to test for certain properties or accepting states of the rest of the code, this routine is always taken as a counterexample for basically any test, since in the model, this timer can be incremented infinitely often without any progress in the rest of the code. On the contrary, it is also possible that this routine is not called at all and the scheduler loops in an endless idle circle, which should also be excluded in my model.

I tried to filter these possibilities with LTL-formulas that indicate a limit on the timer increments until some progress is made, without success since all SPIN does is find me more counterexamples of my desired behaviour.
I know that SPIN is not designed to verify time-dependant systems, but I still think that this example can work when done right.
Maybe some of you have some ideas on this case.   

If someones wishes to see the whole code, I can post it in here, but I think this would be overcomplicating things; all that is relevant here now is the timer routine that runs in parallel to several other processes.

Thanks in advance for any feedback,
and so long,
Max

Last edited by Schachtschabel (2015-09-18 13:18:33)

Offline

#2 2015-09-18 15:56:07

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

Re: Verification with infinite loops

The best way to handle this type of situation is to use progress labels, and then to search for non-progress cycles.
So, incrementing the counter could be considered a progress event, and perhaps iterating the idle cycle.
Now non-progress cycles will be infinite behaviors that do not include either of these, etc.
You can also use never claims to look more specifically for behavior of interest, or indeed ltl formula.

Offline

#3 2015-09-21 09:03:32

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

Re: Verification with infinite loops

Yes, I thought about using progress labels, too.
But I haven't found a clever way yet to apply these in my scenario. When I tell SPIN that incrementing the timer means progress, I tell it that incrementing it over and over again without doing anything else is a good thing. What I like to do is quite the opposite, meaning that a series of increments means no progress.
In fact, this would mean that every transition aside the incrementation means progress, so I would have to label every line of code within the model. And even then, the verifier would just report that there are indeed non-progress cycles, namely the endless increments of the timer, which I am aware of, but I don't want to include this in the further verification.
That is also the reason why the never claims or the ltl forumla couldn't help me in this cause, since all formulas that I can think of just imply what 'should' be true within the model, and not what 'is'. So I have to look for a way to change my model regarding these characteristics.

Offline

#4 2015-09-21 16:49:20

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

Re: Verification with infinite loops

The progress label is just a way to tell the verifier not to bother you with reporting cycles that you already know about, and that are not of interest.
So if you place a progress label in the timer process, you do that in this case primarily to instruct the verifier not to consider it an error if the timer ticks independently forever.
It does mean that you get non-progress cycles that do not contain any clock-ticks -- but that is likely what you want to see.

Offline

Board footer

Powered by FluxBB