Model checking

From Wikipedia, the free encyclopedia

In computer science, model checking or property checking is, for a given model of a system, exhaustively and automatically checking whether this model meets a given specification. Typically, one has hardware or software systems in mind, whereas 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 finite-state 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, the problem is formulated as a task in logic, namely to check whether a given structure satisfies a given logical formula. This general concept applies to many kinds of logics and suitable structures. A simple model checking problem is verifying whether a given formula in the propositional logic is satisfied by a given structure.

Overview

Property checking is used for verification instead of equivalence checking when two descriptions are not functionally equivalent. Particularly, during refinement, the specification is complemented with the details that are unnecessary in the higher level specification. Yet, there is no need to verify the newly introduced properties against the original specification. It is not even possible. Therefore, the strict bi-directional equivalence check is relaxed to one-way property checking. The implementation or design is regarded a model of the circuit whereas the specifications are properties that the model must satisfy.

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 temporal logic specification was done by Amir Pnueli, who received the 1996 Turing award for "seminal work introducing temporal logic into computing science". Model checking began with the pioneering work by E. M. Clarke and E. A. Emerson and by J. P. Queille and J. Sifakis. Clarke, Emerson, and Sifakis shared the 2007 Turing Award for their seminal work founding and developing the field of model checking.

Model checking is most often applied to hardware designs. For software, because of undecidability the approach cannot be fully algorithmic; typically it may fail to prove or disprove a given property. In embedded systems hardware designs it is possible to validate (verify against some specified requirements) a specification delivered i.e. by means of UML activity diagrams or control interpreted Petri nets.

The structure 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 (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 ${\displaystyle M,s\models p}$. 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

Explicit-state model checking

Symbolic model checking

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 set of states and transition relations as logical formulas, binary decision diagrams (BDD) or other related data structures, the model-checking method is symbolic.

Historically, the first symbolic methods used BDDs. After the success of propositional satisfiability in solving the planning problem in artificial intelligence (see satplan) in 1996, the same approach was generalized to model checking for the Linear Temporal Logic LTL (the planning problem corresponds to model-checking for safety properties). This method is known as bounded model checking. The success of Boolean satisfiability solvers in bounded model checking led to the widespread use of satisfiability solvers in symbolic model checking.

Techniques

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 explicitly constructing the graph for the finite state machines (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 and development of open-source BDD manipulation libraries such as CUDD and BuDDy.
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 of SAT. 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. 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.
4. 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.
5. 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.

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.

Computational complexity

First-order logic

The field of computational complexity theory has studied the model checking problem. Specifically, we fix a first-order logical formula without free variables and consider the following decision problem: given a finite interpretation, for instance one described as a relational database, decide whether the interpretation is a model of the formula. This problem is in the circuit class AC0. The problem is tractable when imposing some restrictions on the input structure: for instance requiring that it has treewidth bounded by a constant (which more generally implies the tractability of model checking for monadic second-order logic), bounding the degree of every domain element, and more general conditions such as bounded expansion, locally bounded expansion, and nowhere-dense structures. These results have been extended to the task of enumerating all solutions to a first-order formula with free variables.

Tools

Here is a partial list of model checking tools that have a Wikipedia page:

• 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 modeled and specified as CSP Processes
• ISP code level verifier for MPI programs
• Java Pathfinder – open source model checker for Java programs
• mCRL2 Toolset, Boost Software License, Based on ACP
• 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 modeling, simulation and verification of real-time systems modeled 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.
• TAPAs: tool for the analysis of process algebra.
• TAPAAL, an integrated tool environment for modeling, validation and verification of Timed-Arc Petri Nets
• TLA+ model checker by Leslie Lamport
• UPPAAL, an integrated tool environment for modeling, validation and verification of real-time systems modeled as networks of timed automata
• Zing – experimental tool from Microsoft 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.