Formal Methods for Aviation Safety

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 software safety critical systems. Current research efforts focus on the verification of Air Traffic Managment Systems.

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.

News from FM@NIA

• PVS Class 2005, May 24-27, Hampton, VA

Olds from FM@NIA

• First International Workshop on Design and Application of Strategies/Tactics in Higher Order Logics, STRATA2003
• TPHOLs 2002 in Hampton, Virginia

Research

Research Team

• NIA Staff Scientists
• NASA Civil Servants

Publications

• Recent Publications

Links

• Formal Methods at NASA
  • Langley Formal Methods Program
  • Ames Automated Software Engineering Group
  • Formal Methods Guidebook
  • JPL's Formal Methods Page
• Formal Methods in the World
  • The World Wide Web Virtual Library: Formal Methods
• Aviation Safety at NASA