To accommodate the predicted increase in air traffic, the next generation of air traffic management (ATM) systems relies on operational concepts where the responsibility for separation is distributed between airborne and ground systems. These distributed modes of operation are enabled by new positioning and communication technology that provides precise state information for ownship and traffic aircraft. A critical component of a distributed ATM system is the airborne conflict detection and resolution (CD&R) system. A CD&R system warns pilots about predicted traffic conflicts and advises them on resolution maneuvers.

The mathematical framework consists of a collection of mathematical theories in the formal notation of the Program Verification System (PVS). The framework assumes a 3D rectangular coordinate system, with two aircraft, one of which is identified as the ownship and the other as the intruder aircraft. State information, consisting of position and velocity vectors of the aircraft, is available to both aircraft. Aircraft trajectories are predicted to be linear projections of the current state. Resolution maneuvers are defined as new velocity vectors that the ownship implements instantaneously. The protected zone is a volume around each aircraft of diameter D and height H.

A loss of separation is defined as an overlap of the protected zone of two aircraft. A conflict is a predicted loss of separation between the aircraft within a look-ahead time T. A conflict detection algorithm is a function that has as input the state information of both aircraft and returns the time to conflict and the duration of the conflict. A conflict resolution algorithm is a function that receives as input the state information of the aircraft and returns a set of resolution maneuvers for the ownship. Four kinds of resolution maneuvers are considered: track only, ground speed only, optimal track/ground, and vertical speed only. Resolution maneuvers are independently correct if they yield conflict- free trajectories assuming that only the ownship maneuvers solve the conflict. Resolution maneuvers are coordinately correct if they yield conflict trajectories when both the ownship and the intruder aircraft maneuver.

The framework provides a set of criteria that guarantees correctness of independent and coordinated maneuvers, and algorithm definitions of maneuvers that yield trajectories that are tangential to the protected zone (or larger) and that satisfy these criteria. Although the framework provides concrete algorithms for conflict detection and resolution, it is applicable to a variety of state-based CD&R algorithms. The approach guarantees that different implementations can safely coexist in the air traffic system as long as they satisfy the correctness criteria defined in the framework. The framework has been developed in a formal verification environment. The mathematical correctness extends to the algorithmic definitions provided by the framework.

This work was done by Ricky Butler of Langley Research Center, and Cesar Munoz and Gilles Dowek of the National Institute of Aerospace. LAR-17785-1