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

the variables rbc c pos and rbc t id will be set to the current position p of the
train and to the specific id of the requesting train. By taking this transition a
request for a new EoA will be sent to the RBC and a timer will be started by en-
tering the rbc send state. After the time interval of a normal transmit action but
before the upper bound of transmit actions has been reached, the request will
be transmitted again. This behaviour is modelled in the transition on top 2of
the rbc send state. If no message arrived before the maximum send delay period
is reached the service brake will be initialized by taking the transition 3and
generating a brake event ev brake which will be consumed in the moved state in
Fig. 6. If an acknowledge arrived before the max send delay the transition 4 will
be enabled and an ev calc event is generated, leading to the destination rbc wait
state. This state will be left after consuming a get n seg event and enabling the
transition 5tothe rbc send state. This transition is a model of a request for
travelling to a new track segment after the current EoA which will be sent to the
RBC. The parameters of this request are the current train position rbc c pos ,
the current EoA rbc eoa of the train and the train id t id . The RBC will then
calculate the new EoA with respect to the current train position of train t id ,
the current EoA of this train and the current positions of possible other trains
moving ahead.
The second state is the com cross state (Fig. 2) containing the communication
model between the train and a rail-road crossing. If an ev com cross event is

2 3 4

com_cross

init

[p>x_p]/ev_unlock;

safe

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

1

x_com_point unsafe

ec_com_cross/ev_lock;

[p>x_c && safe==0]/ev_brake

Fig. 2. Level crossing communication control part

consumed the transition 1 will be taken and a lock request will be sent to the
rail-road crossing. If the level crossing has transmitted the safe state message
before the train has reached the start-of-communication-point-to-rbc x c ,the
transition 4 is taken, generating a request for a new EoA to the RBC. The
variable c m will be set to 1 which means that this train has already sent a
lock message to the rail-road crossing. The new state is the safe state. If the
train is behind the start-of-communication-to-rbc point and receives an unsafe
message from the rail-road crossing the transition 4 is enabled and the service
brake will be initiated by an ev brake event. The unsafe state will only be left