Understanding Formal Methods for Use in DO-254 Programs
White Paper
ABSTRACT
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. This paper is a companion to the presentation on this topic presented at the 2009 FAA SW and AEH conference.
Related Resources
Safety-critical Applications and xtUML
On-demand Web Seminar 35:15Safety-critical Applications and xtUML
Interest in adopting modeling practices is very high in domains requiring safety-critical design practices. In this presentation, the capabilities of BridgePoint and ReqTracer, two products from Mentor...
Explore the True Potential of Your FPGA Design
On-demand Web Seminar 19:27Explore the True Potential of Your FPGA Design
In this seminar, you’ll discover how to leverage FPGA Precision Synthesis technology to find the true potential of your design.
First time’s a charm for FPGA verification at Lockheed Martin Space Systems Company
Lockheed Martin uses SystemVerilog, OVM and Mentor Graphics tools for first-pass FPGA verification success