Model checking explained

In computer science, model checking or property checking is a method for checking whether a finite-state model of a system meets a given specification (also known as correctness). This is typically associated with hardware or software systems, where the specification contains liveness requirements (such as avoidance of livelock) as well as safety requirements (such as avoidance of states representing a system crash).

In order to solve such a problem algorithmically, 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 in logic, namely to check whether a structure 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 the propositional logic is satisfied by a given structure.

Overview

Property checking is used for verification when two descriptions are not equivalent. During refinement, the specification is complemented with details that are unnecessary 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.[1]

An important class of model-checking methods has 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".[2] Model checking began with the pioneering work of E. M. Clarke, E. A. Emerson,[3] 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.[4] [5]

Model checking is most often applied to hardware designs. For software, because of undecidability (see computability 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. In embedded-systems hardware, it is possible to validate a specification delivered, e.g., by means of UML activity diagrams[6] or control-interpreted Petri nets.[7]

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 that 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

M,s\modelsp

. If

M

is finite, as it is in hardware, model checking reduces to a graph search.

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 a 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 linear temporal logic (LTL): the planning problem corresponds to model checking for safety properties. This method is known as bounded model checking.[8] The success of Boolean satisfiability solvers in bounded model checking led to the widespread use of satisfiability solvers in symbolic model checking.[9]

Example

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:[10]

\begin{align}\Box((tt{call}\land\Diamondtt{open})\to&((lnottt{atfloor}\landlnottt{open})~l{U}\\ &(tt{open}\lor((tt{atfloor}\landlnottt{open})~l{U}\\ &(tt{open}\lor((lnottt{atfloor}\landlnottt{open})~l{U}\\ &(tt{open}\lor((tt{atfloor}\landlnottt{open})~l{U}\\ &(tt{open}\lor(lnottt{atfloor}~l{U}~tt{open}))))))))))\end{align}

Here,

\Box

should be read as "always",

\Diamond

as "eventually",

l{U}

as "until" and the other symbols are standard logical symbols,

\lor

for "or",

\land

for "and" and

lnot

for "not".

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,[11] as well as of Olivier Coudert and Jean-Christophe Madre,[12] and the development of open-source BDD manipulation libraries such as CUDD[13] and BuDDy.[14]
  2. 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 depth-first search).
  1. 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 be sound (the properties proved on the abstraction are true of the original system); however, sometimes the abstraction is not complete (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 of mutual exclusion.
  2. 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.

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.

First-order logic

Model checking is also studied in the field of computational complexity theory. Specifically, a first-order logical formula is fixed without free variables and the following decision problem is considered:

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. It 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.[15] These results have been extended to the task of enumerating all solutions to a first-order formula with free variables.

Tools

See main article: List of model checking tools.

Here is a list of significant model-checking tools:

Further reading

Notes and References

  1. Book: Lam K., William . 2005 . Hardware Design Verification: Simulation and Formal Method-Based Approaches . http://my.safaribooksonline.com/book/electrical-engineering/semiconductor-technology/0131433474/an-invitation-to-design-verification/ch01lev1sec1#X2ludGVybmFsX0h0bWxWaWV3P3htbGlkPTAxMzE0MzM0NzQlMkZjaDAxbGV2MXNlYzEmcXVlcnk9 . December 12, 2012. Chapter 1.1: What Is Design Verification?.
  2. Web site: Amir Pnueli - A.M. Turing Award Laureate.
  3. Edmund M. Clarke, E. Allen Emerson: "Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic". Logic of Programs 1981: 52-71.
  4. Web site: Press Release: ACM Turing Award Honors Founders of Automatic Verification Technology . 2009-01-06 . https://web.archive.org/web/20081228210748/http://www.acm.org/press-room/news-releases/turing-award-07/ . 2008-12-28 . dead .
  5. http://usacm.acm.org/usacm/weblog/index.php?p=572 USACM: 2007 Turing Award Winners Announced
  6. Book: 10.1007/978-3-319-07013-1_22. Model Checking of UML Activity Diagrams in Logic Controllers Design. Proceedings of the Ninth International Conference on Dependability and Complex Systems DepCoS-RELCOMEX. June 30 – July 4, 2014, Brunów, Poland. Advances in Intelligent Systems and Computing. 2014. Grobelna. Iwona. Grobelny. Michał. Adamski. Marian. 286. 233–242. 978-3-319-07012-4.
  7. I. Grobelna, "Formal verification of embedded logic controller specification with computer deduction in temporal logic", Przeglad Elektrotechniczny, Vol.87, Issue 12a, pp.47–50, 2011
  8. Clarke . E. . Biere . A. . Raimi . R. . Zhu . Y. . Formal Methods in System Design . 19 . 7–34 . 2001 . 10.1023/A:1011276507260. Bounded Model Checking Using Satisfiability Solving. 2484208 .
  9. Vizel . Y. . Weissenbacher . G. . Malik . S. . Proceedings of the IEEE . 103 . 11 . 2021–2035 . 2015 . 10.1109/JPROC.2015.2455034. Boolean Satisfiability Solvers and Their Applications in Model Checking. 10190144 .
  10. M. . Dwyer . G. . Avrunin . J. . Corbett . Patterns in Property Specification for Finite-State Verification . Patterns in property specifications for finite-state verification . Proceedings of the 21st international conference on Software engineering . 411–420 . May 1999 . 10.1145/302405.302672 . 1581130740 .
    • Symbolic Model Checking, Kenneth L. McMillan, Kluwer,, also online .
  12. Coudert . O. . Madre . J.C. . 1990 . A unified framework for the formal verification of sequential circuits . International Conference on Computer-Aided Design . IEEE Comput. Soc. Press . 126–129 . 10.1109/ICCAD.1990.129859 . 978-0-8186-2055-3.
  13. Web site: CUDD: CU Decision Diagram Package .
  14. Web site: BuDDy – A Binary Decision Diagram Package.
  15. Dawar. A. Kreutzer. S. 2009. Parameterized complexity of first-order logic. https://web.archive.org/web/20190303105602/http://pdfs.semanticscholar.org/ac54/505a6c9b843259727dba98fad1a02af2a567.pdf. dead. 2019-03-03. ECCC. 5856640.
  16. https://www.stormchecker.org/ Storm model checker
  17. https://www.microsoft.com/en-us/research/project/zing Zing

This article is licensed under the GNU Free Documentation License. It uses material from the Wikipedia article "Model checking".

Except where otherwise indicated, Everything.Explained.Today is © Copyright 2009-2024, A B Cryer, All Rights Reserved. Cookie policy.