# Presentation: 108852

## Conflict Detection and Resolution

The KB3D Algorithm and 
Its Formal Verification

- The **KB3D Algorithm** and
- Its Formal Verification

_*Contributors:*_
- César Muñoz, Alfons Geser, Gilles Dowek, Víctor Carreño, Radu Siminiceanu, Jeffrey Maddalon, André Galdino, Mauricio Ayala and Ricky Butler

## .

- Current safety assurance methods are inadequate for free flight concepts
- Current method is based on human-factors oriented experimentation with high fidelity simulations.
- But as software takes on more and more responsibility for detecting potential conflicts and recommending or executing the evasive maneuvers, we will need additional methods to guarantee safety of software.
- Simulation and testing cannot accomplish this.

- Today the primary responsibility for aircraft separation is borne by the air traffic controller.

- vi

- vo

- vo’

- D

- ownship

- intruder

## KB3D Conflict Detection Algorithm

- A generalization of Karl Bilimoria’s CD&R algorithm (used in FACET) to 3 dimensions
- The KB3D algorithm produces multiple solutions that only require a change in only one state parameter (i.e. heading, ground speed, vertical speed)
- Formally proved that it will always generate a valid solution for two aircraft with arbitrary trajectories.
- Completed formal proof of optimal return paths (RR3D)
- Formally proved to be coordinated

## Axes Translation To Facilitate Analysis

- Position and velocity translation of axes
-     s = (sx, sy, sz) = s0 - si
-     v = (vx, vy, vz) = v0 - vi
- Of course, one must translate results back to original axes in implementation code (easy to do).

## KB3D: Horizontal/Vertical Views

- D

**KB3D: Horizontal/Vertical Views**

- H

- +
- +

## Resolution Maneuvers

- The KB3D algorithm generates maneuvers where only one of vertical speed, ground speed, or heading are changed.
- (Easier for Pilot to Fly)
- Let vo' = (v'ox, v'oy, v'oz ) be the resolution velocity vector for the own
- Let vo = (vox, voy, voz ) be its original velocity vector
-   Vertical Speed Only       v'ox = vox   ,    v'oy = voy
-   Ground Speed Only       v'ox = k vox  ,   v'oy = k voy,   v'oz = v'oz
-   Heading Only                 v'ox2+ v'oy2 = vox2+ voy2,       v'oz = v'oz

## Cd3d Example

## The Vertical Solutions

- IF not horizontally separated THEN

- ELSE IF  | sz  | ≥ H

- ELSE

## Resolution and Recovery (RR3D)

- The RR3D algorithm computes
-   *relative** *escape velocity vector v' = v'0 - vi
-   turn time t'
*  **relative* recovery velocity vector v''= v''0 - vi

## Verification Goal

- Must show
- escape maneuver (ve) maintains separation
- recovery maneuver (vr) maintains separation
- escape and recovery maneuvers reach the same ending point at the same time as the original course.
- Turn time less than destination time: 0 < te < tr

- m: solution
- RR3D_alg_correct: THEOREM
-                                 FORALL m:member?(m, RR3D_alg(s,vo,vi,tr)) IMPLIES
-                                                 separation?(s, m`ve) AND
-                                                 separation?(s + m`te * m`ve, m`vr) AND
-                                                 s + tr * v = s + m`te * m`ve + (tr - m`te) * m`vr AND
-                                                0 < m`te AND m`te < tr

## Typical Correctness Theorem

-   llhd_escape_C THEOREM
-       sq(s`x) + sq(s`y) > sq(D)  AND                 % TEST CONDITION
-       sq(vo`x) + sq(vo`y) /= sq(vi`x) + sq(vi`y) AND % TEST CONDITION
-       hor_speed_gt_0?(ve) AND                        % TEST AFTER COMPUTATION
-       discr(1 + sq(alpha), vi`x + alpha * vi`y,      % TEST CONDITION
-             sq(vi`x) + sq(vi`y) - sq(vo`x) - sq(vo`y)) >= 0 AND
-       alpha = IF sq(D) = sq(s`x) THEN -(sq(D) - sq(s`y))/(2*s`x*s`y)
-               ELSE (-s`x*s`y+eps*D*sqrt(sq(s`x)+sq(s`y)-sq(D)))/(sq(D)-sq(s`x))
-               ENDIF AND
-       (ve`x = x1(1+sq(alpha),                        % COMPUTED VALUE
-                  vi`x+alpha*vi`y,
-                  sq(vi`x)+sq(vi`y)-sq(vo`x)-sq(vo`y)) OR
-        ve`x = x2(1+sq(alpha),
-                  vi`x+alpha*vi`y,
-                  sq(vi`x)+sq(vi`y)-sq(vo`x)-sq(vo`y)))   AND
-       ve`y = alpha*ve`x                              % COMPUTED VALUE
-     IMPLIES
-       separation?(s,ve)

## Verification that Algorithm is Coordinated

- For two aircraft executing the CD&R algorithm, **prove**
- Recommended/executed trajectories are always in opposite directions
- In a perfectly symmetric case, there is a symmetry breaking mechanism

**Don’t Want:**

## N Aircraft: Collaborative Properties

- For N aircraft executing the CD&R algorithm, **PROVE** all recommended/executed trajectories maintain separation:

- Our CD&R algorithms do not need explicit handshake to achieve
- coordinated resolutions.  The only information exchanged is position,
- and velocity via ADS-B.

## Status Of Formal Verifications

- KB3D formally verified for two aircraft
- RR3D formally verified for two aircraft
- KB3D formally verified to be coordinated
- KB3D vertical maneuvers formally verified to be collaborative (for N aircraft assuming adequate airspace above)

- Current work:
- Adding ability to recover from loss of separation
- Adding target altitude intent information
- Integrating with prediction bands
- Extending analysis to cover input inaccuracies and errors

## How Do You Model the Pilot (N Aircraft Problem)?

- How long will he wait to execute algorithm?
- How long would he wait to turn back to course?
- How long after a conflict warning disappears would the pilot no longer seek to resolve?
- In a situation where there are multiple aircraft, which aircraft would he chose to resolve with?
- The closest aircraft?
- The one requiring the smallest heading change?
- The first one to be in conflict with
- The one with the shortest time until loss of separation?

## Long Term Goals

- Generalize formal proof to multiple aircraft.
- Will require a premise that involves some kind of traffic complexity/density metric
- Integration with strategic algorithms (e.g. based on genetic algorithms)
- Add aircraft performance to KB3D
- Transform KB3D to a great-circle implementation