Understanding Formal Methods for Use in DO-254 Programs

Formal Verification is one of the most misunderstood areas of DO-254. It is 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. The text in this section was largely taken from texts or papers on formal methods intended more for the academic rather than today’s typical user. In addition, it is also too oriented towards formal verification for software. Add to this, the information is over 20 years old. This has resulted in fear (in the minds of the project team who wants to use it on their DO-254 programs but don’t want to increase their project’s scrutiny) and unease (for the certification authority who sees its use called out on a DO-254 program but does not really understand this use or its purpose).

This paper seeks to take the mystery out of the use of formal methods for hardware verification. In this discussion, we will first explain formal methods as clearly and concisely as possible. We will then look at the state of the industry and the changes over the last decade or so that have enabled the widespread use of formal methods for hardware verification. With this knowledge in-hand, we will examine and explain the contents of DO-254 Appendix B 3.3.3 “Formal Methods.” Finally, we will bring this information together and provide recommendations for using formal methods on a DO- 254 project.

Formal Methods Overview

Even though the practical application of formal methods was in its infancy during the original writing of DO-254, the authors of DO-254 certainly understood the potential of formal methods in terms of enhancing design assurance. This section provides some foundational information that can help you understand why the DO-254 authors felt formal methods were pertinent and useful in terms of aiding design assurance.

What are “Formal Methods”?

Formal methods make use of exhaustive mathematical algorithms to verify the functional correctness of a design against its requirements. Because the process is exhaustive, the verification answer to the question “does this design meet this requirement” is guaranteed to be complete. That is, if design can exhibit any undesirable behavior, formal methods will point them out. On the other hand, if formal can prove that no such undesirable behavior exists, then formal methods will say so.