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. Pioneering work in the model checking of temporal logic formulae was done by E. Allen Emerson, whose advisor was Edmund Clarke. In mathematics, computing, linguistics, and related disciplines, an algorithm is a finite list of well-defined instructions for accomplishing some task that, given an initial state, will terminate in a defined end-state. ... In the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain formal specification or property, using formal methods of mathematics. ... System (from Latin systēma, in turn from Greek systēma) is a set of entities, real or abstract, comprising a whole where each component interacts with or is related to at least one other component and they all serve a common objective. ... Hardware is the general term that is used to describe physical artifacts of a technology. ... Computer software (or simply software) refers to one or more computer programs and data held in the storage of a computer for some purpose. ... Look up formal in Wiktionary, the free dictionary. ... Specification may refer to several different concepts: Specification (standards) refers to specific standards Specificatio - a legal concept Specification (regression) refers to the practice of translating theory into a regression model Category: ... In logic, the term temporal logic is used to describe any system of rules and symbolism for representing, and reasoning about, propositions qualified in terms of time. ...

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. Computability theory is the branch of theoretical computer science that studies which problems are computationally solvable using different models of computation. ...

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. In electronics, a hardware description language or HDL is any language from a class of computer languages for formal description of electronic circuits. ... Fig. ... This article just presents the basic definitions. ... This article just presents the basic definitions. ... This article just presents the basic definitions. ... The term node can refer to: Node, a spatial locus along a standing wave where the wave has minimal amplitude. ... This article is about the word proposition as it is used in logic, philosophy, and linguistics. ...

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. In mathematics a combinatorial explosion describes the effect of functions that grow very rapidly as a result of combinatorial considerations. ...

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. A binary decision diagram (BDD), like a negation normal form (NNF) or a propositional directed acyclic graph (PDAG), is a data structure that is used to represent a Boolean function. ... To meet Wikipedias quality standards, this article or section may require cleanup. ... The Partial order reduction is aimed at reducing the size of the state spac that need to be searched by model checking algorithms. ... In computer science, abstract interpretation is a theory of sound approximation of the semantics of computer programs, based on monotonic functions over ordered sets, especially lattices. ... Mutual exclusion (often abbreviated to mutex) algorithms are used in concurrent programming to avoid the simultaneous use of un-shareable resources by pieces of computer code called critical sections. ... Wikipedia does not have an article with this exact name. ... A hybrid system consists of both discrete signals and continuous signals. ...

See also

Articles

• An Introduction to Model Checking at embedded.com

Related techniques

• Abstract interpretation
• Static code analysis
• Automated theorem proving

In computer science, abstract interpretation is a theory of sound approximation of the semantics of computer programs, based on monotonic functions over ordered sets, especially lattices. ... Static analysis is the term applied to the analysis of computer software that is performed without actually executing programs built from that software (analysis performed on executing programs is known as dynamic analysis). ... Automated theorem proving (ATP) or automated deduction, currently the most well-developed subfield of automated reasoning (AR), is the proving of mathematical theorems by a computer program. ...

Research groups

• Software Design Group at MIT
• Modelling and Analysis of Complex Systems group at The University of Birmingham, England
• Software Modeling and Verification (MOVES) group at RWTH Aachen University, Germany
• Formal Methods & Tools (FMT) group at The University of Twente, The Netherlands
• 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

• Rebeca Modeling Language

Rebeca (Reactive Objects Language) is an actor-based language with a formal foundation, designed in an effort to bridge the gap between formal verification approaches and real applications. ...

Model checking tools

These are some tools that support model checking.

• Prover Plug-In commercial proof engines
• 0-In Formal Verification
• DiVinE - Distributed Verification Environment
• PRrobabilistIc Symbolic Model checker (PRISM)
• Markov Reward Model Checker (MRMC)
• Alloy language — GPL
• Synopsys - Magellan
• APMC — GPL v2+
• AcPeg Access Control Systems verification tool through Model Checking (AcPeg)
• Formal Safety Verification of Rail Control Systems
• 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
• 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 Model Checker (UPPAAL)
• Verification Interacting with Synthesis (VIS)
• Database of Verification and Model Checking Tools (Yahoda)

There are very few or no other articles that link to this one. ... BLAST is a software model checking tool for C programs. ... Mapúa Institute of Technology (MIT, MapúaTech or simply Mapúa) is a private, non-sectarian, Filipino tertiary institute located in Intramuros, Manila. ... CHIC is a modular verifier for behavioral compatibility checking of hardware and software systems. ... Coverity is a tool used for static analysis of C and C++ source code. ... Computational tree logic (CTL) is a branching-time logic, meaning that its model of time is a tree-like structure in which the future is not determined; there are different paths in the future, any one of which might be actual path that is realised. ... The μ-calculus (also modal μ calculus) is a class of temporal logics with a least fixpoint operator μ. It is used to describe properties of labelled transition systems and for verifying these properties. ... The GNU logo The GNU General Public License (GNU GPL or simply GPL) is a widely-used free software license, originally written by Richard Stallman for the GNU project. ... The various HOL (which stands for Higher Order Logic) systems are a family of interactive theorem proving systems sharing similar logics and implementation strategies. ... The GNU logo The GNU General Public License (GNU GPL or simply GPL) is a widely-used free software license, originally written by Richard Stallman for the GNU project. ... The Algebra of Communicating Processes (ACP) is an algebraic approach to reasoning about concurrent systems. ... GNU logo The GNU Lesser General Public License (formerly the GNU Library General Public License) is a free software license published by the Free Software Foundation. ... The Algebra of Communicating Processes (ACP) is an algebraic approach to reasoning about concurrent systems. ... Wikipedia does not have an article with this exact name. ... Computational tree logic (CTL) is a branching-time logic, meaning that its model of time is a tree-like structure in which the future is not determined; there are different paths in the future, any one of which might be actual path that is realised. ... Rabbit is a model checking tool for real-time systems. ...

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. The Association for Computing Machinery, or ACM, was founded in 1947 as the worlds first scientific and educational computing society. ... 1986 (MCMLXXXVI) was a common year starting on Wednesday of the Gregorian calendar. ... MIT Press Books The MIT Press is a university publisher affiliated with the Massachusetts Institute of Technology (MIT) in Cambridge, Massachusetts. ... Year 1999 (MCMXCIX) was a common year starting on Friday (link will display full 1999 Gregorian calendar). ... The headquarters of the Cambridge University Press, in Trumpington Street, Cambridge. ... shelby was here 2004 (MMIV) was a leap year starting on Thursday of the Gregorian calendar. ... Gerard J. Holzmann (born 1951) is an American computer scientist, best known as the developer of the SPIN model checker. ... The Free On-line Dictionary of Computing (FOLDOC) is an online, searchable encyclopedic dictionary of computing subjects. ... Bold text // “GFDL” redirects here. ...