Formal Methods
The Formal Methods research program at the National Institute of Aerospace (NIA) aims at developing and applying techniques and tools for the specification, analysis, and verification of digital systems that are of interest to NASA. Application areas include flight guidance systems, integrated modular avionics, airborne information systems, and other hardware and softwaresafety critical systems. Current research efforts focus on the verification of the next generation of air traffic systems and supporting autonomy for spacecraft operations.
NIA’s Formal Methods program supports NASA Langley’s Formal Methods Group by developing and applying state-of-the-art formal technologies.
The Formal Methods Groups at NIA and NASA Langley have developed and verified several fundamental algorithms for Air Traffic Management such as Conflict Detection and Resolution (CD3D, KB3D), Resolution and Recovery (RR3D), and Cooperative and Collaborative Resolution.