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

request to the rail-road crossing and the rail-road crossing has to lock the crossing
and acknowledge the lock request. After receiving a safe message the train can
send a request for a new EoA to the RBC. The point to initialize a lock request
to a level crossing is calculated by

x c x = x c − 2 . 1 · ( x time + max send delay ) · v (14)

The time to set up the rail-road crossing in a safe state is stored in the x time
variable. These three points ( x b , x c and x c x ) are updated every time the
brake point state is entered. A spatial view of this scenario is shown in Fig. 4, and

RBC

ST

CS afterCS

SB

v

￿￿￿￿￿￿￿￿￿ ￿￿￿￿￿￿￿￿￿

Train

p x_c x_b EoA

Fig. 4. Radio-based train control

a snapshot of the dynamical behaviour can be seen in Fig. 5. After explaining
the main ideas to guarantee a safe motion, we continue to discuss Fig. 3. The
transition 1 is enabled after receiving an end-of-authority message from the
RBC. By taking this transition the two variables which count the messages to
the RBC and to the rail-road crossing are initialized to 0.Thevariable xcross
picks up the information if a rail-road crossing is just in front of the current
position p of the train. The position of the rail-road crossing itself is stored in
the x p variable. The information of the rail-road crossing is read out of the track
data dictionary. If there is no rail-road crossing ahead and the current position
of the train is before the point to initialize the service brake and before the
point to initialize an EoA-request the transition 9 will be taken and an ev drive
event is generated to switch into the driving mode of the train. In case there is a
rail-road crossing ahead the transition 8 will be enabled. If the train has passed
the point to send an EoA-request to the RBC but in front of the x b point the
transition 3 will be taken and a get n seg event is generated to initialize the
request of a new EoA. If there is a rail-road crossing ahead and the train has
passed the x c x point a lock request is generated by the ev com cross event
released by the transition 4 . If the train has passed the x b point the transition
7 is enabled which leads to the service brake mode by the ev brake event. In
case of an emergency halt indicated by the ev halt event the brake point state
will be left by enabling the transition 6tothe halt state.