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

Warnings. The following type A verification condition checks that each trajec-
tory leading from a plant state without warning to a collision must cross an
activation condition of one of the correcting modes, i.e., it checks whether the
set of provided maneuvers is complete .

(VC 4) Completeness of maneuvers.

P 1 P 2 | =( ¬ φ N ; true) ∧ ( ¬ collision ; ↑ collision ) ⇒ ↑ Φ start

The activation conditions for maneuvers must be chosen in such a way that crit-
icality is below the critical threshold when maneuvers become enabled, leading
to the following type A verification condition.

(VC 5) During warning period criticality is still low.

Th ( R ) | = ∀ δ ≤ Δ C :( acc 1 = acc 2 =0 ∧↑ pre ( δ, Φ start ) ⇒ cr < c safe )

This yields P 1 P 2 | =( acc 1 = acc 2 =0 ∧ = Δ C ; ↑ Φ start ) ⇒ cr < c safe .

In particular, this ensures that maneuvers are not activated too late.

Negotiation phase. The negotiation phase must be initiated as soon as a first
warning occurs. Recall that this event is represented by Φ N becoming true. The
following type B verification condition checks this.

(VC 6) Initiating negotiating phase. For i =1 , 2

↑Φ N
−−−→

C i P 1 P 2 | = FAR ( C i ) NEG ( C i )

Note that both controllers enter their negotiating phase simultaneously when
the trigger

φ N occurs.
The following type D verification condition guarantees that pre ( Δ C ,Φ start ),
the warning to start maneuvers according to Φ start , was raised early enough. If
the tra c agents changed their speeds during negotiation and selection (sub-)
phase, the calculations of the warning would be wrong.

↑

(VC 11) No acceleration during negotiation and selection. For i =1 , 2

C i P i | = NEG ( C i ) ∨ SEL ( C i ) ⇒ acc i =0

The last type C verification condition for the negotiation phase checks, that
indeed negotiation is completed within the given time window of length Δ N .

(VC 12) Negotiation completes in time.

C 1 C 2 | = NEG ( C 1 ) ∨ NEG ( C 2 ) ⇒ ≤ Δ N

where Δ N <Δ C .Thus both controllers have left their negotiating phase after
at most Δ N time units.