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.
Unmanned Aircraft Systems in the National Airspace System: A Formal Methods Perspective
2016
10 pages
Report
No indication
English
Computer Software , Unmanned aircraft systems , National airspace system , Safety , Air traffic control , Formalism , Algorithms , Computer programming , Program verification (computers) , Detection , Collision avoidance , Mathematical models , Airspace , Situational awareness , Functional design specifications , Systems integration , Nasa programs