shemesh.larc.nasa.gov

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 Detection): Formal framework for the development of state-based separation assurance systems.
    • 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 systems, 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): Assistive Detect and Avoid technology 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 aircraft applications.
    • PolyCARP: Library of formally verified algorithms and software for computations with polygons.
    • SIRIUS (Simulation Infrastructure for Research on Interoperating Unmanned Systems): Research framework for simulation and analysis of future concepts for Urban Air Mobility (UAM) operations.
    • Early Air Traffic Management Research
  • Verification Tool Research
  • 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

The tag [*] identifies links that are outside the NASA domain