Glossary · Automation software engineering and architecture
Model checking
German: Modellprüfung
In formal verification, model checking is an automated technique that explores all reachable states of a finite model of a system to determine whether it satisfies a formally specified property, and produces a counterexample if it does not.
- Software engineering
- Functional safety
In one sentence
Model checking automatically explores all reachable states of a system model to prove a formal property or find a counterexample.
Example
Engineers model the interlocking logic of a press as a state machine and use a model checker to show that the ram can never move while the guard door is open.
How it applies
- Engineering: Model checking suits control logic with many combinations of states, such as interlocks, sequences and protocols, where tests cannot cover every case. Its limit is state explosion: large models must be abstracted.
- Functional safety: IEC 61508 lists formal methods among techniques that can be used for higher integrity levels. A proof only covers the model and the property stated; it says nothing about hardware faults or a wrong specification.
- Documentation: Record the model, its assumptions and abstractions, the properties checked, the tool and version and the results as Safety evidence or verification records.
Model checking vs. testing
Testing runs selected cases on the real or simulated system. Model checking covers all states of the model, but only of the model. The two complement each other in Verification.