Unmanned aircraft systems in the national airspace system
- 8 August 2016
- journal article
- research article
- Published by Association for Computing Machinery (ACM) in ACM SIGLOG News
- Vol. 3 (3), 67-76
- https://doi.org/10.1145/2984450.2984459
Abstract
As the technological and operational capabilities of unmanned aircraft systems (UAS) have grown, so too have international efforts to integrate UAS into civil airspace. However, one of the major concerns that must be addressed in realizing this integration is that of safety. For example, UAS lack an on-board pilot to comply with the legal requirement that pilots see and avoid other aircraft. This requirement has motivated the development of a detect and avoid (DAA) capability for UAS that provides situational awareness and maneuver guidance to UAS operators to aid them in avoiding and remaining well clear of other aircraft in the airspace. The NASA Langley Research Center Formal Methods group has played a fundamental role in the development of this capability. This article gives a selected survey of the formal methods work conducted in support of the development of a DAA concept for UAS. This work includes specification of low-level and high-level functional requirements, formal verification of algorithms, and rigorous validation of software implementations.Keywords
This publication has 14 references indexed in Scilit:
- Affine Arithmetic and Applications to Real-Number ProvingPublished by Springer Science and Business Media LLC ,2015
- Software Validation via Model AnimationPublished by Springer Science and Business Media LLC ,2015
- Formally-Verified Decision Procedures for Univariate Polynomial Computation Based on Sturm’s and Tarski’s TheoremsJournal of Automated Reasoning, 2015
- Defining Well Clear for Unmanned Aircraft SystemsPublished by American Institute of Aeronautics and Astronautics (AIAA) ,2015
- A Family of Well-Clear Boundary Models for the Integration of UAS in the NASPublished by American Institute of Aeronautics and Astronautics (AIAA) ,2014
- Automated Real Proving in PVS via MetiTarskiLecture Notes in Computer Science, 2014
- A Formally Verified Generic Branching Algorithm for Global OptimizationLecture Notes in Computer Science, 2014
- Formalization of Bernstein Polynomials and Applications to Global OptimizationJournal of Automated Reasoning, 2012
- UAS Integration into the National Airspace System: Modeling the Sense and Avoid ChallengePublished by American Institute of Aeronautics and Astronautics (AIAA) ,2009
- Sense and Avoid System for a MALE UAVPublished by American Institute of Aeronautics and Astronautics (AIAA) ,2007