Incomputer science,model checking orproperty checking is a method for checking whether afinite-state model of a system meets a givenspecification (also known ascorrectness). This is typically associated withhardware orsoftware systems, where the specification contains liveness requirements (such as avoidance oflivelock) as well as safety requirements (such as avoidance of states representing asystem crash).

In order to solve such a problemalgorithmically, both the model of the system and its specification are formulated in some precise mathematical language. To this end, the problem is formulated as a task inlogic, namely to check whether astructure satisfies a given logical formula. This general concept applies to many kinds of logic and many kinds of structures. A simple model-checking problem consists of verifying whether a formula in thepropositional logic is satisfied by a given structure.

Property checking is used forverification when two descriptions are not equivalent. Duringrefinement, the specification is complemented with details that areunnecessary in the higher-level specification. There is no need to verify the newly introduced properties against the original specification since this is not possible. Therefore, the strict bi-directional equivalence check is relaxed to a one-way property check. The implementation or design is regarded as a model of the system, whereas the specifications are properties that the model must satisfy.^[2]

An important class of model-checking methods has been developed for checking models ofhardware andsoftware designs where the specification is given by atemporal logic formula. Pioneering work in temporal logic specification was done byAmir Pnueli, who received the 1996 Turing award for "seminal work introducing temporal logic into computing science".^[3] Model checking began with the pioneering work ofE. M. Clarke,E. A. Emerson,^[4][5][6] by J. P. Queille, andJ. Sifakis.^[7] Clarke, Emerson, and Sifakis shared the 2007Turing Award for their seminal work founding and developing the field of model checking.^[8][9]

Model checking is most often applied to hardware designs. For software, because of undecidability (seecomputability theory) the approach cannot be fully algorithmic, apply to all systems, and always give an answer; in the general case, it may fail to prove or disprove a given property. Inembedded-systems hardware, it is possible to validate a specification delivered, e.g., by means ofUML activity diagrams^[10] or control-interpretedPetri nets.^[11]

The structure is usually given as a source code description in an industrialhardware description language or a special-purpose language. Such a program corresponds to afinite-state machine (FSM), i.e., adirected graph consisting of nodes (orvertices) andedges. A set of atomic propositions is associated with each node, typically stating which memory elements are one. Thenodes represent states of a system, the edges represent possible transitions that may alter the state, while the atomic propositions represent the basic properties that hold at a point of execution.^[12]

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

Instead of enumerating reachable states one at a time, the state space can sometimes be traversed more efficiently by considering large numbers of states at a single step. When such state-space traversal is based on representations of a set of states and transition relations as logical formulas,binary decision diagrams (BDD) or other related data structures, the model-checking method issymbolic.

Historically, the first symbolic methods usedBDDs. After the success ofpropositional satisfiability in solving theplanning problem inartificial intelligence (seesatplan) in 1996, the same approach was generalized to model checking forlinear temporal logic (LTL): the planning problem corresponds to model checking for safety properties. This method is known as bounded model checking.^[13] The success ofBoolean satisfiability solvers in bounded model checking led to the widespread use of satisfiability solvers in symbolic model checking.^[14]

One example of such a system requirement:Between the time an elevator is called at a floor and the time it opens its doors at that floor, the elevator can arrive at that floor at most twice. The authors of "Patterns in Property Specification for Finite-State Verification" translate this requirement into the following LTL formula:^[15]

Here,${\displaystyle ◻}$ should be read as "always",${\displaystyle ◊}$ as "eventually",${\displaystyle \mathcal{U}}$ as "until" and the other symbols are standard logical symbols,${\displaystyle \vee }$ for "or",${\displaystyle \wedge }$ for "and" and${\displaystyle \mathrm{\neg }}$ for "not".

