NASA Langley Formal Methods Research Program
The NASA Langley's Formal Methods Research Program of the NASA Langley Safety-Critical Avionics Systems Branch develops formal methods technology for the
development of mission-critical and safety-critical digital systems of interest to NASA.
These types of systems are being developed in support of the following NASA strategic initiatives:
- Sustainable air transportation system vehicle and airspace technologies
- Concepts and technologies to enable 100X capacity using trajectory-based operations (TBO)
If you are not familiar with
formal methods, you might want
to start your exploration by visiting our pages that
try to answer the questions,
Why is Formal Methods Necessary? and
What is Formal Methods?
Research Project Areas
- Air Traffic Management Research
- ACCoRD (Airborne Coordinated Conflict Resolution and
Formal framework for the development of state-based separation
- CPR (Compact Position Reporting):
Formal analysis of the CPR algorithm, which is a safety-critical element of the Automatic Dependent Surveillance - Broadcast (ADS-B) protocol.
- DAA-Displays: Library of
interactive graphical display elements (widgets) for cockpit
and simulations tools supporting comparative analysis of cockpit displays.
- DAIDALUS (Detect and Avoid Alerting Logic for
Unmanned Systems): Library of formally verified
detect and avoid algorithms for Unmanned Aircraft Systems.
- DANTi (Detect and Avoid in the
Cockpit): Detect and avoid safety enhancement concept for manned aircraft.
- ICAROUS (Independent Configurable Architecture for Reliable Operations of Unmanned Systems): On-board software architecture that enables the robust
integration of mission specific software modules and highly assured
core software modules for building autonomous unmanned
- PolyCARP: Library of formally verified
algorithms and software for computations with polygons.
- Early Air Traffic Management Research
- Verification Tool Research
- PVS Theorem Prover Related
- Kodiak: Software library
for the solution of numerical, possibly non-linear, problems
over hyper-rectangular variable and parameter domains.
- MINERVA (Mirrored Implementation Numerically Evaluated against Rigorously Verified Algorithms):
Practical, but rigorous, approach to the
development of safety-critical numerical software components.
- Plaidypvs: A formal embedding of differential dynamic logic in the Prototype Verification System (PVS).
- PLEXIL: Formal semantics and verification
environment of NASA's
Plan Execution Interchange Language (PLEXIL).
- PRECiSA (Program Round-off Error Certifier via Static Analysis): Fully automatic analyzer for the estimation of round-off errors of floating-point valued functional expressions.
- VSCode-PVS: Modern IDE for PVS based on Visual Studio Code.
Using Formal Methods in Certification
- Spacecraft Autonomy and AI Planning
- Certification Oriented Software Research
- Accident Analysis
- Avionics Software Verification and Validation
- Fault Tolerance
Papers, Presentations, and Downloads
Past Research Projects
identifies links that are outside
the NASA domain