Model checking
In
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.[2]
An important class of model-checking methods has been developed for checking models of
Model checking is most often applied to hardware designs. For software, because of undecidability (see
The structure is usually given as a source code description in an industrial
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
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,
Historically, the first symbolic methods used
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:[14]
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
- 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,[15] as well as of Olivier Coudert and Jean-Christophe Madre,[16] and the development of open-source BDD manipulation libraries such as CUDD[17] and BuDDy.[18]
- 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 process can be repeated with larger and larger values of until all possible violations have been ruled out (cf. Iterative deepening depth-first search).
- 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.
- 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.[19]
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
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
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 (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 as CSPProcesses
- ISP code level verifier for MPI programs
- Java Pathfinder: an open-source model checker for Java programs
- Libdmc: a framework for distributed model checking
- 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:[21] A model checker for probabilistic systems.
- TAPAs: a tool for the analysis of process algebra
- Petri Nets
- TLA+ 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
- Zing[22] – 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.
See also
- Abstract interpretation
- Automated theorem proving
- Binary decision diagram
- Büchi automaton
- Computation tree logic
- Counterexample-guided abstraction refinement
- Formal verification
- Linear temporal logic
- List of model checking tools
- Partial order reduction
- Program analysis (computer science)
- Static code analysis
References
- ^ For convenience, the example properties are paraphrased in natural language here. Model-checkers require them to be expressed in some formal logic, like LTL.
- ^ Lam K., William (2005). "Chapter 1.1: What Is Design Verification?". Hardware Design Verification: Simulation and Formal Method-Based Approaches. Retrieved December 12, 2012.
- ^ "Amir Pnueli - A.M. Turing Award Laureate".
- ISBN 978-3-540-10003-4
- ^ Edmund M. Clarke, E. Allen Emerson: "Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic". Logic of Programs 1981: 52-71.
- S2CID 52853200
- ISBN 978-3-540-11494-9
- ^ "Press Release: ACM Turing Award Honors Founders of Automatic Verification Technology". Archived from the original on 2008-12-28. Retrieved 2009-01-06.
- ^ USACM: 2007 Turing Award Winners Announced
- ISBN 978-3-319-07012-4.
- ^ 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
- S2CID 2484208.
- S2CID 10190144.
- ISBN 1581130740.
- .
- ISBN 978-0-8186-2055-3.
- ^ "CUDD: CU Decision Diagram Package".
- ^ "BuDDy – A Binary Decision Diagram Package".
- ISBN 978-3-540-67770-3
- S2CID 5856640. Archived from the original(PDF) on 2019-03-03.
- ^ Storm model checker
- ^ Zing
Further reading
- S2CID 5371327.
- ISBN 0-262-03270-8.
- Berard, B.; Bidoit, M.; Finkel, A.; Laroussinie, F.; Petit, A.; Petrucci, L.; Schnoebelen, P. Systems and Software Verification: Model-Checking Techniques and Tools. ISBN 3-540-41523-8.
- Huth, Michael; Ryan, Mark (2004). Logic in Computer Science: Modelling and Reasoning About Systems. Cambridge University Press.
- ISBN 0-321-22862-6.
- Bradfield, Julian; Stirling, Colin (2001). "Modal Logics and mu-Calculi: An Introduction". Handbook of Process Algebra. Elsevier. pp. 293–330. ISBN 978-0-444-82830-9.. JA Bergstra, A. Ponse and SA Smolka, editors." ().
- "Specification Patterns". SAnToS Laboratory, Kansas State University. Archived from the original on 2011-07-19.
- "Property Pattern Mappings for RAFMC". CADP:Construction and Analysis of Distributed Processes. 2019.
- Mateescu, Radu; S2CID 10942856.
- Müller-Olm, M.; Schmidt, D.A.; ISBN 978-3-540-48294-9.
- ISBN 978-0-262-30403-0.
- ISBN 978-3-540-69849-4.
- Emerson, E. Allen (2008). "The Beginning of Model Checking: A Personal Perspective". In Grumberg, Orna; Veith, Helmut (eds.). 25 Years of Model Checking — History, Achievements, Perspectives. LNCS. Vol. 5000. Springer. pp. 27–45. ISBN 978-3-540-69849-4. (this is also a very good introduction and overview of model checking)