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

EoA

Train Controller RBC Controller

extEoA

EoA

OK

pos spd sc

Train Plant

pos

spd

acc

Fig. 8. Communication between train and RBC

For the dynamics of the train we assume the continuous transition relations
pos • = spd and spd • = acc and the invariants − b ≤ acc and spd ≤ v max .Here

we are interested only in the change of speed during braking:
acc =

0 if sc = Keep ∨ ( sc = Brake ∧ spd =0)

− b if sc = Brake ∧ spd > 0

The train controller monitors the position and speed of the train. When ap-
proaching the current end of authority EoA (guarding a critical section) it re-
quests for an extension from the RBC by sending an extEoA signal. If the RBC
sends a signal OK the controller requests the train plant to keep the (desired)
speed. If the RBC does not reply in time and instead the train passes the posi-
tion SB the controller forces the train plant to brake. Thus the train controller
has the following time dependent variables.

Variables: Train controller

→

input pos : Time Position (position of the train)

spd : Time → Speed (speed of the train)

EoA : Time → Position (current EoA)

OK : Time → B (EoA is extended)

local CS . s : Time → Position (begin of critical section)

output extEoA : Time → B (request to extend EoA)

sc : Time →{ Keep , Brake } (speed control)

Modes: Far, Appr, SafeAppr, Braking, FailSafe