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.
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.
Wagner, Lucas, Alain Mebsout, Cesare Tinelli, Darren Cofer, and Konrad Slind. "Qualification of a Model Checker for Avionics Software Verification.
https://en.wikipedia.org/wiki/DO-178C
Formal Methods Tool Qualification - NASA Technical Report
Formal Methods Case Studies for DO-333