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

true / sc := Keep, Φ N /

Far Appr

sc := Keep, extEoA := tt

CS.s := EoA

sc = Keep sc = Keep

afterCS(pos) /
sc := Keep

sc := Brake /

OK

SafeAppr Braking

sc = Brake

sc = Keep

FailSafe

(spd=0)

sc = Brake

Fig. 9. Train controller

The dynamics of the train controller is described by the automaton in Fig. 9.
Initially, the controller is in the mode Far. When the predicate Φ N abbrevi-
ating pos ST ( spd ,Δ C ) becomes true the controller switches to the

mode Appr. On occurrence of a signal OK the controller switches to the mode
SafeAppr indicating that the train can safely approach the critical section. In
this mode the train continues to keep its speed. If the predicate Φ abbreviating
pos

≥ EoA −

SB ( spd ) becomes true the controller switches to the mode Braking
where it forces the train to brake until a complete stop. If the train's speed is
zero, the controller enters the mode FailSafe. In the terminology of Fig. 7, the
mode Appr is the phase NEGOTIATION , SafeAppr is CORRECTING ,and
Braking is RECOVERY .
The RBC is modelled only as far as the communication concerning the exten-
sion of EoA is concerned. It outputs of current EoA to the train and if requested
to extend it by an extEoA signal may grant an OK signal. Thus the RBC con-
troller has the following time dependent variables.

≥ EoA −

Variables: RBC controller

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

local x : Time → Time (clock)

output EoA : Time → Position (current EoA)

OK : Time → B (EoA is extended)

Modes: Idle, Check, Unsafe