Glossary · Automation software engineering and architecture
Formal verification
Also known as: Formal methods verification
German: Formale Verifikation
In software and systems engineering, formal verification is the use of mathematical methods, such as model checking, theorem proving or abstract interpretation, to prove or disprove that a system or its model satisfies a formally specified property for all possible inputs and states within the analyzed scope.
- Software engineering
- Functional safety
In one sentence
Formal verification uses mathematical methods such as model checking to prove that a system satisfies specified properties for all inputs.
Example
A model checker proves that the interlocking logic of a press can never command the ram down while the guard-closed signal is false, for all input sequences in the model.
How it applies
- Engineering: Formal methods find defects that testing misses, because they cover all behaviors within the model rather than selected test cases. They are used for protocols, interlocking logic, state machines and safety-critical algorithms, and some tools analyze PLC code directly.
- Functional safety: IEC 61508 lists formal methods among the techniques recommended for higher safety integrity levels. The results are only as good as the formal specification and the model; errors in either are not detected by the proof.
- Documentation: Record the properties proven, the model or code version, tool and assumptions. The assumptions, such as input behavior or timing, must be stated clearly, because they limit what the proof shows.
Formal verification vs. testing
Testing shows that a system behaves correctly for the cases tried. Formal verification shows that a property holds for all cases within the model. It complements rather than replaces testing, and it does not replace Validation, which asks whether the specified properties are the right ones.