Model checking

from Wikipedia, the free encyclopedia

Model Checking (German also model test ) is a method for fully automated verification of a system description (model) for a specification (formula). The term is motivated by the mathematical formulation of the problem: For a given system description and a given logical property , check whether model is for (formal ).

The method is called fully automatic because it does not require any user interaction (in contrast to some deductive methods, such as interactive theorem proving ). The system description takes place in a formal language, for example by a program , a finite automaton or a transition system . The state space of the system does not necessarily have to be finite, but finitely representable. The specification is the formal property of the system to be verified, given for example by a temporal-logical formula or by an observation machine.

principle

The model checker inputs the system description and specification. If the system description meets the specification, the algorithm stops and provides a certificate of correctness as output. If the algorithm finds a violation of the specification, the algorithm stops and provides a counterexample as output. This is usually a possible system version that proves the violation of the specification.

Temporal logical logics

The logical formula, the formalized specification, is often a formula of temporal logic . This makes a statement about the behavior of the system to be checked over time (e.g. no deadlock occurs in any execution ). Such properties can be expressed in one of the following commonly used logics:

The modal μ-calculus is an approach based on fixed point operators over the states of the model (in the list of the mentioned logics it represents the most powerful logic and includes the others). In practical use, however, the logics CTL * , CTL and LTL are represented far more frequently.

CTL * represents a superset of the two logics CTL and LTL. Furthermore, statements from CTL and LTL i. A. do not merge.

Types of algorithms of model checking

The algorithms of model checking are divided into two types.

Explicit model checking

Explicit model checking builds up the transition system in a suitable manner and explores it with regard to the property to be checked.

Machine-based LTL model checking

A well-known approach to verifying LTL formulas uses Büchi automata . First of all, both the system to be tested and the property itself are transferred to a Büchi machine. These machines are designated with or .

Now the system fulfills the property if and only if a subset of the admissible system developments described by the property automaton can realize; if the following inclusion relationship applies to the languages ​​described by the Büchi automata :

.

This can be transformed into

.

Again, this is equivalent to

or .

So it is sufficient to construct a Büchi automaton for the negated property and to intersect it with the Büchi automaton designed for the system. If the result describes the empty language, the property is fulfilled. Otherwise, the resulting automaton precisely describes the system developments that led to the failure of the property.

CTL model checking

With CTL formulas , partial formulas are checked for their truth values ​​step by step at the states.

The state space explosion can e.g. B. be counteracted by exploiting symmetries and partial order reduction in order to be able to verify the largest possible transition systems.

Symbolic model checking

Symbolic model checkers are based either on binary decision diagrams (e.g. for CTL formulas ) or on SAT solvers (e.g. for LTL formulas ). In the first case, a BDD (binary decision diagram) is set up for the state transition relation and the achievable states of the formula. In the second case, the model and specification are converted into a propositional formula, which is then checked for satisfiability.

Practical use

Since the beginning of the 1990s, great progress has been made in the performance of the algorithms, which has made the method interesting in practice. In quality assurance when designing large integrated circuits, model checkers are already used in industrial practice. In recent years, model checkers for software have been developed in some research projects.

Extensions

Classic model checking does not include quantitative aspects such as probabilities or costs in the analysis. Therefore, questions such as:

  • What is the probability of a property?
  • Is the probability that the property is fulfilled above / below a given bound?
  • Is the cost necessary to perform the property within a given budget?

Such properties can be expressed in the PCTL * logic , an extension of CTL * that allows the quantification of probabilities.

Implementations

literature

Basic introduction with many examples.
(Considered the first major comprehensive publication, up to now a standard work in the field.)
  • Peled: Software Reliability Methods . Springer-Verlag, 2001. ISBN 0-387-95106-7
  • B. Berard, M. Bidoit, A. Finkel, F. Laroussinie, A. Petit, L. Petrucci, P. Schnoebelen: Systems and Software Verification: Model-Checking Techniques and Tools , ISBN 3-540-41523-8
(In addition to a part with theoretical basics and illustrative examples, the book presents various different tools and their typical areas of application in a second part.)
(In a brief overview, different modeling types and logics and in particular the modal Mu-calculus are presented.)