NASA Logo

NTRS

NTRS - NASA Technical Reports Server

Collections About News Help Login
Back to Results
How Formal Methods Impels Discovery: A Short History of an Air Traffic Management ProjectIn this paper we describe a process of algorithmic discovery that was driven by our goal of achieving complete, mechanically verified algorithms that compute conflict prevention bands for use in en route air traffic management. The algorithms were originally defined in the PVS specification language and subsequently have been implemented in Java and C++. We do not present the proofs in this paper: instead, we describe the process of discovery and the key ideas that enabled the final formal proof of correctness
Document ID
20100018537
Acquisition Source
Langley Research Center
Document Type
Conference Paper
Authors
Butler, Ricky W. (NASA Langley Research Center Hampton, VA, United States)
Hagen, George (NASA Langley Research Center Hampton, VA, United States)
Maddalon, Jeffrey M. (NASA Langley Research Center Hampton, VA, United States)
Munoz, Cesar A. (NASA Langley Research Center Hampton, VA, United States)
Narkawicz, Anthony (NASA Langley Research Center Hampton, VA, United States)
Dowek, Gilles (Ecole Polytechnique Palaiseau, France)
Date Acquired
August 24, 2013
Publication Date
April 1, 2010
Publication Information
Publication: Proceedings of the Second NASA Formal Methods Symposium
Subject Category
Mathematical And Computer Sciences (General)
Meeting Information
Meeting: NASA Formal Methods Symposium
Location: Washington D.C.
Country: United States
Start Date: April 13, 2010
End Date: April 15, 2010
Sponsors: NASA Headquarters
Distribution Limits
Public
Copyright
Public Use Permitted.

Related Records

IDRelationTitle20100018529Collected WorksProceedings of the Second NASA Formal Methods Symposium
No Preview Available