Mentor Graphics

The purpose of this paper was to explain formal methods to both certification authorities and potential applicants who could benefit from its use. Formal Verification is one of the most misunderstood areas of DO-254. It is also one of the few actual design or verification methods named in the RTCA/DO-254 document (Appendix B) and is in fact listed as an appropriate method for the "Advanced Verification" requirements for Level A/B designs. The problem is that the content of Appendix B is extremely difficult to understand. This has resulted in an undue amount of misunderstanding and confusion, and has unfortunately caused many engineers and certification authorities alike to be discouraged or discouraging in terms of the use of formal methods on DO-254 programs.