Airspace Research: Formal Methods

Airspace Research: Formal Methods


  • Develop mathematical techniques for the specification and verification of the safety critical aspects of airspace systems
  • NextGen applications: conflict detection and resolution, safety buffers, position reporting

Why It Matters

  • Design errors and failures can have catastrophic consequences for safety-critical airspace systems
  • Formal Methods are geared to ensure the functional and operational correctness of systems

Recent Accomplishments

  • Development of mathematical tools aimed to the round-off error analysis of floating-point functions
  • Formal analysis of the Compact Position Reporting algorithm, part of the FAA NextGen’s protocol
  • Development and formal verification of decision making software infrastructure for Unmanned Aircraft Systems
  • Development of fundamental theorem proving technology related to complex data structure reuse, termination criteria, specification animation


NASA Langley Research Center

Participants / Collaborators

National Institute of Aerospace

Screen Shot 2017-04-27 at 4.43.42 PM