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 ?
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.
Its advanced next-generation tools, including the Clover parasitic extraction tool suite, the ATTSIM mixed-signal simulator, and now the FormalCheck model checker, come from research performed at Bell Laboratories.

Full browser ?