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

The major challenge in dealing with symbolic parameters is that they lead
to nonlinearities: Even comparably simple flow constraints like 2 b ( EoA p ) be-

come nonlinear when b is considered as a symbolic parameter rather than in-
stantiated with some specific value like 0 . 1.
To handle parameters, we follow a fully symbolic deductive approach. We
have introduced a logic, d L

−

, for verifying hybrid systems with parameters and a
corresponding verification calculus [43]. It generalizes dynamic logic from the dis-
crete case [23] to hybrid systems. Our d L

calculus can be used both for verifying
correctness statements about parametric hybrid systems and for deriving con-
straints on their free parameters that are required for safety [43]. Thus, with d L ,

it is possible to zoom in to a subset of the system, typically at the coordination
layer, and find safety constraints for the parameters.

5.2 Technical Approach: Differential Logic

To illustrate how our techniques for parameterized hybrid systems work, we
provide a short survey of the d L principles. The full details of the theory behind

d L are reported in [43,45,44,46].

The logic d L

provides modal formulae like [ MA ] φ , which express that all runs
of the parametric hybrid system MA (see Subsection 4.2) lead to states which
satisfy some safety constraint φ . Further, such formulae can be combined propo-
sitionally, by quantifiers, or modalities [ β ] about other automata β .Withthis,
safety of parametric hybrid systems can be stated as formulae in the logic d L ,

for instance:

b > 0 ∧ ≥ 0 ⇒ [ MA ]( p ≤ EoA ) . (17)

This d L formula states that all runs of the hybrid system MA are such that the

train position p remains within the movement authority EoA , provided that the
braking force b is non-zero and the maximum reaction-cycle-time is some

0.
Both symbols, b and , are train model parameters and given externally. Their
values depend on the specific characteristics of the actual train and should be
handled symbolically for a thorough analysis of all trains. From the perspective of
a single train automaton, EoA can also be considered as an external parameter.
In the full system MA , which involves trains and RBCs, it can also be considered
as a state variable instead.
Using the d L

≥

calculus, such a formula can be analyzed systematically in order
to find out if it holds or under which parameter constraints the system is safe. For
instance, for the safety constraint (17), the d L

calculus reveals that the system is
only safe when the initial velocity does not exceed the braking capabilities and
the control parameters are chosen in accordance with the movement authorities,
speed, and reaction times.
To make our calculus compositional and simplify its step-wise symbolic pro-
cessing principle, we use a textual notation of hybrid automata as hybrid pro-
grams [43]. As hybrid automata [25] can be embedded in hybrid programs by a
simple canonical construction [43], we identify hybrid automata and their cor-
responding program rendition, here. With this embedding, parametric safety