Automating Verification of Cooperation, Control, and Design in Traffic Applications - Formal Methods and Hybrid Real-Time Systems - page 125

2

1

move

ev_drive{d_c:=1;}/v_d:ml.req_speed(p);,

slope:=ml.req_slope(p);

[o_v_d~=v_d]/c_v_d:=0;

change switch

init/
entry:o_c_d:=0;

3

[o_v_d==v_d]

4

[c_v_d==0]
/c_v_d:=1;

ev_brake{d_c:=0;}/sb_c:=1;

ev_drive
/v_d:=ml.req_speed(p);,
slope:=ml.req_slope(p);

move/
entry:o_v_d:=v_d;

13

5

6

12

[v<v_d]/d_c:=1;,sb_c:=0;

7

cont

[v>=v_d && v<1.05*v_d]/d_c:=0;

8

11

[v<=v_s]{sb_c:=0;} [v>1.1*v_d && sb_c==0]{d_c:=0;}/sb_c:=1;

10 [sb_c==1 && v>1.5*v_d]

/d_c:=0;,sb_c:=0;,eb_c:=0;

ev_brake{d_c:=0;}/sb_c:=1;

init_brake/
during:v_s:=sqrt(1.1*rbc_eoa−p)*2*ml.b/1.1;

halt

[v>1.1*v_s]{sb_c:=0;}
/eb_c:=1;ev_halt;

9

Fig. 6. Speed control

- If the current velocity of the train is below the desired value the transition
8 is enabled, the drive mode is set, and the service brake mode is switched
off.
- If the current velocity is equal or greater than the desired velocity but not
greater than 5% of the desired velocity the transition 7 is taken and the
drivemodeisswitchedoff.
- If the speed is greater than 10% of the desired speed and the service brake
mode is not active, the mode is switched from driving mode to the the service
brake mode by activating the transition 6.
The destination state in all three cases is the cont state. This state is left
either by receiving an ev drive event taking the transition 13 to the change
state and updating the slope and the desired speed variable or receiving an
ev brake event 10 and switching to the init brake state.
- If in the move state the service break mode is active and the current speed
is greater than 50% of the desired speed, then the emergency brake mode is
switched on by taking the transition 5tothe halt state.