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

4 Verification of the Cooperation Layer

In [13] we proposed a rule that decomposes the proof of the global property
of collision avoidance of two tra c agents into simpler properties with the aim
that they can be automatically verified. In this section we give a summary of
this proof rule and show that an important ingredient of this rule, the criticality
function, can indeed be found automatically. This is illustrated with the train
case study.

4.1 A Design Pattern for Collision Avoidance

Proving the global safety property of collision freedom for a collection of trac
agent is extremely dicult because each trac agent is (modelled by) a hybrid
system with a number of (discrete) modes and a different continuous dynamics
in each mode. To break down the complexity of this verification task we exploit
that trac agents typically cooperate using a certain pattern of operation modes
that can be described as a generic phase-transition diagram shown in Fig. 7.

(1)

φ N

FAR

NEGOTIATING

φ F

(3)

(2)

(4)

CORRECTING

FAILSAFE

RECOVERY

(5)

Fig. 7. Phase-transition diagram for proof rule

The phase FAR collects all controller modes that are not pertinent to collision
avoidance. The protocol may only be in phase FAR if it is known to the con-
troller that the two agents are “far apart”. Determining conditions for entering
and leaving phase FAR is thus safety critical. The NEGOTIATION phase is ini-
tiated as soon as the agents might evolve into a potentially hazardous situation.
Within the negotiation phase the two agents determine the set of maneuvers to