Spinroot

A forum for Spin users

You are not logged in.

#1 2020-07-13 10:12:23

TheAnyKey
Member
Registered: 2020-07-10
Posts: 2

Model resets of a process

I am modelling a sdafetycritical embedded system, where I having (simplified) a main core, which executes some functionality doing some persisting operations. And, further, I have a monitoring subsystem, that resets the main core, when it detects some critical conditions. Reset means that the execution in the main subsystem starts from the beginning and reset some not persisting variables, some other that model persistent states are keeping its values. These conditions that trigger a reset can also be externally, such that we cannot control when it happens and cannot prevent them by design. I want to verify that I designed the persisting operations and their order in a way that iregardless when the main core is reset, it can recover to a defined state.

I found two ways to do model that in spin, but both having some severe drawbacks. Maybe there is a better way.

One way is to to model after each persisting operation a non-deterministic decision to reset or not.
proctype sys_main{
    …
    V0=a;
    If
        :: true -> goto reset;
        :: true -> skip;
    Fi
    V1=b;
    If
        :: true -> goto reset;
        :: true -> skip;
    fi
    …
}
Of course I can make this with makros, but it would still require to model plenty of resets.

The second way is to use move the core function to an inline and call it form several processes, where each use the provided syntax to ensure that only one is active

inline sys_main(){…}
proctype sys_main_a provided (reset_cnt==0) {sys_main();}
proctype sys_main_b provided (reset_cnt==1) {sys_main();}
proctype sys_main_c provided (reset_cnt==2) {sys_main();}
proctype sys_main_d provided (reset_cnt==3) {sys_main();}
proctype sys_main_e provided (reset_cnt==4) {sys_main();}

As a further interruption is of course possible before the system has recovered completely, the relevant state space is larger and so we need to reason how many resets we need to handle. Overall this blows up the state space of the verification.

Is there a further way to model such a behaviour in spin that I missed?

Offline

#2 2020-07-13 17:35:55

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

Re: Model resets of a process

did you try using an 'unless' construct?
http://spinroot.com/spin/Man/unless.html

Offline

#3 2020-08-04 09:28:21

TheAnyKey
Member
Registered: 2020-07-10
Posts: 2

Re: Model resets of a process

Thanks for that hint. I modelled it now all three options. Not really surprisingly, the way with the explicitly modelled resets has significantly less states and thus the verification time is shorter. Although the way with the unless has less states than the way using proctypes.

Offline

Board footer

Powered by FluxBB