Skip to Main Content
백서

Understanding formal verification methods for use in DO-254 programs

Formal explained for humans.

DO-254 defines a process that hardware vendors must follow to get their hardware certified for use in avionics.
This paper seeks to take the mystery out of the use of formal methods for hardware verification. 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 the 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.

Contrast this with commonly used simulation techniques, which is considered a “probabilistic” approach. This means the tool itself cannot guarantee that all undesirable behavior will be identified. It’s entirely up to the user to think of all possible undesirable behavior and test each one individually.

This is best explained with an analogy to doing a math problem. Consider solving the equation 2X² – 8X + 5 = 0 for X. You can brute force and estimate an answer by trying various combinations of X and narrowing down the possibilities. This is similar to how you’d write tests using a directed test simulation approach. Your attempts might look something like this. (X is the input, Y is the output. According to the above equation, we want Y to equal zero, so our challenge is to find the correct value of X).

공유