«A Mathematical Framework for the Verification of Air Traffic Separation Assurance Systems»

This talk presents the Airborne Coordinated Conflict Resolution and Detection (ACCoRD) framework for the design and verification of state-based separation assurance systems. The framework, which has been specified and mechanically verified in PVS, consists of a set of definitions and formally proven criteria that guarantee the correctness of a family of SA algorithms. For instance, in the case of pairwise conflict resolution, ACCoRD provides criteria that guarantee that two distributed algorithms, which satisfy the same coordination criteria, independently compute resolution maneuvers that yield conflict free trajectories when simultaneously implemented by the aircraft. This talk gives more examples of such criteria and algorithms that satisfy them. It also argues that a criteria-based verification framework, such as ACCoRD, will enable the natural evolution of the worldwide Air Transportation System.

Cesar Muñoz
NASA Langley Research Center