|
|
|
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.
Publications:
- Parasara Sridhar Duggirala, Le Wang, Sayan Mitra, Mahesh
Viswanathan, and
César Muñoz,
Temporal Precedence Checking for Switched Models and Its Application to a Parallel Landing Protocol, Proceedings of the 19th International Symposium on Formal Methods (FM 2014),
Lecture Notes in Computer Science, Vol. 8442, pp. 215-229, 2014
 . BibTeX
Reference.
- Anthony Narkawicz, César Muñoz, Jason Upchurch,
James Chamberlain, and María Consiglio,
A
Well-Clear Volume Based on Time to Entry Point,
Technical Memorandum, NASA/TM-2014-218155,
January 2014. BibTeX Reference.
- César Muñoz, Anthony Narkawicz, and James Chamberlain, A TCAS-II
Resolution Advisory Algorithm, Proceedings of the AIAA
Guidance, Navigation, and Control Conference (GNC), AIAA-2013-4622,
Boston, Massachusetts, 2013. BibTeX Reference.
- Ricky W. Butler and Timothy A. Lewis,
A Turn-Projected State-Based Conflict Resolution Algorithm,
Technical Memorandum NASA/TM–2013-218055, November, 2013
- Anthony Narkawicz, César Muñoz, Heber
Herencia-Zapana, and George Hagen, Formal
Verification of Lateral and Temporal Safety Buffers for State-Based
Conflict Detection, Proceedings of the Institution of
Mechanical Engineers, Part G: Journal of Aerospace Engineering,
Vol. 227, No. 9, pp. 1412-1424, September 2013. BibTeX Reference.
- Ricky W. Butler, George Hagen, and Jeffrey M. Maddalon,
The Chorus Conflict and Loss of Separation Resolution Algorithms,
Technical Memorandum NASA/TM-2013-218030, August 2013.
- Raleigh B. Perry, Michael M. Madden, Wilfredo Torres-Pomales, Ricky W. Butler.
The Simplified Aircraft-Based Paired Approach With the ALAS Alerting Algorithm,
Technical Memorandum NASA/TM-2013-217804, February, 2013
- Anthony Narkawicz and César Muñoz, Formal
Verification of Conflict Detection Algorithms for Arbitrary
Trajectories,
Reliable
Computing, Volume 17, pp. 209-237, December, 2012. BibTeX Reference.
- Ricky Butler, George Hagen, Jeffrey Maddalon, César
Muñoz, and Anthony Narkawicz, The search for
effective algorithms for recovery from loss of separation,
Proceedings of the 31st Digital Avionics Systems Conference (DASC 2012),
Williamsburg, Virginia, 2012. BibTeX Reference.
- Anthony Narkawicz, César Muñoz, and Jeffrey Maddalon, A Mathematical Analysis of Air Traffic Priority Rules, Proceedings of the 12th AIAA Aviation Technology,
Integration, and Operations (ATIO) Conference, AIAA-2012-5544,
Indianapolis, Indiana, 2012. BibTeX Reference.
- Anthony Narkawicz and César Muñoz,
State-based implicit coordination and applications,
Technical Publication, NASA/TP-2011-217067,
March 2011. BibTeX Reference.
- César Muñoz, Ricky Butler, Anthony Narkawicz, Jeffrey Maddalon, and George Hagen,
A Criteria Standard for Conflict Resolution: A Vision for Guaranteeing the Safety of Self-Separation in
NextGen,
Technical Memorandum, NASA/TM-2010-216862,
October 2010. BibTeX Reference.
- César Muñoz and Anthony Narkawicz, Time of Closest Approach in Three-Dimensional Airspace,
Technical Memorandum, NASA/TM-2010-216857,
October 2010. BibTeX Reference.
- Heber Herencia-Zapana, Jean-Baptiste Jeannin, and César Muñoz, Formal Verification of Safety Buffers for State-Based Conflict Detection
and Resolution, Proceedings of the 27th International Congress of the Aeronautical
Sciences (ICAS 2010), 2010. BibTeX Reference.
- Anthony Narkawicz, César Muñoz, and Gilles Dowek,
Provably Correct Conflict Prevention Bands Algorithms,
Science of
Computer Programming, Volume 77, Issues 10-11, pp. 1039-1057, September 2012. BibTeX Reference.
- Anthony Narkawicz, César Muñoz, and Gilles Dowek, Formal verification of air traffic prevention bands algorithms,
Technical Memorandum, NASA/TM-2010-216706,
June 2010. BibTeX Reference.
- Ricky Butler, George Hagen, Jeffrey Maddalon, César Muñoz, Anthony Narkawicz, and Gilles Dowek, How Formal Methods Impels Discovery: A Short History of an Air Traffic Management Project,
Technical Memorandum, NASA/CP-2010-216215,
April 2010. BibTeX Reference.
- Jeffrey Maddalon, Ricky Butler, César Muñoz, and Gilles Dowek,
A Mathematical Analysis of Conflict Prevention Information,
9th AIAA Aviation Technology, Integration, and Operations Conference, September 2009. BibTeX Reference.
- 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.
|
