Formal Methods Research in Support of the Next Generation Air Transportation System

Опубликовано 6 сентября 2016, 17:17

This talk will provide an overview of the formal methods research conducted at NASA Langley and the National Institute of Aerospace (NIA) in support of the Next Generation of Air Transportation Systems (NGATS). NGATS is a possible implementation of the Vision 100 Century of Aviation Reauthorization Act in Dec 2003, which calls for a major transformation of the nation's air transportation system that will enable growth to 3 times the traffic of the current system. The transformation will require an unprecedented level of safety-critical automation used in complex procedural operations that enable distributed air/ground traffic management concepts. The goal of our formal methods research is to provide verification methods that can be used to insure the safety of the NGATS system. Our work has focused on the safety assessment of concepts of operation and fundamental algorithms for conflict detection and resolution. Formal analysis of a concept of operations is a novel area of application of formal methods. Here one must establish that a system concept involving aircraft, pilots, and ground resources is safe. The formal analysis of algorithms is a more traditional endeavor. It involves reasoning about the interaction of algorithmic logic and physical constraints, e.g., aircraft trajectories on a 3-D space. The verification challenge is to establish that the safety-critical algorithms produce valid solutions that are guaranteed to maintain air traffic separation under all possible scenarios. In this talk, we will illustrate our formal methods research with two examples: NASA's Small Aircraft Transportation System (SATS), an operational concept for use at non-radar, non-towered airports, and NIA's KB3D, a distributed conflict detection and resolution algorithm. All of the formal developments were accomplished using the Prototype Verification System (PVS).