HOME

TheInfoList



OR:

In
computer science Computer science is the study of computation, information, and automation. Computer science spans Theoretical computer science, theoretical disciplines (such as algorithms, theory of computation, and information theory) to Applied science, ...
, 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 system A software system is a system of intercommunicating software component, components based on software forming part of a computer system (a combination of Computer hardware, hardware and software). It "consists of a number of separate Computer progr ...
s, 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 lock. ...
) 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 Rigour#Mathematics, mathematically rigorous instructions, typically used to solve a class of specific Computational problem, problems or to perform a computation. Algo ...
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 study of deductively valid inferences or logical truths. It examines how conclusions follow from premises based on the structure o ...
, namely to check whether a
structure A structure is an arrangement and organization of interrelated elements in a material object or system, or the object or system so organized. Material structures include man-made objects such as buildings and machines and natural objects such as ...
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 The propositional calculus is a branch of logic. It is also called propositional logic, statement logic, sentential calculus, sentential logic, or sometimes zeroth-order logic. Sometimes, it is called ''first-order'' propositional logic to contra ...
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. An important class of model-checking methods has been developed for checking models of hardware and
software Software consists of computer programs that instruct the Execution (computing), execution of a computer. Software also includes design documents and specifications. The history of software is closely tied to the development of digital comput ...
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 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 the fi ...
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 Computability theory, also known as recursion theory, is a branch of mathematical logic, computer science, and the theory of computation that originated in the 1930s with the study of computable functions and Turing degrees. The field has since ex ...
) 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 net (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 t ...
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, usually to design application-specific integrated circuits (ASICs) and to progra ...
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 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 \models p. 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 Planning is the process of thinking regarding the activities required to achieve a desired goal. Planning is based on foresight, the fundamental capacity for mental time travel. Some researchers regard the evolution of forethought - the cap ...
problem in
artificial intelligence Artificial intelligence (AI) is the capability of computer, computational systems to perform tasks typically associated with human intelligence, such as learning, reasoning, problem-solving, perception, and decision-making. It is a field of re ...
(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. 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: :\begin\Box\Big((\texttt \land \Diamond \texttt) \to & \big((\lnot \texttt \land \lnot \texttt) ~\mathcal \\ & (\texttt \lor ((\texttt \land \lnot \texttt) ~\mathcal\\ & (\texttt \lor ((\lnot \texttt \land \lnot \texttt) ~\mathcal \\ & (\texttt \lor ((\texttt \land \lnot \texttt) ~\mathcal \\ & (\texttt \lor (\lnot \texttt ~\mathcal~ \texttt))))))))\big)\Big)\end Here, \Box should be read as "always", \Diamond as "eventually", \mathcal 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. # 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, as well as of Olivier Coudert and Jean-Christophe Madre, 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, 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 SAT ( ) is a standardized test widely used for college admissions in the United States. Since its debut in 1926, its name and Test score, scoring have changed several times. For much of its history, it was called the Scholastic Aptitude Test ...
. 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 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 incre ...
). #
Abstraction Abstraction is a process where general rules and concepts are derived from the use and classifying of specific examples, literal (reality, real or Abstract and concrete, concrete) signifiers, first principles, or other methods. "An 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 concurr ...
. # 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 "student John Smith is not lazy" is a c ...
) 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, automaton, or a differ ...
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 explores the relationships between these classifications. A computational problem ...
. 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 variable may be said to be either free or bound. Some older books use the terms real variable and apparent variable for f ...
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 on a set of input values. An example of a decision problem is deciding whether a given natura ...
is considered: ''Given a finite interpretation, for instance, one described as a
relational database A relational database (RDB) is a database based on the relational model of data, as proposed by E. F. Codd in 1970. A Relational Database Management System (RDBMS) is a type of database management system that stores data in a structured for ...
, 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 ...
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 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 list of significant model-checking tools: * Afra: a model checker for Rebeca which is an actor-based language for modeling concurrent and reactive systems *
Alloy An alloy is a mixture of chemical elements of which in most cases at least one is a metal, metallic element, although it is also sometimes used for mixtures of elements; herein only metallic alloys are described. Metallic alloys often have prop ...
(Alloy Analyzer) * BLAST (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 * 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 for
MPI MPI or Mpi may refer to: Science and technology Biology and medicine * Magnetic particle imaging, a tomographic technique * Myocardial perfusion imaging, a medical procedure that illustrates heart function * Mannose phosphate isomerase, an enzyme ...
programs * Java Pathfinder: an open-source model checker for Java programs * Libdmc: a framework for distributed model checking * mCRL2 Toolset,
Boost Software License Boost is a set of library (computing), libraries for the C++ programming language that provides support for tasks and structures such as linear algebra, pseudorandom number generator, pseudorandom number generation, multithreading, image proces ...
, 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 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 A storm is any disturbed state of the natural environment or the atmosphere of an astronomical body. It may be marked by significant disruptions to normal conditions such as strong wind, tornadoes, hail, thunder and lightning (a thunderstor ...
: A model checker for probabilistic systems. *
TAPAs Tapas () are appetisers or snacks in Spanish cuisine. They can be combined to make a full meal and are served cold (such as mixed olives and cheese) or hot (such as , which are battered, fried baby squid; or , spicy potatoes). In some bars ...
: a tool for the analysis of process algebra *
TAPAAL TAPAAL is a tool for modelling, Computer simulation, simulation and Formal verification, verification of Petri net#Extensions, Timed-Arc Petri nets developed at Department of Computer Science at Aalborg University in Denmark and it is available fo ...
: an integrated tool environment for modelling, validation, and verification of Timed-Arc
Petri Nets A Petri net, also known as a place/transition net (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 grap ...
*
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-te ...
model checker by Leslie Lamport * UPPAAL: an integrated tool environment for modelling, validation, and verification of real-time systems modelled as networks of timed automata * ZingZing
/ref> – experimental tool from
Microsoft Microsoft Corporation is an American multinational corporation and technology company, technology conglomerate headquartered in Redmond, Washington. Founded in 1975, the company became influential in the History of personal computers#The ear ...
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