Testing or Formal Verification: DO-178C Alternatives and Industrial Experience looks at how to use formal verification instead of testing of software in civilian airplanes (for which DO-178C applies). It is based on the experience of Airbus and Dassault-Aviation in the application of formal verification with the Frama-C platform. In particular it describes:
- What the avionics certification standard DO-178C asks in replacement for test coverage, which does not apply when one uses formal verification instead of testing.
- How formal verification tools can help with these alternate objectives.
- The solutions that Airbus and Dassault-Aviation have implemented to cover these objectives.
This paper is copyrighted by IEEE, and reproduced here with their permission. You can also access it on the IEEE Software website.