Model checking is the collection of methods for analyzing an abstract representation of a system to determine the validity of one or more properties of interest. Much specifically, it has been defined as an algorithmic formal verification technique for finite-state, concurrent systems (Clarke, Emerson, and Sistla 1986; Queille and Sifakis 1982; NASA 2004).
A concurrent system can be modeled by a finite-state machine represented as a directed graph consisting of:
a) nodes, which represent the states of the system, and
b) edges, which represent transitions between states
In theory, a model checker can exhaustively search the entire state space of the system and verify whether certain properties are satisfied. A property is a predicate on a system state or states, and is usually expressed as a logical specification such as a propositional temporal logic formula. If the system satisfies the property, the model checker typically generates a confirmation response; otherwise, it produces a trace (also called a counter illustration) that shows the violation of the property and the major events leading to that violation. Therefore, the model checker can be used both to prove correctness of the system behavior and to find bugs in the system.