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 objectives, activities, and software life cycle data that should be addressed when formal methods are used as part of the software development process. This includes artifacts that would be expressed using some formal notation and the verification evidence that could be derived from them.
This NASA-funded project developed three case studies describing the use of different classes of formal methods to satisfy DO-178C certification objectives. 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.
The three case studies illustrate the use of theorem proving, model checking, and abstract interpretation. Each of these techniques has strengths and weaknesses, and each could be applied to different life cycle data items and different objectives than those described here. The purpose here is to illustrate a reasonable application of each of these techniques for satisfying certification objectives.
The case studies examine different aspects of a common avionics example – a dual-channel Flight Guidance System (FGS). While not intended to be a complete example, it is representative of the issues encountered in actual avionics development projects and includes design artifacts specified using PVS, MathWorks Simulink/Stateflow®, and C source code. These files and the full technical report are available for download and use without restriction.