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

- A criticality function measures for each configuration of the (physical) state
of involved agents its closeness to collisions;
- Thresholds of this function are chosen taking into account the dynamics of
trac agents to initiate negotiations on agreeing on strategies, as well as on
their initiation;
- Strategies are reducing criticality of the agents state.
These design patterns have been proven to be expressive enough to cover rail,
automotive, as well as avionics applications. A key feature of our approach to the
verification of the coordination level is the capability to automate the generation
of candidate criticality functions for linear strategies, by using linear matrix
inequality (LMI) solvers to instantiate parameters in a suitably chosen quadratric
generic form for candidate criticality functions taking into account the dynamics
of the strategies. Moreover, the application of the design pattern generates safety
requirements for the subsystem of the trac agents responsible for inter-agent
communication as well as strategy realization.
Such safety requirements are discharged at the control-level using symbolic
reachability analysis (see Section 7). We have tuned the verification algorithms
to cater for control models with non-trivial discrete control (e.g., resulting from
the interaction between inter-agent coordination and control). This calls for a
fully symbolic representation of the hybrid system state space in reachability
analysis - in contrast to the explicit representation of discrete states used in hy-
brid system verification tools such as PHAVer [21], Checkmate [49], HyperTech
[27]. The key to achieve this are recent results to lift techniques for compact
discrete state space representations based on And-Inverter Graphs to the theory
of linear arithmetic (Lin-AIGs) required to deal with hybrid system verifica-
tion. The current prototype of our verification engine [11] uses substitution in
backward image computation along jumps, providing for linear guards and lin-
ear expressions in assignments, and Loos-Weispfennig quantifier elimination for
backward image computations at flows, and redundancy elimination for sets of
linear-constraints, assuming linear hybrid automata. Future work will lift this
extension to include plant models supporting linear differential equations. To
cater for the transition to design models, we re-verify the safety requirements
allocated to this subsystem, now using an abstraction refinement approach ad-
dressing discrete time reachability analysis for models with linear dynamics [48].
Stability of control models is demonstrated using LMI based candidate genera-
tion for Lyapunov functions for hybrid systems with linear differential equations,
developed in [41]. As discussed in Section 6, we also show that stability can be
re-proven after discretizing the system model with a given sampling rate, result-
ing in a discrete-time hybrid system with linear difference equations. This allows
for the identification of safe sampling rates maintaining stability, which can in
turn be used for discrete-time reachability analysis.
Jointly, these techniques allow a formal verification of stability and safety
properties, with traceability of requirements from the coordination layer to de-
sign models.