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

input of this controller is the present deceleration of the train and the coecient
for a comfortable deceleration of the service brake.

a sb )+ T b

t

( dv

dv
dt −

a sb dt

I b = P b ·

dt −

(11)

0

We have presented here a sucient precise description of the dynamical sys-
tem. The equations are kept simple to get a linear system. The model can be
extended mostly and a more detailed description can be found in [54].

2.4 ETCS Control Part

We consider a train system which is under the control of a variant of the ETCS
level 3 protocol. The ETCS level 3 provides collision avoidance through a fully
automated, decentralized interlocking scheme where the trains are moving in
safe blocks. These blocks are controlled track-side by radio block centers (RBC)
which are control centers to supervise and control train movements in a terri-
tory with radio based train control. One RBC is responsible for a fixed number
of track segments and the trains currently on these track segments. The RBC
grants movement authorities for trains to freely move ahead until so called end
of movement authority (EoA) points. At each time there exist a certain EoA
for each train, which is typically the end of a track segment, the position of a
possibly unsafe point (e.g., a rail-road crossing), or the end of a train driving
ahead. The granted movement authority defines a safety block surrounding the
train. It is a moving block system which means that the signaling system will
clear the track behind a train continuously.
This protocol is completely modelled in Stateflow and consists mainly of four
states running in parallel. The rbc req state shown in detail in Fig. 1 is respon-
sible for the communication to the RBC. The rbc req state is entered in the init

2 3 4 5

after(ml.send_delay*10,time)[before(ml.max_send_delay*10,time)]

rbc_req

/ev_rbc_req;

after(ml.max_send_delay*10,time)/ev_brake;

rbc_send rbc_wait

init

ev_rbc_ack[before(ml.send_delay*10,time)]/ev_calc;

get_n_seg{rbc_c_pos:=p;rbc_c_eoa:=rbc_eoa;rbc_t_id:=ml.t_id;}
/ev_rbc_req;

1

[mode==1]{rbc_c_pos:=p;,rbc_t_id:=ml.t_id;}/ev_rbc_req;

Fig. 1. RBC communication control part

state. This state will be left by taking the transition 1 only if the variable mode
is equal to 1 which means that this train is under the supervision of the ETCS .
After enabling this transition and before entering the destination state rbc send ,