Model checking

This article is about checking of models in computer science. For the checking of models in statistics, see regression model validation.
In computer science, model checking refers to the following problem: Given a model of a system, test automatically whether this model meets a given specification. Typically, the systems one has in mind are hardware or software systems, and the specification contains safety requirements such as the absence of deadlocks and similar critical states that can cause the system to crash. Model checking is a technique for automatically verifying correctness properties of finitestate systems.
In order to solve such a problem algorithmically, both the model of the system and the specification are formulated in some precise mathematical language: To this end, it is formulated as a task in logic, namely to check whether a given structure satisfies a given logical formula. The concept is general and applies to all kinds of logics and suitable structures. A simple modelchecking problem is verifying whether a given formula in the propositional logic is satisfied by a given structure.
Contents
Overview
An important class of model checking methods have been developed for checking models of hardware and software designs where the specification is given by a temporal logic formula. Pioneering work in the model checking of temporal logic formulae was done by E. M. Clarke and E. A. Emerson^{[1]}^{[2]}^{[3]} and by J. P. Queille and J. Sifakis.^{[4]} Clarke, Emerson, and Sifakis shared the 2007 Turing Award for their work on model checking.^{[5]}^{[6]}
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 structure is usually given as a source code description in an industrial hardware description language or a specialpurpose language. Such a program corresponds to a finite state machine (FSM), 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 structure M with initial state s, decide if . If M is finite, as it is in hardware, model checking reduces to a graph search.
Algorithms
state space enumeration, symbolic state space enumeration, abstract interpretation, symbolic simulation, symbolic trajectory evaluation, symbolic execution
Explicitstate model checking
Symbolic model checking
Tools
Main article: List of model checking toolsModel checking tools face a combinatorial blow up of the statespace, commonly known as the state explosion problem, that must be addressed to solve most realworld problems. There are several approaches to combat this problem.
 Symbolic algorithms avoid ever building the graph for the FSM; instead, they represent the graph implicitly using a formula in quantified propositional logic. The use of binary decision diagrams (BDDs) was made popular by the work of Ken McMillan.^{[7]}
 Bounded model checking algorithms unroll the FSM for a fixed number of steps k and check whether a property violation can occur in k or fewer steps. This typically involves encoding the restricted model as an instance of SAT. The process can be repeated with larger and larger values of k until all possible violations have been ruled out (cf. Iterative deepening depthfirst search).
 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.
 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 in fact be sufficient to prove e.g. properties of mutual exclusion.
 Counterexample guided abstraction refinement (CEGAR) begins checking with a coarse (imprecise) abstraction and iteratively refines it. When a violation (counterexample) is found, the tool analyzes it for feasibility (i.e., is the violation genuine or the result of an incomplete abstraction?). If the violation is feasible, it is reported to the user; if it is not, the proof of infeasibility is used to refine the abstraction and checking begins again.^{[8]}
Model checking tools were initially developed to reason about the logical correctness of discrete state systems, but have since been extended to deal with realtime and limited forms of hybrid systems.
See also
 Binary decision diagram
 Büchi automaton
 Computation tree logic
 Formal verification
 Linear temporal logic
 Partial order reduction
Tools
For a categorized list of tools see here.
 BLAST model checker
 CADP (Construction and Analysis of Distributed Processes) a toolbox for the design of communication protocols and distributed systems
 CHESS model checker
 CHIC
 FDR2 a model checker for verifying realtime systems modeled and specified as CSP Processes
 ISP code level verifier for MPI programs
 Java Pathfinder  open source model checker for Java programs
 Markov Reward Model Checker (MRMC)
 mCRL2 Toolset, Boost Software License, Based on ACP
 MoonWalker  open source model checker for .NET programs
 NuSMV, a new symbolic model checker
 ompca, an interactive symbolic simulator with API control for C/C++ programs with OpenMP directives. The tool is built as an application of REDLIB.
 PAT  an enhanced simulator, model checker and refinement checker for concurrent and realtime systems
 Prism, a probabilistic symbolic model checker
 Rabbit
 REDLIB, library for the modelchecking of communicating timed automatas with BDDlike diagrams. Applications include a TCTL modelchecker with timed fairness quantifications, fair simulation checker, and interactive symbolic simulator for C/C++ programs with OpenMP directives. GUI for model editing and symbolic simulation are also available.
 SMART Model checker , Symbolic Model checking Analyzer for Reliability and Timing
 SPIN model checker a general tool for verifying the correctness of distributed software models in a rigorous and mostly automated fashion.
 TAPAs: tool for the analysis of process algebra.
 Vereofy,^{[9]} a software model checker for componentbased systems for operational correctness
 μCRL, GPL, Based on ACP
 UPPAAL an integrated tool environment for modeling, validation and verification of realtime systems modeled as networks of timed automata
 Roméo an integrated tool environment for modeling, simulation and verification of realtime systems modeled as parametric, time and stopwatch Petri nets
 TLA+ model checker by Leslie Lamport
 AlPiNA,^{[10]} AlPiNA stands for Algebraic Petri Nets Analyzer and is a model checker for Algebraic Petri Nets.
 Related techniques
 Abstract interpretation
 Automated theorem proving
 Model checking tools
 Program analysis (computer science)
 Static code analysis
 History
 E.M. Clarke: The birth of model checking
 E. Allen Emerson: The Beginning of Model Checking: A Personal Perspective (this is also a very good introduction and overview of model checking)
 Model Checking, Doron Peled, Patrizio Pelliccione, Paola Spoletini, Wiley Encyclopedia of Computer Science and Engineering, 2009.
