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 developped 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
  • DAIDALUS (Detect and Avoid Alerting Logic for Unmanned Systems), a collection of formally verified detect and avoid algorithms for Unmanned Aircraft Systems,
  • ACCoRD (Airborne Coordinated Conflict Resolution and Detection), a formal framework for the development of state-based separation assurance systems, and
  • Formally Verified and Partially Verified Software Modules
  • Early Air Traffic Management Research
• Verification Tool Research
  • Kodiak, a software library for the solution of numerical, possibly non-linear, problems over hyper-rectangular variable and parameter domains.
  • PVS Theorem Prover Related Research
  • PVSio
• Using Formal Methods in Certification
  • DO-333 Case Studies
  • Qualification of Formal Methods Tools under DO-330
    • Study by Rockwell Collins
    • Study by Kestrel Technology
• Spacecraft Autonomy and AI Planning
• Certification Oriented Software Research
• Accident Analysis
• Avionics Software Verification and Validation
• Fault Tolerance

Papers, Presentations, and Downloads

• Publications
• NASA Langley FM Workshops
• PVS Libraries

Past Research Projects

• Past Programs
• Early Projects

The tag identifies links that are outside the NASA domain