Model checking is a computer-aided verification method developed to formally
verify the correct functioning of a system design model by examining all of
its possible behaviours. The models used in model checking are quite similar
to those used in simulation, as basically the model must describe the
behaviour of the system design for all sequences of inputs. However, unlike
simulation, model checkers examine the behaviour of the system design with all
input sequences and compare it with the system specification.
In model checking, at least in principle, the analysis can be fully automated
with computer-aided tools. The specification is expressed in a suitable
specification language, temporal logics being a prime example, describing the
allowed behaviours of a system. Given a model and a specification as inputs, a
model checking algorithm decides whether the system violates its specification
or not. If none of the behaviours of the system violate the given
specification, the (model of the) system is correct. Otherwise, the model
checker will automatically give a counter-example execution of the system
demonstrating why the property is violated.