Airspace Research: Formal Methods
Objectives
- 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
Client
NASA Langley Research Center
Participants / Collaborators
National Institute of Aerospace
