Model Checking

Given a formal model of the system and a formal specification of the properties, model checking provides automated procedures to prove or disprove that the system satisfies the property. This is achieved via an exhaustive examination of the state space.

Method Purpose Short description of the method's purpose and main benefits

Method description A detailed description of the method

Model checking [MCH1, MCH2, MCH3] is a method to verify if a model of the system under verification satisfies its specification. Many languages to write the model exist and range from finite-state to infinite-state machines, from discrete-time to timed or hybrid systems, from non-deterministic automata to stochastic models, from synchronous to asynchronous communicating programs. Given a formal semantics of the input language, model checking can also be applied to models defined for other purposes (architectural description or simulation) or directly to software or hardware source code.
Also, for the property specification, there is a wide range of options, ranging from simple reachability or invariant properties, to temporal properties, from safety to liveness properties. Depending on the modelling language, temporal properties can be specified in various logics, either propositional or first-order, discrete or continuous or hybrid time, linear or branching or probabilistic or hyper-properties logic.
The model checking problem is solved algorithmically by a procedure that decides if the model satisfies the property or finds a counterexample that shows how the model violates it. When the problem is undecidable (as for example for software), the model checking procedure may be incomplete.
Explicit-state model checkers (such as Spin [MCH4]) prove the property by enumerating the reachable states of the model. Symbolic model checkers [MCH5] (such as nuXmv [MCH6]) represent states and transition symbolically and perform the search by means of logical operations. Modern model checkers combine various techniques, integrating explicit-state search with deductive and abstraction refinement techniques.
Automated abstraction [MCH7], in particular, predicate abstraction [MCH8, MCH9], refined according to the encountered false counterexamples to the property being verified using the so-called CEGAR loop [MCH10], is successful especially in software verification.
Approaches based on bounded model checking [MCH11, MCH12, MCH13] explore the state space up to a certain bound. Although they do not provide sound results in general to prove universal properties, they are very successful in practice in finding counterexamples. In case of symbolic model checking, they typically exploit the efficiency of the underlying SAT or SMT solvers.
Other effective and efficient SAT-based model checking techniques are based on generalization of induction such as k-induction [MCH14] and IC3 [MCH15], and their integration with implicit predicate abstraction [MCH16, MCH17].
Various competitions exist to evaluate and compare model checkers on different kinds of benchmarks, with focus on hardware [MCH18], software [MCH19], or other logical formats such as horn clauses [MCH20].

Method Strengths A listof the strengths of the method

Automatic - making model checkers relatively easy to use;
Can check for specific properties without verifying the full system;
Exhaustively explores the state space;
Well-established verification tools and techniques with industrial applications.

Method Limitations The limitations of the method

Exhaustively explores the state space so careful consideration has to be taken regarding the inputs (models and properties to be checked);
The size of the state space is often exponential in the number of variables and the number of components of the system which execute in parallel.

Method References Bibliography references to papers about the method.

[MCH1] Edmund M. Clarke, Orna Grumberg, Doron A. Peled: Model checking. MIT Press 1999, ISBN 978-0-262-03270-4
[MCH2] Christel Baier, Joost-Pieter Katoen: Principles of model checking. MIT Press 2008, ISBN 978-0-262-02649-9, pp. I-XVII, 1-975
[MCH3] Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, Roderick Bloem: Handbook of Model Checking. Springer 2018, ISBN 978-3-319-10574-1
[MCH4] G. J. Holzmann: The SPIN Model Checker - primer and reference manual. Addison-Wesley 2004, ISBN 978-0-321-22862-8, pp. I-XII, 1-596
[MCH5] Kenneth L. McMillan: Symbolic model checking. Kluwer 1993, ISBN 978-0-7923-9380-1, pp. I-XV, 1-194
[MCH6] Roberto Cavada, Alessandro Cimatti, Michele Dorigatti, Alberto Griggio, Alessandro Mariotti, Andrea Micheli, Sergio Mover, Marco Roveri, Stefano Tonetta: The nuXmv Symbolic Model Checker. CAV 2014: 334-342
[MCH7] E. Clarke, O. Grumberg, and D. Long. Model Checking and Abstraction. Trans. Program. Lang. Syst., 16(5):1512–1542, 1994.
[MCH8] Graf, S., Saidi, H.: Construction of Abstract State Graphs with PVS. Proc. of CAV’97, LNCS 1254, Springer, 1997.
[MCH9] Flanagan, C., Qadeer, S.: Predicate Abstraction for Software Verification. Proc. of POPL’02, ACM, 2002.
[MCH10] E. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith. Counterexample-Guided Abstraction Refinement for Symbolic Model Checking. J. ACM, 50(5):752–794, 2003.
[MCH11] Armin Biere, Alessandro Cimatti, Edmund M. Clarke, Yunshan Zhu: Symbolic Model Checking without BDDs. TACAS 1999: 193-207
[MCH12] Clarke, E.M., Biere, A., Raimi, R., Zhu, Y.: Bounded Model Checking Using Satisfiability Solving. Formal Methods Syst. Des. 19(1), 2001.
MCH13] Abhishek Udupa, Ankush Desai, Sriram K. Rajamani: Depth Bounded Explicit-State Model Checking. SPIN 2011: 57-74
[MCH14] Sheeran, M., Singh, S., Stalmarck, G.: Checking Safety Properties Using Induction and a SAT-solver. Proc. of FMCAD’00, LNCS 1954, Springer, 2000.
[MCH15] Bradley, A.R.: SAT-Based Model Checking without Unrolling. Proc. of VMCAI’11, LNCS 6538, Springer, 2011.
[MCH16] Stefano Tonetta: Abstract Model Checking without Computing the Abstraction. FM 2009: 89-105
[MCH17] A. Cimatti, A. Griggio, S. Mover, S. Tonetta: IC3 Modulo Theories via Implicit Predicate Abstraction. TACAS 2014: 46-61
[MCH18] Hardware Model Checking Competition 2020: http://fmv.jku.at/hwmcc20/
[MCH19] International Competition in Software Verification SV-COMP (https://sv-comp.sosy-lab.org/).
[MCH20] P. Rümmer. Competition report: CHC-COMP 2020. https://arxiv.org/abs/2008.02939

Method Dimensions

Evaluation Environment Type Type of environment where the method is applied. It can be more than one type of environment. (Dimension 1)

Evaluation Type Type of evaluation performed with that method. If a method is hybrid, more than one type can be selected. (Dimension 2)

Type of Component Under Evaluation Type of components that can be evaluated with that method. It can be more than one type. (Dimension 3)

Evaluation Stage The evaluation stage where the method is used. (Dimension 5)

Purpose of the Component Under Evaluation The type of purpose that can be evaluated by a method. It can be more than one type. (Dimension 6)

Type of Requirement Under Evaluation The type of requirements that a method is able to evaluate. It can be more than one type. (Dimension 7)

Evaluation Performance Indicator The type of evaluation criteria or KPI that a method is able to improve. It can be more than one type. (Dimension 8)

Relations

Related Methods A method could be related to other methods.

Tools A method can use zero or more tools.

Part Method A method (when it is a combination: Combination of method artefact that is a specialization of a V&V Method) could be composed of a set of V&V Methods.

Test Case or Verification and Validation activity Test Case or V&V activity performed in a Use Case. We will link to the method to the test cases where the method is used.

Standards A method can be linked with standards.

Context

Workflow

Contents

There are currently no items in this folder.