NASA logo

+ Contact NASA

  • + HOME
  • + TEAM
  • + LINKS

  • DO-333 Case Studies

    The arrival of RTCA DO-333 has greatly improved the prospects for using formal methods technology to create certification evidence. At the same time, the expectation is that additional guidance beyond DO-333 will be needed to infuse formal methods into the development and certification workflows for civil aviation. In response to this need, a study task was issued in 2012 by NASA Langley Research Center. Awarded to Boeing and Rockwell Collins, this study had the goal of creating guidance material to help smooth the introduction of formal methods into relevant software practices. The main result from that effort is the following case studies report, intended as an aid to applicants and certification authorities alike.


    RTCA DO-333, Formal Methods Supplement to DO-178C and DO-278A provides guidance for software developers wishing to use formal methods in the certification of airborne systems and air traffic management systems. The supplement identifies the modifications and additions to DO-178C and DO-278A objectives, activities, and software life cycle data that should be addressed when formal methods are used as part of the software development process. This report presents three case studies describing the use of different classes of formal methods to satisfy certification objectives for a common avionics example ‐ a dual-channel Flight Guidance System. The three case studies illustrate the use of theorem proving, model checking, and abstract interpretation. The material presented is not intended to represent a complete certification effort. Rather, the purpose is to illustrate how formal methods can be used in a realistic avionics software development project, with a focus on the evidence produced that could be used to satisfy the verification objectives found in Section 6 of DO-178C.



    This report was the work of Darren Cofer and Steven Miller, along with contributions from several other staff members at Rockwell Collins.

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