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

by switching off the automatic mode of this train. The safe state will be left if
the train position is behind the position of the rail-road crossing and an unlock
message is sent to the rail-road crossing 2.Thenewstateisthe init state and
this train is ready to initiate a new request to a rail-road crossing.

8

9

calc_brake_point

[xcross==0 && p<x_b && p<x_c]/ev_drive
[xcross==1 && p<x_b && p<x_c && p<x_c_x]/ev_drive;

ev_calc/xcross:=ml.is_xcross(p):,
x_p:=ml.cross_p(p);,x_m:=0;,c_m:=0;

1

7

brake_point/
entry:x_b:=rbc_eoa−1.1*v^2/(2*ml.b);,
x_c:=x_b−2.1*max_send_delay*v;,
x_c_x:=x_c−2.1*(ml.x_time*v+ml.max_send_delay*v);

[p>=x_b]/ev_brake;

6

init

2

ev_halt

ev_reset/get_n_seg;

[xcross==1 && p>x_c_x && x_m==0]{x_m:=1}/ev_comm_cross;

3

[xcross==0 && p>=x_c && p<x_b && c_m==0]{c_m:=1}/get_n_seg;

4

Fig. 3. Monitoring of safe motion

The main calculations to guarantee the safe motion of the train are done in
the third state calc brake point showninFig.3.Thethreevariables x b , x c and
x c x are updated every time the brake point state is entered. To guarantee that
the train stops before reaching the EoA, the train has to initialize the service
brake some distance in front of the EoA. This distance depends on the current
velocity of the train and the deceleration induced by the service brake. The point
to initialize the service brake ( x b ) is dynamically calculated every time step by

v 2 1 . 1 ·

x b = EoA − (12)

2 · b

where v is the actual velocity of the train and b is the typical deceleration of
the service brake. The factor 1 . 1 guarantees a 10% safety margin. Typically, the
train should not stop at every EoA, so the train has to ask the RBC for a new
EoA before reaching the actual EoA. For comfort reason the new EoA should be
received before the train has switched to the braking mode so the request has
to be sent early enough in time before reaching the service brake initialization
point x b . The train will travel the distance p = v

t in time t with the velocity
v . The delay for the request of the new EoA is two times the maximal send delay
to the RBC plus the response time to serve this request. The point to initialize
the request for the new EoA canthenbecalculatedby

·

x c = x b − 2 . 1 · max send delay · v (13)

In case that the EoA is a rail-road crossing the train has to lock the rail-road
crossing before the train will reach this point. The train has to initiate a lock