Events

Formal Methods Research in Support of the Next Generation Air Transportation System
Cesar Munoz
National Institute of Aerospace, NASA Langley,July 21, 2008, 11h-12h,
MSR-INRIA Joint Centre,
Parc Orsay Université - Batiment I.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, which calls for a major transformation of the nation’s air transportation system. This transformation will require an unprecedented level of safety-critical systems that rely on distributed air/ground traffic management concepts.

The goal of our formal methods research is to provide verification methods that can be used to ensure the safety of the NGATS system. We will illustrate our approach by presenting the verification of a 3-dimensional conflict detection and resolution algorithm for distributed air traffic management. This verification involves reasoning about the interaction of algorithmic logic and physical constraints, e.g., aircraft trajectories on a 3-D space. The verification objective is to establish that all conflicts are detected and that the resolution maneuvers keep aircraft safely separated. This formal development has been mechanically verified in the Prototype Verification System (PVS).