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

Safety. For the train's safety envelope SE Train ( p ) we choose an extension around
its current front position p which encompasses the length of the train, indepen-
dent of mode and speed:
SE Train ( p )=[ p

− L T , p ] ⊆ Position

where L T is the length of the train. The critical section's safety envelope depends
on the position of the EoA :
SE CS = ∅

if CS . e < EoA

[ CS . b , CS . e ] otherwise

The choice of as the extension of the safety envelope caters for the case that

the RBC has granted an extension of the EoA beyond the critical section. This
permits the train to pass the critical section without safety violation.
We define inCS ( p )

∅

CS . e + L T . The predicate inCS describes
all positions where the safety envelopes of the train and the critical section
overlap, i.e.,
SE Train ( p ) ∩ SE CS

⇔ CS . s ≤ p ≤

= ∅ ⇔ inCS ( p ) ∧ EoA ≤ CS . e .

Thus collision freedom is equivalent to inCS ( p ) CS . e < EoA , i.e., whenever

the front position p is in the critical section, the EoA has been extended beyond
the critical section.

⇒

Trac Agents. The scenario movement authority is modeled as a system MA
with two trac agents:
MA = Train

RBC ,

one train consisting of plant and controller interacting with an RBC consisting
of a controller only. Fig. 8 shows how these agents are represented by real-valued
variables pos (position), spd (speed), acc (acceleration) and EoA (end of author-
ity), and which (other) variables the four components share for communication
with each other.
We assume that the train plant has knowledge of its position on the track
and controls its speed depending on requests from the train controller. It will
react to speed control commands from the train controller. Thus we consider the
variables below. We do not distinguish between the (syntactic) variables of the
automaton and the corresponding trajectories in runs. So we take for the type
of a variable the type of its time-dependent trajectory, and we permit variables
with discrete ranges without explicitly coding them in reals.

Variables: Train plant

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

output pos : Time → Position (position of the train)

→

spd : Time Speed (speed of the train)

acc : Time → Acc (acceleration of the train)