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

hybrid automata. We consider one train moving along a track and communi-
cating with a radio block center (RBC) that grants movement authorities to
the train. At each moment of time there is a certain end of movement authority
(EoA) for the train because after the EoA a critical section begins, which may be
a rail-road crossing or a track segment occupied by a preceding train (cf. Fig. 4).
We start from domains Position =

R ≥ 0 with typical element p for the position

of the train on the track, Speed = R ≥ 0 with typical element v for the speed of

the train, and Acc = R with typical element a for the acceleration of the train.

Let v max denote the maximal speed of the train and − b the braking force of the

train, represented as a negative acceleration, i.e., with − b < 0. The current end

of authority for the train is modelled by an observable

EoA : Time → Position

which is maintained by the RBC. We require

∀ t 1 , t 2 ∈ Time : t 1 ≤ t 2 ⇒ EoA ( t 1 ) ≤ EoA ( t 2 ) .

The critical section CS behind the EoA is represented by an interval of positions

[ CS . s , CS . e ] ⊆ Position

starting at CS . s and ending at CS . e , with a fixed positive length CS . e − CS . s .

A predicate describing all positions after the critical section is

afterCS : Position → B with ∀ p ∈ Position : afterCS ( p ) ⇔ CS . e ≤ p .

When the train approaches the current EoA it has to start talking to the RBC
to get permission to extend the EoA. The distance relative to EoA where start
talking has to be initiated is modelled by a function

× →

ST : Speed Time Position

depending on the train's speed, the maximal time delay needed to communicate
with the RBC, and implicitly on the fixed braking force b . If the permission is

not granted by the RBC the train has to start braking with the braking force

−

b .
The distance relative to EoA where the braking has to be initiated is modelled
by a function

−

SB : Speed → Position

depending on the train's speed and implicitly on the fixed braking force − b .

These positions and distances are illustrated in Fig. 4. We require

∀ v ∈ Speed ,Δ ∈ Time : ST ( v ,Δ ) ≥ SB ( v ) .