![Two One G (cropped)](https://upload.wikimedia.org/wikipedia/commons/9/9a/Two_One_G_%28cropped%29.jpg)
In
computer science
Computer science is the study of computation, automation, and information. Computer science spans theoretical disciplines (such as algorithms, theory of computation, information theory, and automation) to practical disciplines (includi ...
, model checking or property checking is a method for checking whether a
finite-state model of a system meets a given
specification
A specification often refers to a set of documented requirements to be satisfied by a material, design, product, or service. A specification is often a type of technical standard.
There are different types of technical or engineering specificati ...
(also known as
correctness). This is typically associated with
hardware or
software systems
A software system is a system of intercommunicating components based on software forming part of a computer system (a combination of hardware and software). It "consists of a number of separate programs, configuration files, which are used to ...
, where the specification contains liveness requirements (such as avoidance of
livelock
In concurrent computing, deadlock is any situation in which no member of some group of entities can proceed because each waits for another member, including itself, to take action, such as sending a message or, more commonly, releasing a loc ...
) as well as safety requirements (such as avoidance of states representing a
system crash).
In order to solve such a problem
algorithm
In mathematics and computer science, an algorithm () is a finite sequence of rigorous instructions, typically used to solve a class of specific problems or to perform a computation. Algorithms are used as specifications for performing ...
ically, 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
Logic is the study of correct reasoning. It includes both formal and informal logic. Formal logic is the science of deductively valid inferences or of logical truths. It is a formal science investigating how conclusions follow from premise ...
, 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
Propositional calculus is a branch of logic. It is also called propositional logic, statement logic, sentential calculus, sentential logic, or sometimes zeroth-order logic. It deals with propositions (which can be true or false) and relations b ...
is satisfied by a given structure.
Overview
Property checking is used for
verification
Verify or verification may refer to:
General
* Verification and validation, in engineering or quality management systems, is the act of reviewing, inspecting or testing, in order to establish and document that a product, service or system meets ...
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.
An important class of model-checking methods has been developed for checking models of
hardware and
software
Software is a set of computer programs and associated software documentation, documentation and data (computing), data. This is in contrast to Computer hardware, hardware, from which the system is built and which actually performs the work.
...
designs where the specification is given by a
temporal logic In logic, temporal logic is any system of rules and symbolism for representing, and reasoning about, propositions qualified in terms of time (for example, "I am ''always'' hungry", "I will ''eventually'' be hungry", or "I will be hungry ''until'' I ...
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 of
E. M. Clarke,
E. A. Emerson,
[Edmund M. Clarke, E. Allen Emerson]
"Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic"
Logic of Programs 1981: 52-71. by J. P. Queille, and
J. Sifakis.
Clarke, Emerson, and Sifakis shared the 2007
Turing Award
The ACM A. M. Turing Award is an annual prize given by the Association for Computing Machinery (ACM) for contributions of lasting and major technical importance to computer science. It is generally recognized as the highest distinction in comput ...
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 (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 or control-interpreted
Petri net
A Petri net, also known as a place/transition (PT) net, is one of several mathematical modeling languages for the description of distributed systems. It is a class of discrete event dynamic system. A Petri net is a directed bipartite graph that ...
s.
The structure is usually given as a source code description in an industrial
hardware description language
In computer engineering, a hardware description language (HDL) is a specialized computer language used to describe the structure and behavior of electronic circuits, and most commonly, digital logic circuits.
A hardware description language en ...
or a special-purpose language. Such a program corresponds to a
finite state machine
A finite-state machine (FSM) or finite-state automaton (FSA, plural: ''automata''), finite automaton, or simply a state machine, is a mathematical model of computation. It is an abstract machine that can be in exactly one of a finite number o ...
(FSM), i.e., a
directed graph
In mathematics, and more specifically in graph theory, a directed graph (or digraph) is a graph that is made up of a set of vertices connected by directed edges, often called arcs.
Definition
In formal terms, a directed graph is an ordered pa ...
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
In general, a node is a localized swelling (a "knot") or a point of intersection (a Vertex (graph theory), vertex).
Node may refer to:
In mathematics
*Vertex (graph theory), a vertex in a mathematical graph
*Vertex (geometry), a point where two ...
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
, and a structure
with initial state
, decide if
. If
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 logic and computer science, the Boolean satisfiability problem (sometimes called propositional satisfiability problem and abbreviated SATISFIABILITY, SAT or B-SAT) is the problem of determining if there exists an interpretation that satisfie ...
in solving the
planning problem in
artificial intelligence
Artificial intelligence (AI) is intelligence—perceiving, synthesizing, and inferring information—demonstrated by machines, as opposed to intelligence displayed by animals and humans. Example tasks in which this is done include speech r ...
(see
satplan
Satplan (better known as Planning as Satisfiability) is a method for automated planning. It converts the planning problem instance into an instance of the Boolean satisfiability problem, which is then solved using a method for establishing satisfia ...
) 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. The success of
Boolean satisfiability solvers in bounded model checking led to the widespread use of satisfiability solvers in symbolic model checking.
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:
:
Here,
should be read as "always",
as "eventually",
as "until" and the other symbols are standard logical symbols,
for "or",
for "and" and
for "not".
Techniques
Model-checking tools face a combinatorial blow up of the state-space, commonly known as the
state explosion problem
In mathematics, a combinatorial explosion is the rapid growth of the complexity of a problem due to how the combinatorics of the problem is affected by the input, constraints, and bounds of the problem. Combinatorial explosion is sometimes used ...
, that must be addressed to solve most real-world problems. There are several approaches to combat this problem.
# 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 the development of open-source BDD manipulation libraries such as CUDD and BuDDy.
# Bounded model-checking algorithms unroll the FSM for a fixed number of steps,
, and check whether a property violation can occur in
or fewer steps. This typically involves encoding the restricted model as an instance of
SAT
The SAT ( ) is a standardized test widely used for college admissions in the United States. Since its debut in 1926, its name and scoring have changed several times; originally called the Scholastic Aptitude Test, it was later called the Schol ...
. The process can be repeated with larger and larger values of
until all possible violations have been ruled out (cf.
Iterative deepening depth-first search
In computer science, iterative deepening search or more specifically iterative deepening depth-first search (IDS or IDDFS) is a state space/graph search strategy in which a depth-limited version of depth-first search is run repeatedly with incr ...
).
#
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
In computer science, mutual exclusion is a property of concurrency control, which is instituted for the purpose of preventing race conditions. It is the requirement that one thread of execution never enters a critical section while a concurrent ...
.
# Counterexample-guided abstraction refinement (CEGAR) begins checking with a coarse (i.e. imprecise) abstraction and iteratively refines it. When a violation (i.e.
counterexample
A counterexample is any exception to a generalization. In logic a counterexample disproves the generalization, and does so rigorously in the fields of mathematics and philosophy. For example, the fact that "John Smith is not a lazy student" is a ...
) 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 system A hybrid system is a dynamical system that exhibits both continuous and discrete dynamic behavior – a system that can both ''flow'' (described by a differential equation) and ''jump'' (described by a state machine or automaton). Often, the te ...
s.
First-order logic
Model checking is also studied in the field of
computational complexity theory
In theoretical computer science and mathematics, computational complexity theory focuses on classifying computational problems according to their resource usage, and relating these classes to each other. A computational problem is a task solved ...
. Specifically, a
first-order logical formula is fixed without
free variable
In mathematics, and in other disciplines involving formal languages, including mathematical logic and computer science, a free variable is a notation (symbol) that specifies places in an expression where substitution may take place and is not ...
s and the following
decision problem
In computability theory and computational complexity theory, a decision problem is a computational problem that can be posed as a yes–no question of the input values. An example of a decision problem is deciding by means of an algorithm wheth ...
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
In graph theory, the treewidth of an undirected graph is an integer number which specifies, informally, how far the graph is from being a tree. The smallest treewidth is 1; the graphs with treewidth 1 are exactly the trees and the forests. The gra ...
bounded by a constant (which more generally implies the tractability of model checking for
monadic second-order logic In mathematical logic, monadic second-order logic (MSO) is the fragment of second-order logic where the second-order quantification is limited to quantification over sets. It is particularly important in the logic of graphs, because of Courcelle's ...
), bounding the
degree
Degree may refer to:
As a unit of measurement
* Degree (angle), a unit of angle measurement
** Degree of geographical latitude
** Degree of geographical longitude
* Degree symbol (°), a notation used in science, engineering, and mathematics
...
of every domain element, and more general conditions such as
bounded expansion
In graph theory, a family of graphs is said to have bounded expansion if all of its shallow minors are sparse graphs. Many natural families of sparse graphs have bounded expansion. A closely related but stronger property, polynomial 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 list of significant model-checking tools:
*
Alloy
An alloy is a mixture of chemical elements of which at least one is a metal. Unlike chemical compounds with metallic bases, an alloy will retain all the properties of a metal in the resulting material, such as electrical conductivity, ductilit ...
(Alloy Analyzer)
*
BLAST
Blast or The Blast may refer to:
*Explosion, a rapid increase in volume and release of energy in an extreme manner
*Detonation, an exothermic front accelerating through a medium that eventually drives a shock front
Film
* ''Blast'' (1997 film), ...
(Berkeley Lazy Abstraction Software Verification Tool)
*
CADP
CADP (Construction and Analysis of Distributed Processes) is a toolbox for the design of communication protocols and distributed systems. CADP is developed by the CONVECS team (formerly by the VASY team) at INRIA Rhone-Alpes and connected to vari ...
(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 as
CSP Processes
*
ISP
An Internet service provider (ISP) is an organization that provides services for accessing, using, or participating in the Internet. ISPs can be organized in various forms, such as commercial, community-owned, non-profit, or otherwise private ...
code level verifier for
MPI programs
*
Java Pathfinder
Java Pathfinder (JPF) is a system to verify executable Java bytecode programs. JPF was developed at the NASA Ames Research Center and open sourced in 2005. The acronym JPF is not to be confused with the unrelated ''Java Plugin Framework'' project. ...
: an open-source model checker for Java programs
*
Libdmc: a framework for distributed model checking
*
mCRL2
mCRL2 is a specification language for describing concurrent discrete event systems. It is accompanied with a toolset, that facilitates tools, techniques and methods for simulation, analysis and visualization of behaviour. The behavioural part of th ...
Toolset,
Boost Software License, Based on
ACP
*
NuSMV
NuSMV is a reimplementation and extension of SMV symbolic model checker, the first model checking tool based on Binary Decision Diagrams (BDDs).K.L. McMillan. Symbolic model checking. In Kluwer Academic Publ.,1993.
The tool has been designed as a ...
: a new symbolic model checker
*
PAT: an enhanced simulator, model checker and refinement checker for concurrent and real-time systems
*
Prism
Prism usually refers to:
* Prism (optics), a transparent optical component with flat surfaces that refract light
* Prism (geometry), a kind of polyhedron
Prism may also refer to:
Science and mathematics
* Prism (geology), a type of sedimentary ...
: 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
*
TAPAs
A tapa () is an appetizer or snack in Spanish cuisine. Tapas can be combined to make a full meal, and can be cold (such as mixed olives and cheese) or hot (such as ''chopitos'', which are battered, fried baby squid, or patatas bravas). In so ...
: a tool for the analysis of process algebra
*
TAPAAL: an integrated tool environment for modelling, validation, and verification of Timed-Arc
Petri Nets
A Petri net, also known as a place/transition (PT) net, is one of several mathematical modeling languages for the description of distributed systems. It is a class of discrete event dynamic system. A Petri net is a directed bipartite graph that ...
*
TLA+
TLA+ is a formal specification language developed by Leslie Lamport. It is used for designing, modelling, documentation, and verification of programs, especially concurrent systems and distributed systems. TLA+ is considered to be exhaustively-t ...
model checker by
Leslie Lamport
Leslie B. Lamport (born February 7, 1941 in Brooklyn) is an American computer scientist and mathematician. Lamport is best known for his seminal work in distributed systems, and as the initial developer of the document preparation system LaTeX an ...
*
UPPAAL: an integrated tool environment for modelling, validation, and verification of real-time systems modelled as networks of timed automata
*
Zing
Zing or ZING may refer to:
*Zing (model-checker), infrastructure for verification of concurrent software via model checking
*Zing (punctuation) or irony punctuation, invented by English printer Henry Denham in the 1580s
*Zing (quartet), the 2010 S ...
Zing
/ref> – experimental tool from Microsoft
Microsoft Corporation is an American multinational technology corporation producing computer software, consumer electronics, personal computers, and related services headquartered at the Microsoft Redmond campus located in Redmond, Washin ...
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.
See also
References
Further reading
*
*
*
*
*
*. JA Bergstra, A. Ponse and SA Smolka, editors." ().
*
*
*
*
*
*
* (this is also a very good introduction and overview of model checking)
{{DEFAULTSORT:Model Checking