|
|
|
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.
A formally verified algorithm called
KB3D
has been developed to demonstrate the viability
of a mathematically rigorous approach to safety assessment.
See
PVS development to obtain machine readable versions
of the specifications and proofs.
The current research focus is the development of ACCoRD
(Airborne Coordinated Conflict Resolution and Detection), a mathematical framework for
the formal design and verification of state-based separation assurance systems.
- Jeffrey Maddalon, Ricky Butler, César Muñoz, and Gilles Dowek, Mathematical Basis for the Safety Analysis of Conflict Prevention
Algorithms, Technical Memorandum, NASA TM-2009-215768, June 2009. BibTex Reference.
- Ricky Butler and César Muñoz,
Formally Verified Practical Algorithms For Recovery From Loss of Separation,
Technical Memorandum, NASA TM-2009-215726, June 2009. BibTex Reference.
- Ricky Butler and César Muñoz,
A Formal Framework for the Analysis of Algorithms That Recover From Loss of Separation,
Technical Memorandum, NASA TM-2008-215356, October 2008. BibTeX Reference.
-
Gilles Dowek and César Muñoz,
Conflict Detection and Resolution for 1,2,..,N Aircraft,
7th AIAA Aviation Technology, Integration and Operations Conference, 2007.
BibTeX Reference.
-
André Galdino, César Muñoz, and Mauricio Ayala,
Formal Verification of an Optimal Air Traffic Conflict Resolution and Recovery Algorithm,
14th Workshop on Logic, Language, Information and Computation, 2007.
BibTeX Reference.
-
César Muñoz, Radu Siminiceanu, Víctor Carreño, and Gilles Dowek,
KB3D Reference Manual - Version 1.a, Technical Memorandum,
NASA/TM-2005-213769, June 2005.
BibTeX Reference.
-
Gilles Dowek, César Muñoz, and Víctor Carreño,
Provably Safe Coordinated Strategy for Distributed Conflict Resolution,
AIAA Guidance Navigation, and Control Conference and Exhibit 2005, 2005. BibTeX Reference.
- Jeffrey Maddalon, Ricky Butler, Alfons Geser, and César Muñoz,
Formal Verification of a Conflict Resolution and Recovery Algorithm,
Technical Paper, NASA/TP-2004-213015, April 2004.
BibTeX Reference.
- Ricky Butler, Alfons Geser, Jeffrey Maddalon, and César
Muñoz,
Formal Analysis of Air Traffic Management Systems: The case of Conflict Resolution and Recovery, Proceedings
of the 2003 Winter Simulation Conference (WSC 2003), 2003. BibTeX Reference.
-
Alfons Geser and César Muñoz,
A
Geometric Approach to Strategic Conflict Detection and Resolution, Proceedings
of the 21st Digital Avionics Systems Conference (DASC 2002), 2002. BibTeX Reference.
-
Alfons Geser, César Muñoz, Gilles Dowek, and Florent
Kirchner, Air Traffic Conflict
Resolution and Recovery, Contractor Report, ICASE 2002-12, 2002.
BibTeX Reference.
- Víctor Carreño,
Evaluation of a Pair-Wise Conflict Detection and Resolution Algorithm in
a Multiple Aircraft Scenario, Technical Memorandum, NASA TM-2002-211963, 2002.
- Gilles Dowek, César Muñoz, and Alfons Geser,
Tactical
Conflict Detection and Resolution in a 3-D Airspace, Proceedings of
the Fourth International Air Traffic Management R&D
Seminar (ATM 2001), 2001. BibTeX
Reference.
Extended version available as Contractor Report ICASE 2001-7, 2001.
BibTeX
Reference.
Note: The
tag identifies links that are outside of the NASA domain.
|
