CAREER: Theoretical Foundations of the UAS in the NAS Problem

Due to increasing use by civil and federal authorities and vast commercial and amateur applications, Unmanned Aerial Systems (UAS) will be introduced into the National Air Space (NAS); the question is only how we can do this safely. NASA and the FAA are designing a new automated air traffic control system (NextGen) for all aircraft, manned or unmanned. New algorithms and tools need to be developed to enable computation of the complex questions inherent in designing such a system while proving adherence to rigorous safety standards. We must grow the tools of formal analysis to be able to address the UAS in the NAS problem, reason about UAS integration during the design phase of NextGen, and tie this design to on-board capabilities to provide runtime System Health Management (SHM), ensuring the safety of people and property. To address the UAS in the NAS problem, we take a holistic view, integrating advances in the state of the art from three intertwined perspectives: on-board the UAS, the environment (NAS), and the underlying theory enabling their formal analysis. Despite advances in formal methods, few are grounded in real-world avionics systems. There has been rapid development of UAS technologies yet few of them are formally mathematically rigorous to the degree needed for FAA safety-critical system certification. This CAREER proposal bridges that gap, integrating new UAS and air traffic control designs with advances in formal analysis. In the wealth of promising directions for autonomous UAS capabilities, this CAREER proposal fills a unique need, providing a direct synergy between on- board UAS SHM, the NAS environment in which they operate, and the theoretical foundations common to both of these.