An article which I co-authored was just published in the May-June special issue of IEEE Software on Safety-Critical Software. It’s called Testing or Formal Verification: DO-178C Alternatives and Industrial Experience, and it talks about how to use formal verification instead of testing for 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.
- 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.
We’ll be happy to get some feedback from others! Please comment. This paper is copyrighted by IEEE, and reproduced here with their permission. You can also access it on IEEE Software website.