Model checking

This article is about checking of models in computer science. For the checking of models in statistics, see statistical model validation.
Elevator control software can be model-checked to verify both safety properties, like "The cabin never moves with its door open",[1] and liveness properties, like "Whenever the nth floor's call button is pressed, the cabin will eventually stop at the nth floor and open the door".

In computer science, model checking or property checking is a method for checking whether a finite-state model of a system meets a given specification (also known as correctness). This is typically associated with hardware or software systems, where the specification contains liveness requirements (such as avoidance of livelock) as well as safety requirements (such as avoidance of states representing a system crash).

In order to solve such a problem algorithmically, both the model of the system and its specification are formulated in some precise mathematical language. To this end, the problem is formulated as a task in logic, namely to check whether a structure satisfies a given logical formula. This general concept applies to many kinds of logic and many kinds of structures. A simple model-checking problem consists of verifying whether a formula in the propositional logic is satisfied by a given structure.

  1. ^ For convenience, the example properties are paraphrased in natural language here. Model-checkers require them to be expressed in some formal logic, like LTL.