Skip past navigation NASA Langley Formal Methods



quick page





  home > research > fm-atm > fm-atm-cdr

Formal Analysis of Conflict Detection and Resolution Algorithms

Current software safety assurance methods are not adequate for the Next Generation Air Transportation System (NGATS). The current method is based on human-factors oriented experimentation with high fidelity simulations, systems-level safety analyses, and process control of the software development process. 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 the software. The correctness of the algorithms, designs implementations must be established for all possible situations. Simulation and testing alone cannot accomplish this.

The current research focus is the development of Airborne Coordinated Conflict Resolution and Detection (ACCoRD), a mathematical framework for the formal design and verification of state-based separation assurance systems. There are now several NASA-developed software packages which are available upon request for government work.


Note: The external link tag identifies links that are outside of the NASA domain.


  Skip past navigation  
home | welcome | quick page | philosophy | team | research | quote | links | new?
Curator and Responsible NASA Official: Ricky W. Butler
larc privacy statement
last modified: 26 September 2003 (10:10:40)