Model checking is a formal verification technique used in computer science and systems engineering to systematically explore the states of a finite system model to verify whether certain properties hold. It is often applied to hardware and software systems, where the goal is to ensure that the system behaves correctly under all possible scenarios. Key components of model checking include: 1. **Model**: The system being verified is represented as a mathematical model. This model typically captures the system's states, transitions, and behaviors.
Articles by others on the same topic
Model checking verifies whether a formally represented system satisfies a specified property, often a temporal logic formula over a finite transition system. A safety question asks whether a bad state is reachable; exhaustive state exploration can either find a counterexample path or establish its absence in the model. Symbolic model checking represents sets of states compactly, while bounded methods search executions up to a chosen horizon. Verification is relative to the model and assumptions: a missing physical behaviour is not ruled out merely because it was omitted from the transition relation.[ref]
https://www.cs.cmu.edu/~modelcheck/. CMU model-checking group, finite-state verification and temporal specifications