Formal Methods Support to UAS in the NAS

NASA’s Unmanned Aircraft Systems Integration in the National Airspace System (UAS in the NAS) project aims at conducting research towards the integration of civil Unmanned Aircraft Systems (UAS) into non-segregated airspace operations. Formal methods research played a key role on the development of a detect and avoid concept for UAS that interoperates with existing traffic collision avoidance systems such as TCAS. A practical contribution of this research is DAIDALUS, a collection of formally verified detect and avoid algorithms for UAS.

Publications

• Víctor Carreño, Evaluation, Analysis and Results of the DANTi Flight Test Data, the DAIDALUS Detect and Avoid Algorithm, and the DANTi Concept for Detect and Avoid in the Cockpit, Contractor Report, NASA/CR-20205004594, August 2020. BibTeX Reference.
• Víctor Carreño, María Consiglio, and César Muñoz, Analysis and Preliminary Results of a Concept for Detect and Avoid in the Cockpit, Proceedings of the 38th Digital Avionics Systems Conference (DASC 2019), San Diego, California, US, 2019. BibTeX Reference.
• Anthony Narkawicz, César Muñoz, and Aaron Dutle, Sensor Uncertainty Mitigation and Dynamic Well Clear Volumes in DAIDALUS, Proceedings of the 37th Digital Avionics Systems Conference (DASC 2018), London, England, UK, 2018. BibTeX Reference.
• James Chamberlain, María Consiglio, and César Muñoz DANTi: Detect and Avoid iN The Cockpit, Proceedings of the 17th AIAA Aviation Technology, Integration, and Operations Conference (ATIO 2017), AIAA-2017-4491, 2017. BibTeX Reference.
• Rania W. Ghatas, Devin P. Jack, Dimitrios Tsakpinis and Michael J. Vincent, James L. Sturdy, César A. Muñoz, Keith D. Hoffler, Aaron M. Dutle, Robert Myer, Anna M. DeHaven and Tod Lewis, and Keith E. Arthur, Unmanned Aircraft Systems Minimum Operational Performance Standards End-to-End Verification and Validation (E2-V2) Simulation, Technical Memorandum, NASA/TM-2017-20780, January 2017. BibTeX Reference.
• César Muñoz, Aaron Dutle, Anthony Narkawicz, and Jason Upchurch, Unmanned Aircraft Systems in the National Airspace System: A Formal Methods Perspective, ACM SIGLOG News, Vol. 3. Number 3, pp. 67-76, 2016. BibTeX Reference.
• César Muñoz and Anthony Narkawicz, Formal analysis of extended well-clear boundaries for unmanned aircraft, Proceedings of the 8th NASA Formal Methods Symposium (NFM 2016), Lecture Notes in Computer Science, Vol. 9690, pp. 221-226, 2016. BibTeX Reference.
• James Comstock, Rania Ghatas, Michael Vincent, María Consiglio, César Muñoz, James Chamberlain, Paul Volk, and, Keith Arthur, Unmanned Aircraft Systems Human-in-the-Loop Controller and Pilot Acceptability Study: Collision Avoidance , Self-Separation, and Alerting Times (CASSAT), Technical Memorandum, NASA/TM-2016-219181, April 2016. BibTeX Reference.
• Formal Methods in Air Traffic Management: The Case of Unmanned Aircraft Systems (Invited Lecture), Proceedings of the 12th International Colloquium on Theoretical Aspects of Computing (ICTAC 2015), Lecture Notes in Computer Science, Vol. 9399, pp. 58-62, 2015. BibTeX Reference.
• César Muñoz, Anthony Narkawicz, George Hagen, Jason Upchurch, Aaron Dutle, María Consiglio, and James Chamberlain, DAIDALUS: Detect and Avoid Alerting Logic for Unmanned Systems, Proceedings of the 34th Digital Avionics Systems Conference (DASC 2015), Prague, Czech Republic, 2015. BibTeX Reference.
• María Consiglio, César Muñoz, George Hagen, Anthony Narkawicz, Jason Upchurch, James Comstock, Rania Ghatas, Michael Vincent, and James Chamberlain, Human-In-The-Loop Experimental Research for Detect and Avoid, Proceedings of the 34th Digital Avionics Systems Conference (DASC 2015), Prague, Czech Republic, 2015. BibTeX Reference.
• Jason Upchurch, César Muñoz, Anthony Narkawicz, María Consiglio, and James Chamberlain, Characterizing the Effects of a Vertical Time Threshold for a Class of Well-Clear Definitions, Air Traffic Control Quarterly, Vol 23(4) pp. 275-299, 2015. BibTeX Reference. Also appeared as Jason Upchurch, César Muñoz, Anthony Narkawicz, María Consiglio, and James Chamberlain, Characterizing the Effects of a Vertical Time Threshold for a Class of Well-Clear Definitions (Best paper of track award), Proceedings of the 11th USA/Europe Air Traffic Management R&D Seminar, ATM 2015, Lisbon, Portugal, 2015. BibTeX Reference.
• James R. Comstock, Jr., Rania W. Ghatas, Maria C. Consiglio, James P. Chamberlain, and Keith D. Hoffler UAS Air Traffic Controller Acceptability Study 2: Evaluating Detect and Avoid Technology and Communication Delays in Simulation, Technical Memorandum, NASA/TM-2015-218989, November 2015.
• James Chamberlain, María Consiglio, James Comstock, Rania Ghatas, and César Muñoz, NASA Controller Acceptability Study 1 (CAS-1) Experiment Description and Initial Observations, Technical Memorandum, NASA/TM-2015-218763, May 2015. BibTeX Reference.
• Jason Upchurch, César Muñoz, Anthony Narkawicz, James Chamberlain, and María Consiglio, Analysis of Well-Clear Boundary Models for the Integration of UAS in the NAS, Technical Memorandum, NASA/TM-2014-218280, June 2014. BibTeX Reference.
• César Muñoz, Anthony Narkawicz, James Chamberlain, María Consiglio, and Jason Upchurch, A Family of Well-Clear Boundary Models for the Integration of UAS in the NAS, Proceedings of the 14th AIAA Aviation Technology, Integration, and Operations (ATIO) Conference, AIAA-2014-2412, Atlanta, Georgia, 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, August 2013. BibTeX Reference.
• María Consiglio, James Chamberlain, César Muñoz, and Keith Hoffler, Concept of integration for UAS operations in the NAS, Proceedings of the 28th International Congress of the Aeronautical Sciences (ICAS 2012), 2012. BibTeX Reference.

The tag identifies links that are outside the NASA domain