model checking

(redirected from Model checkers)

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 ?
The application of model checking to Cyber Physical Systems (CPS) including physical, control and communication systems, has received much attention, such as the focus on hybrid systems verification [9], as well as the use of probabilistic model checkers (e.
Most of these challenges stem from the complexity growth [7] that hampers the efficiency of model checkers, as well as the inherent use of model abstractions of complex dynamics.
These proofs could be performed automatically, using model checkers, or interactively through proof tools.
There are a number of integrated tools in the Rodin platform including theorem provers and model checkers.
To answer the third question, we will design suitable translations to related logical formalisms, for which optimized model checkers and theorem provers exist.
Although testing is still the most important part of software development, issues like automatic testing, requirement or specification verification can now be reached through model checkers.
Besides that, model checkers can only produce finite representation of model behavior due to the problem known as 'state explosion'.
These provide the section headings for the 48 papers presented, which examine such topics as modeling and verification for the compatibility of software components, similarities and differences in information security systems versus critical information infrastructure protection systems, bandwidth control in redundant news server links, model-based automatic test generation for event-driven embedded systems using model checkers, crypto- computing approach to protecting interaction protocols of mobile agents from malicious host attack, and self-dual modules in design of dependable digital devices, to name a few examples.
Today it is standard practice for hardware engineers to use OBDD-based equivalence checkers, and symbolic model checkers.
0-In Confirm has a much greater capacity than traditional model checkers, so the designer can run it on an entire chip sub-section and not just on individual blocks.
Under the terms of the agreement, TransEDA has licensed a state space exploration tool kit that may be used to build model checkers, simulators, static debuggers, symbolic simulators and other tools.
BUSINESS WIRE)--April 8, 1997--Lucent Technologies' Bell Labs Design Automation (BLDA) group today announced the release of FormalCheck, the first in a family of comprehensive system-level model checkers.

Full browser ?