Model-checking tools face a combinatorial blow up of the state-space, commonly known as thestate 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 explicitly constructing 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,^[16] as well as of Olivier Coudert and Jean-Christophe Madre,^[17] and the development of open-source BDD manipulation libraries such as CUDD^[18] and BuDDy.^[19]
2. Bounded model-checking algorithms unroll the FSM for a fixed number of steps,${\displaystyle k}$, and check whether a property violation can occur in${\displaystyle k}$ or fewer steps. This typically involves encoding the restricted model as an instance ofSAT. The process can be repeated with larger and larger values of${\displaystyle k}$ until all possible violations have been ruled out (cf.Iterative deepening depth-first search).
3. Abstraction attempts to prove properties of 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 besound (the properties proved on the abstraction are true of the original system); however, sometimes the abstraction is notcomplete (not all true properties of the original system are true of the abstraction). An example of abstraction is 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 ofmutual exclusion.
4. Counterexample-guided abstraction refinement (CEGAR) begins checking with a coarse (i.e. imprecise) abstraction and iteratively refines it. When a violation (i.e.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.^[20]

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

Model checking is also studied in the field ofcomputational complexity theory. Specifically, afirst-order logical formula is fixed withoutfree variables and the followingdecision problem is considered:

Given a finiteinterpretation, for instance, one described as arelational database, decide whether the interpretation is a model of the formula.

This problem is in thecircuit classAC⁰. It istractable when imposing some restrictions on the input structure: for instance, requiring that it hastreewidth bounded by a constant (which more generally implies the tractability of model checking formonadic second-order logic), bounding thedegree of every domain element, and more general conditions such asbounded expansion, locally bounded expansion, and nowhere-dense structures.^[21] These results have been extended to the task ofenumerating all solutions to a first-order formula with free variables.^{[citation needed]}

Here is a list of significant model-checking tools:

• Afra: a model checker forRebeca which is an actor-based language for modeling concurrent and reactive systems
• Alloy (Alloy Analyzer)
• BLAST (Berkeley Lazy Abstraction Software Verification Tool)
• CADP (Construction and Analysis of Distributed Processes) a toolbox for the design of communication protocols and distributed systems
• CPAchecker: an open-source software model checker for C programs, based on the CPA framework
• ECLAIR: a platform for the automatic analysis, verification, testing, and transformation of C and C++ programs
• FDR2: a model checker for verifying real-time systems modelled and specified asCSP Processes
• FizzBee: an easier to use alternative to TLA+, that uses Python-like specification language, that has both behavioral modeling like TLA+ and probabilistic modeling like PRISM
• ISP code level verifier forMPI programs
• Java Pathfinder: an open-source model checker for Java programs
• Libdmc: a framework for distributed model checking
• mCRL2 Toolset,Boost Software License, Based onACP
• NuSMV: a new symbolic model checker
• PAT: an enhanced simulator, model checker and refinement checker for concurrent and real-time systems
• Prism: a probabilistic symbolic model checker
• Roméo: an integrated tool environment for modelling, simulation, and verification of real-time systems modelled as parametric, time, and stopwatch Petri nets
• SPIN: a general tool for verifying the correctness of distributed software models in a rigorous and mostly automated fashion
• Storm:^[22] A model checker for probabilistic systems.
• TAPAs: a tool for the analysis of process algebra
• TAPAAL: an integrated tool environment for modelling, validation, and verification of Timed-ArcPetri Nets
• TLA+ model checker byLeslie Lamport
• UPPAAL: an integrated tool environment for modelling, validation, and verification of real-time systems modelled as networks of timed automata
• Zing^[23] – experimental tool fromMicrosoft to validate state models of software at various levels: high-level protocol descriptions, work-flow specifications, web services, device drivers, and protocols in the core of the operating system. Zing is currently being used for developing drivers for Windows.

• Model checking
• Logic in computer science

• Webarchive template wayback links
• Articles with short description
• Short description is different from Wikidata
• All articles with unsourced statements
• Articles with unsourced statements from May 2019