References
 ^ Allen Emerson, E.; Clarke, Edmund M. (1980), "Characterizing correctness properties of parallel programs using fixpoints", Automata, Languages and Programming, doi:10.1007/3540100032_69
 ^ Edmund M. Clarke, E. Allen Emerson: "Design and Synthesis of Synchronization Skeletons Using BranchingTime Temporal Logic". Logic of Programs 1981: 5271.
 ^ Clarke, E. M.; Emerson, E. A.; Sistla, A. P. (1986), "Automatic verification of finitestate concurrent systems using temporal logic specifications", ACM Transactions on Programming Languages and Systems 8 (2): 244, doi:10.1145/5397.5399
 ^ Queille, J. P.; Sifakis, J. (1982), "Specification and verification of concurrent systems in CESAR", International Symposium on Programming, doi:10.1007/3540114947_22
 ^ Press Release: ACM Turing Award Honors Founders of Automatic Verification Technology
 ^ USACM: 2007 Turing Award Winners Announced
 ^ * Symbolic Model Checking, Kenneth L. McMillan, Kluwer, ISBN 0792393805, also online.
 ^ Clarke, Edmund; Grumberg, Orna; Jha, Somesh; Lu, Yuan; Veith, Helmut (2000), "CounterexampleGuided Abstraction Refinement", Computer Aided Verification 1855: 154, doi:10.1007/10722167_15
 ^ Vereofy.de
 ^ alpina.unige.ch
Further reading
 Model Checking, Doron Peled, Patrizio Pelliccione, Paola Spoletini, Wiley Encyclopedia of Computer Science and Engineering, 2009.
 Model Checking, Edmund M. Clarke, Jr., Orna Grumberg and Doron A. Peled, MIT Press, 1999, ISBN 0262032708.
 Systems and Software Verification: ModelChecking Techniques and Tools, B. Berard, M. Bidoit, A. Finkel, F. Laroussinie, A. Petit, L. Petrucci, P. Schnoebelen, ISBN 3540415238
 Logic in Computer Science: Modelling and Reasoning About Systems, Michael Huth and Mark Ryan, Cambridge University Press, 2004. DOI DOI/org.
 The Spin Model Checker: Primer and Reference Manual, Gerard J. Holzmann, AddisonWesley, ISBN 0321228626.
 Julian Bradfield and Colin Stirling, Modal logics and mucalculi, Inf.ed.ac.uk
 Specification Patterns KSU.edu
 Property Pattern Mappings for RAFMC Inria.fr
 Radu Mateescu and Mihaela Sighireanu Efficient OntheFly ModelChecking for Regular AlternationFree MuCalculus, page 6, Science of Computer Programming 46(3):255281, 2003
 MüllerOlm, M., Schmidt, D.A. and Steffen, B. Model checking: a tutorial introduction. Proc. 6th Static Analysis Symposium, G. File and A. Cortesi, eds., Springer LNCS 1694, 1999, pp. 330–354.
This article was originally based on material from the Free Online Dictionary of Computing, which is licensed under the GFDL.
Categories:
Wikimedia Foundation. 2010.
Look at other dictionaries:
Model Checking — (deutsch auch Modellprüfung) ist ein Verfahren zur vollautomatischen Verifikation einer Systembeschreibung (Modell) gegen eine Spezifikation (Formel). Der Begriff ist motiviert durch die mathematische Formulierung des Problems: Für eine gegebene… … Deutsch Wikipedia
Model Checking — Le Model Checking désigne une famille de techniques de vérification automatique des systèmes dynamiques (souvent d origine informatique ou électronique). Il s agit de vérifier algorithmiquement si un modèle donné, le système lui même ou une… … Wikipédia en Français
Model checking — Le Model Checking désigne une famille de techniques de vérification automatique des systèmes dynamiques (souvent d origine informatique ou électronique). Il s agit de vérifier algorithmiquement si un modèle donné, le système lui même ou une… … Wikipédia en Français
Model checking — Con el nombre Model checking se conoce a un método automático de verificación de un sistema formal, en la mayoría de las ocasiones derivado del hardware o del software de un sistema informático. El sistema es descrito mediante un modelo, que debe … Wikipedia Español
Model checking (disambiguation) — Model checking may refer to model checking regression model validation This disambiguation page lists articles associated with the same title. If an internal link led you here, you may wish to chan … Wikipedia
Abstraction model checking — is for systems where an actual representation is too complex in developing the model alone. So, the design undergoes a kind of translation to scaled down abstract version.The set of variables are partitioned into visible and invisible depending… … Wikipedia
Modelbased testing — is the application of Model based design for designing and optionally executing the necessary artifacts to perform software testing. Models can be used to represent the desired behavior of the System Under Test (SUT), or to represent the desired… … Wikipedia
Model audit — A model audit is the colloquial term for the tasks performed when conducting due diligence on a financial model, in order to eliminate spreadsheet error. (Also known as Model Review in some areas). A study in 1998 concluded that even MBA students … Wikipedia
Model theory — This article is about the mathematical discipline. For the informal notion in other parts of mathematics and science, see Mathematical model. In mathematics, model theory is the study of (classes of) mathematical structures (e.g. groups, fields,… … Wikipedia
Model View ViewModel — The Model View ViewModel (MVVM) is an architectural pattern used in software engineering that originated from Microsoft as a specialization of the Presentation Model design pattern introduced by Martin Fowler.[1] Largely based on the Model view… … Wikipedia