Model checking

From Wikipedia, the free encyclopedia

Model checking is the process of checking whether a given model satisfies a given logical formula. The concept is general and applies to all kinds of logics and their models. A simple model-checking problem is testing whether a given formula in the propositional logic is satisfied by a given model.

An important class of model checking methods have been developed to algorithmically verify formal systems. This is achieved by verifying if the model, often derived from a hardware or software design, satisfies a formal specification, typically a temporal logic formula.

Model checking is most often applied to hardware designs. For software, because of undecidability (see Computability theory) the approach cannot be fully algorithmic; typically it may fail to prove or disprove a given property.

The model is usually given as a source code description in an industrial hardware description language or a special-purpose language. Such a program corresponds to a finite state machine, i.e., a directed graph consisting of nodes (or vertices) and edges. A set of atomic propositions is associated with each node, typically stating which memory elements are one. The nodes represent states of a system, the edges represent possible transitions which may alter the state, while the atomic propositions represent the basic properties that hold at a point of execution.

Formally, the problem can be stated as follows: given a desired property, expressed as a temporal logic formula p, and a model M with initial state s, decide if . If M is finite, as it is in hardware, model checking reduces to a graph search.

Model checking tools face a combinatorial blow up of the state-space, commonly known as the state explosion problem, that must be addressed to solve most real-world problems. There are several approaches to combat this problem.

1. Symbolic algorithms avoid ever building the graph for the FSM; instead, they represent the graph implicitly using a formula in propositional logic. The use of binary decision diagrams (BDDs) was made popular by the work of Ken McMillan (1992). More recently, SAT solvers (see Boolean satisfiability problem) have been used to perform the graph search.
2. Partial order reduction can be used (on explicitly represented graphs) to reduce the number of independent interleavings of concurrent processes that need to be considered. The basic idea is that if it does not matter, for the kind of things one intends to prove, whether A or B is executed first, then it is a waste of time to consider both the AB and the BA interleavings.
3. Abstraction attempts to prove properties on a system by first simplifying it. The simplified system usually does not satisfy exactly the same properties as the original one so that a process of refinement may be necessary. Generally, one requires the abstraction to be sound (the properties proved on the abstraction are true of the original system); however, most often, the abstraction is not complete (not all true properties of the original system are true of the abstraction). An example of abstraction is, on a program, to ignore the values of non boolean variables and to only consider boolean variables and the control flow of the program; such an abstraction, though it may appear coarse, may be in fact be sufficient to prove e.g. properties of mutual exclusion.

Model checking tools were initially developed to reason about the logical correctness of discrete state systems, but have since been extended to deal with real-time and limited forms of hybrid systems.

Contents 1 See also 1.1 Articles 1.2 Related techniques 1.3 Research groups 1.4 Model checking tools 2 References

[edit] See also

[edit] Articles

• An Introduction to Model Checking at embedded.com

[edit] Related techniques

• Abstract interpretation
• Static code analysis
• Automated theorem proving

[edit] Research groups

• Software Design Group at MIT
• Modelling and Analysis of Complex Systems group at The University of Birmingham, England
• Model Checking at Carnegie Mellon University
• Software Verification and Validation at UT Austin
• SAnToS Laboratory at K-State
• Automated Software Engineering at Nasa Ames Research Center
• NASA/JPL Laboratory for Reliable Software
• VLSI/CAD Research group — University of Colorado at Boulder
• Verification and Validation — Brigham Young University, Provo, Utah
• ParaDiSe Laboratory — Masaryk University in Brno
• VASY Research team — INRIA Rhône-Alpes, France
• Formal Methods & Tools (FMT) group at The University of Twente, The Netherlands
• Software Modeling and Verification (MOVES) group at RWTH Aachen University, Germany
• Rebeca Modeling Language

[edit] Model checking tools

There are related tools in the list of Petri net tools that support model checking.

• Alloy language — GPL
• Synopsys - Magellan
• APMC — GPL v2+
• BLAST (Berkeley Lazy Abstraction Software Verification Tool) — MIT-style license
• LoTREC
• Bogor
• BOOP Toolkit
• Cadena
• Cadence SMV
• CADP
• CBMC, a bounded Model Checker for C/C++ programs
• CHIC
• COSPAN
• Coverity
• GEAR, a game based model checking tool capable of CTL, modal µ-calculus and specification patterns.
• Helena [1] — GPL — High Level Colored Petri Nets Analyzer
• HOL theorem prover
• Java Pathfinder
• LASH, Liège Automata-based Symbolic Handler
• KRONOS - TCTL-based timed model checker
• LTSA
• [mc]square, a model checker for microcontroller (ATMEL ATmega and Infineon XC167) assembly code
• MOPED
• MOPS, Modelchecking Programs for Security properties
• μCRL, GPL, Based on ACP
• mCRL2 Toolset, LGPL, Based on ACP
• NuSMV, a new symbolic model checker
• ORIS, uses a CTL-like temporal logic with real-time bounds, action and state based.
• ProB
• Probabilistic Symbolic Model Checker
• ProofPower
• PROSPER
• Rabbit
• RAVEN (Real-Time Analysis and Verification Environment)
• RuleBase
• SATABS, predicate abstraction for C/C++ programs
• SAL
• SLAM project
• Symbolic Model Checker (SMV)
• Spin
• StEAM (State Exploring Assemblylevel Model Checker) Verification of concurent C++ programs
• TLC
• UPPAAL
• Verification Interacting with Synthesis (VIS)
• Markov Reward Model Checker (MRMC)

• Database of Verification and Model Checking Tools (Yahoda)

[edit] References

• Automatic verification of finite state concurrent systems using temporal logic, E.M. Clarke, E.A. Emerson, and A.P. Sistla, ACM Trans. on Programming Languages and Systems, 8(2), pp. 244–263, 1986.
• Symbolic Model Checking, Kenneth L. McMillan, Kluwer, ISBN 0-7923-9380-5, also online.
• Model Checking, Edmund M. Clarke, Jr., Orna Grumberg and Doron A. Peled, MIT Press, 1999, ISBN 0-262-03270-8.
• Logic in Computer Science: Modelling and Reasoning About Systems, Michael Huth and Mark Ryan, Cambridge University Press, 2004. DOI.
• The Spin Model Checker: Primer and Reference Manual, Gerard J. Holzmann, Addison-Wesley, ISBN 0-321-22862-6.
• Julian Bradfield and Colin Stirling, Modal logics and mu-calculi, [2]
• Specification Patterns [3]
• Property Pattern Mappings for RAFMC [4]
• more patterns: page 6 of [5]

This article was originally based on material from the Free On-line Dictionary of Computing, which is licensed under the GFDL.