Airborne Coordinated Conflict Resolution and Detection (ACCoRD) is a framework for the formal specification and verification of state-based conflict detection and resolution algorithms. ACCoRD originates from KB3D, a state-based conflict detection and resolution algorithm. ACCoRD provides:

• A 3-D conflict detection algorithm, called CD3D, that is correct and complete.
• A 3-D conflict resolution algorithm, called CR3D, that is independent and coordinated for track only, ground speed only, vertical only, and combined track and ground speed resolution maneuvers.
• A loss of separation recovery algorithm that is correct.
• A 3-D prevention bands algorithm that computes all the critical vectors.
• Definition of provably correct safety buffers for CD&R algorithms (assuming that track and ground speed errors are unknown but bounded).
• Least but not last, formal specifications and proofs of the ACCoRD framework are available in the NASA PVS Library.

The ACCoRD framework is part of our research on Formal Analysis of Conflict Detection and Resolution Algorithms. Software prototypes in Java and C++ are available upon request. Note that these prototypes are not suitable for use in a real system and they should not be used as such.

Publications

• Anthony Narkawicz, César Muñoz, and Aaron Dutle, Coordination Logic for Repulsive Resolution Maneuvers, Proceedings of the 16th AIAA Aviation Technology, Integration, and Operations Conference (ATIO 2016), AIAA-2016-2756, Washington D.C., 2016. BibTeX Reference.
• Anthony Narkawicz and César Muñoz, A Formally Verified Conflict Detection Algorithm for Polynomial Trajectories, Proceedings of the 2015 AIAA Infotech @ Aerospace Conference, AIAA-2015-0795, Kissimmee, Florida, 2015. BibTeX Reference.
• Anthony Narkawicz, César Muñoz, and George Hagen, An Independent and Coordinated Criterion for Kinematic Aircraft Maneuvers, Proceedings of the 14th AIAA Aviation Technology, Integration, and Operations (ATIO) Conference, AIAA-2014-2859, Atlanta, Georgia, 2014. BibTeX Reference.
• 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.
• 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, 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 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, 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. An extended version available as A Mathematical Basis for the Safety Analysis of Conflict Prevention Algorithms, Technical Memorandum, NASA/TM-2009-215768, June 2009. BibTeX Reference.
• Jeffrey Maddalon, Ricky Butler, César Muñoz, and Gilles Dowek, A 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, BibTex Reference, 2007.
• 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, BibTex Reference, 2007.
• César Muñoz, Radu Siminiceanu, Víctor Carreño, and Gilles Dowek, KB3D Reference Manual - Version 1.a, NASA/TM-2005-213769, BibTex Reference, 2005.
• 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, BibTeX Reference, 2005.
• 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, BibTex Reference, 2003.
• 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, BibTex Reference, 2002.
• Alfons Geser, César Muñoz, Gilles Dowek, and Florent Kirchner, Air Traffic Conflict Resolution and Recovery, ICASE Report 2002-12, BibTex Reference, 2002.
• Gilles Dowek, Alfons Geser, and César Muñoz, Tactical Conflict Detection and Resolution in a 3-D Airspace, Proceedings of the Fourth International Air Traffic Management R&D Seminar ATM 2001, BibTeX Reference, 2001. Extended version available as ICASE Report 2001-7, BibTeX Reference, 2001.

*The ACCoRD logo was designed by Mahyar Malekpour (NASA).

The tag identifies links that are outside the NASA domain