Model Car Security: FAST Encoding




Three integer variables are used: s as speed for the speed, t as time for the seconds and d as distance for the estimated distance that the model car travels after loosing its track.
Four states are used to model the car. State one is the normal state. Two basic transitions can occur, t1 and t2. Transition t1 is fired when a wheel movement is detected. The distance is increased and so is the current estimated speed. Transition t2 is fired by a timer. The time t is increased and the estimated speed is reset.
State Two is the error state. It is reached from State One when the distance d is greater than 9: the security limit is broken.
State Three and State Four are final states reached safely by the car. State Three is reached when the speed s exceeds its limit. State Four is reached when the elapsed time is to large.
These numerical constants could be changed, but have to be known numerically at analysis time to keep the invariants in the affine relationship set.


model voiture {

var t, s, d;

states one,two,three,four;

transition t1 := {
 from   := one;
 to     := one;
 guard  := s<=1 && d<=8;
 action := s'=s+1,d'=d+1;
};

transition t2 := {
 from   := one;
 to     := one;
 guard  := t<=2;
 action := s'=0, t'=t+1;
};

transition t3 := {
 from   := one;
 to     := two;
 guard  := d>=9;
 action := s'=s+1, d'=d+1;
};

transition t4 := {
 from   := one;
 to     := three;
 guard  := s>=2;
 action := s'=s+1, d'=d+1;
};

transition t5 := {
 from   := one;
 to     := four;
 guard  := t>=3;
 action := t'=t+1, d'=d+1;
};

}

strategy s1 {

Region init := {state=one && t=0 && s=0 && d=0};



Region bad := {state=two};
}