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

80

70

60

50

40

30

20

10

0

−2000 −1500 −1000 −500 0

EoA−pos

Fig. 12. Safe region for initiating the braking

5 Parameterized Verification of the Cooperation Layer

In this section, we present results for verifying parameterized instances of trac
protocols. On the one hand, system safety in systems like ETCS crucially de-
pends on the right choice of parameter values. For instance, whether a train can
keep its speed safely depends on the relationship of EoA to the current veloc-
ity v and maximum braking power b . If these values are imbalanced then the
train protocol is no longer guaranteed to avoid crashes. Hence, it is utterly im-
portant to analyze and discover safety constraints between such parameters or
state variables and adjust design parameters in accordance with those parametric
constraints.
On the other hand, once those constraints have been discovered, all instances
of the trac scenario that satisfy the parametric safety constraints can be veri-
fied at once. Generally, safety statements do not only hold for a particular setting
but generalise to a broader range of possibilities. For instance, train control is not
only safe for a particular initial speed v 10 and a specific braking force b =0 . 1

with remaining EoA-distance of 5 km . Instead, the system remains safe for all
choices of parameters that satisfy a corresponding constraint. Using our tech-
niques from [43,45,44,46], all such instances of the system can be verified at once,
and the required safety constraints on the free parameters can be discovered.

≤

5.1 Parameterized Hybrid Systems

Parameters naturally arise from the degrees of freedom of how a part of the
system can be instantiated or how a controller can respond to input. They in-
clude both external system parameters like the braking force b of a train, and
design parameters of internal choice like SB , i.e., when to start braking before
approaching EoA in order to ensure that the train cannot possibly run into an
open gate or preceeding train.