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

can get an EoA-extension from the RBC before reaching EoA. The control para-
meter SB is the safety distance at which the speed supervision needs to initiate
braking when no positive EoA extension has occurred yet (recovery mode). Both
parameters are formulated as points on the track in terms of distances from EoA
(see Fig. 4).
The parameter SB is a very important safety parameter that needs to be
chosen adequately such that the train can guarantee to remain within its move-
ment authority, regardless of the behavior of other trac agents like preceeding
trains or gates at critical sections as mediated by the RBC agent. Especially,
if SB is chosen right, the system remains safe, whatever the outcome of the
RBC communication may be.
The safety constraint for parameter SB can be derived from an analysis of
the hybrid program rendition of the MA -automata using a proof of the form in
Fig. 13, see [43] for details. In addition, the underlying RBC and train models
bridge the gap from cooperation layer models to design layer models as they take
maximum controller response times into account. Similar to the notion of lazy
hybrid automata [51], we account for the fact that controller implementations
react with a processing delay and that the effect of actuators like brakes can be
delayed as well.
An acceleration a SB , when adaptively

choosing SB depending on the current speed v and the parameters of maximum
braking force b and maximum speed supervision response time in accordance
with the following constraint:

≤ a max is permitted in case EoA − p ≥

2 b + a max

+1 a max
2

ε 2 + ε v .

v 2

SB ≥ (19)

b

This constraint expresses that it is only safe to keep on driving when the control-
lability constraint (18) is maintained even after a maximal acceleration of a max
during a maximum period of time units. In particular, constraint (19) makes
the controllability constraint (18) inductive.
Observe that constraint (19) is a refined and parameterized version of the (12)
(remember that x b is the point on the track corresponding to the distance SB
from EoA ). The actual symbolic constraints in (19) identify what needs to be
captured by the 10% safety margin in (12). It also clearly identifies under what
conditions a 10% safety margin is sucient. Likewise, constraint (19) explains the
shape of the safety region given in Fig. 12 and gives insights about a systematic
symbolic generalization of the numerical criticality function in (15). It identifies
fully symbolic constraints as opposed to specific real numbers that only hold for
a particular scenario.
Parameter ST is a liveness parameter. Depending on the expected maximum
RBC communication latency L , which again is a parameter for the train analysis,
it ensures that the RBC can still respond in time before the train needs to
decelerate. That is, when the train enters negotiation at ST , it does not need
to brake unless an EoA extension cannot be granted by the RBC within L at
all. For instance, an RBC may not be able to grant an EoA extension despite