David Landoll
Mentor Graphics

Formal Verification (a.k.a., Formal Methods) is one of the few technologies mentioned by the RTCA/DO-254 document. It is listed as an example of an acceptable method for Appendix B "Advanced Verification" requirements for level A/B designs. However, many people (hardware applicants and certification authorities alike) do not have a good understanding of what Formal Verification is, how it works, and how it can or should be used within DO-254 programs. Using simple language, analogies and examples, this paper introduces Formal Verification in the context of its use for DO-254 and/or safety-critical programs, taking the ambiguity out of this powerful verification method.