Model checking refers to the following problem: given a model of a system, test automatically whether this model meets a given specification.
Model checking refers to the following problem: given a model of a system, test automatically whether this model meets a given specification.
Typically, the systems one has in mind are hardware or software systems, and the specification contains safety requirements such as the absence of deadlocks and similar critical states that can cause the system to crash. Model checking is a technique for automatically verifying correctness properties of finite-state systems.
An important class of model checking methods have been developed for checking models of hardware and software designs where the specification is given by a temporal logic formula.
