model checking

(redirected from Model-checking)

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].
References in periodicals archive ?
Furthermore, we will apply our methods to two specific applicationareas, model-checking in computer-aided verification and inferenceproblems in Bayesian networks.
Holzmann is being recognized "for fundamental contributions to improving software quality, in particular through model-checking tools and coding standards, and for successfully transferring these contributions to practitioners developing mission-critical software.
Verification of Communication Protocols in Web Services: Model-Checking Service Compositions
Chapters cover models for real-time embedded systems, timed model-checking, control and fault diagnosis of timed systems, quantitative verification of Markov chains, tools for model-checking timed systems, and tools for the analysis of hybrid models.
Developed in cooperation with the industry's leading manufacturers, HyperCrash increases departmental efficiency and results accuracy through process-driven workflows and automated model-checking and correction.
Program analysis and model-checking techniques could also be developed to prevent error from occurring in voting software.
These accomplished researchers have been recognized with the highest honor in the area of computing for their role in developing Model-Checking into a highly effective verification technology, widely adopted in the hardware and software industries.
Motivated especially by applications to software model checking (more specifically the termination of linear loops and predicate abstraction computations), as well as parametric real-time reasoning and the verification of Markov chains, we will focus on model-checking, module-checking, and synthesis problems for linear dynamical systems and one-counter automata against various fragments and extensions of Linear Temporal Logic (LTL) specifications.
Extending the 2007 Turing Award winning Model-checking that transformed quality assurance in the semiconductor chip industry
The new model-checking features for these important safety-critical standards extend the existing support available within Simulink Verification and Validation for customer-developed modeling guidelines.
After SVA syntax and semantics are covered, assertion-based verification techniques are explained, as are model-checking techniques.
imPROVE-HDL is a model-checking tool that uses formal methods to quickly and formally validate properties on VHDL/Verilog RTL and structural models.

Full browser ?