Model Checking

Model Checking ( German and model testing ) is a method for the fully automatic verification of a system description ( model) against 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 if model is available for (formal).

The method is referred to as fully automatic, since it does not require any user interaction (as opposed to some deductive method, such as interactive theorem ). The system takes place in a formal description language, for example by a program, a finite state machine, or a transition system. The state space of the system is not necessarily finite, but finally be representable. The formal specification is the detected property of the system, if for example, by a temporal or by a logical formula observation point.

Principle

Input of the model checker (English model checkers ) are the system description and the specification. Meets the system specification, the specification, the algorithm stops and returns a correctness certificate as output. If the algorithm finds a violation of the specification, the algorithm stops and returns as output a counterexample. This is usually a possible system design, which demonstrates violating the specification.

Temporal logic logics

The logical formula, the formalized specification is often a formula of a temporal logic. This makes a statement about the behavior of the system to be tested over time ( for example, in any embodiment, there is a deadlock ). Such properties can be expressed in one of the following logics commonly used.

• CTL *
• Linear Time Temporal Logic ( LTL short )
• Modal Mu -Calculus

In the modal μ - calculus is based on a fixed point operators on the states of the model approach ( in the list of specified logics, it represents the most powerful logic and includes the other ). In practical application, the logics CTL *, CTL and LTL, however, are represented far more common.

CTL * is a superset of the two logics CTL and LTL dar. Furthermore, statements from CTL and LTL let iA not transferable.

Types of algorithms of the model checkings

The algorithms of the model checkings are divided into two types.

Explicit Model Checking

Explicit Model Checking builds the transition system to appropriately and explored it with respect to the property to be tested.

Automata -based LTL model checking

A known approach for verifying LTL formulas used Büchi automata. Here, first, both the system to be tested and the property can be transferred even in a Büchi automaton. These machines were designated respectively.

Now the system satisfies the property if and only if a subset of the permitted system evolutions described by the property machine can realize; So if the following inclusion relation holds for the languages ​​described by the Büchi automata:

.

.

Or.

So it suffices for the negated property to construct a Büchi automaton and this to blend with the constructed for the system Büchi automata. Describes the result of the empty language, the property is satisfied. Otherwise, the resulting automaton accurately describes the system evolutions that led to the failure of the property.

CTL model checking

In CTL formulas progressively sub-formulas are checked for their truth values ​​to the states.

The state space explosion can, for example, be counteracted by exploiting symmetries and Partial Order Reduction to verify the largest possible transition systems.

Symbolic Model Checking

Symbolic model checker based on either binary decision diagrams (eg CTL formulas ) or SAT - solvers (eg for LTL formulas ). In the first case ever a BDD ( binary decision diagram german, binary decision diagram ) is set up for the transition relation and the states of the satisfiable formula. In the second case, model and specifications are converted into a propositional formula, which is then checked for satisfiability.

Practical use

Since the early 90s, a lot of progress in the performance of the algorithms has been made, making the process for the practice has become more interesting. In quality assurance in the design of large integrated circuits model checker are already used in industrial practice. In recent years, model checker for software have been developed in several research projects.