Description
Source: Qualification of a Model Checker for Avionics Verification
The publication of DO-178C and the accompanying formal methods supplement DO-333 provide guidance for aircraft manufacturers and equipment suppliers who wish to obtain certification credit for the use of formal methods for software development and verification. However, there are still a number of issues that must be addressed before formal methods tools can be injected into the design process for avionics
systems. DO-178C requires that a tool used to meet certification objectives be qualified to demonstrate that its output can be trusted. The qualification of formal methods tools is a relatively new concept presenting unique challenges for both formal methods researchers and software developers in the aerospace industry.
One of the foundational principles of DO-178C is requirements-based testing. This means that the verification activities are centered around explicit demonstration that each requirement has been met. A second principle is complete coverage, both of the requirements and of the code that implements them. This means that every requirement and every line of code must be examined in the verification process. Furthermore, several metrics are defined which specify the degree of structural coverage that must be obtained in the verification process, depending on the criticality of the software being verified. A third principle is traceability among all of the artifacts produced in the development process.
- RTCA DO-178C: Software Considerations in Airborne Systems and Equipment Certification, Washington, DC. (2011)
- RTCA DO-333: Formal Methods Supplement to DO-178C and DO-278A, Washington, DC. (2011)
- RTCA DO-330: Software Tool Qualification Considerations, Wash., DC. (2011)
https://en.wikipedia.org/wiki/DO-178C