model checking

Also found in: Wikipedia.

model checking

(theory, algorithm, testing)
To algorithmically check whether a program (the model) satisfies a specification.

The model is usually expressed as a directed graph consisting of nodes (or vertices) and edges. A set of atomic propositions is associated with each node. The nodes represents states of a program, the edges represent possible executions which alters the state, while the atomic propositions represent the basic properties that hold at a point of execution.

A specification language, usually some kind of temporal logic, is used to express properties.

The problem can be expressed mathematically as: given a temporal logic formula p and a model M with initial state s, decide if M,s \models p.

["Automatic verification of finite state concurrent systems using temporal logic", E.M. Clarke, E.A. Emerson, and A.P. Sisla, ACM Trans. on Programming Languages and Systems 8(2), pp. 244--263, 1986].
This article is provided by FOLDOC - Free Online Dictionary of Computing (
References in periodicals archive ?
Given a finite state system, the symbolic model checking method starts with the construction of the OBDD for the transition relations TR(V, V').
Model checking is a formal method used for the verification of finite-state systems.
There are five steps in Box Jenkins method: removal of non-stationery components, identification model, parameter estimation, model checking and forecasting.
A step-by-step method is proposed to translate the cause-effect tables in finite state machines, which are then submitted to formal verification in the UPPAAL model checking tool.
Then, using model checking technique for timed automata, the verification could be done using reachability analysis.
Most of above researches concentrate on protocols of e-commerce and model checking of such transaction properties as atomicity, but the validations of protocols are not sufficient to ensure the integrity and reliability of e-commerce systems because there are still many defects and logic errors at the design level of business processes, which can be exploited by malicious clients.
Besides the satisfiability problem, model checking (MC) is another important computational problem.
Already highly popular in the USA, VDC services offer third-party laser scanning, 3D modelling and model checking capabilities and expertise to anyone wishing to buy-in expertise or build upon its existing in-house capabilities in order to win bigger and better contracts without the need for upfront investment in either hardware or training.
Formal Methods, and in particular Model Checking, are seeing an increasing use in the Aerospace domain.
These include control of discrete event systems [2], realizability and synthesis, model checking [3], planning [4], [mu]-calculus [5-6], and the analysis of systems where the distinction among the choices controlled by different components are made explicit.
Model Checking is vital to safeguard the manufacturability & quality of products.

Full browser ?