Temporal logic and model checking

Often different behavior definitions for a given system component are given in different description formalisms. For instance, (a) the behavior of a method (declared in the interface of a given object class) can be desribed by the algorithm of its body - or by input and output assertions concerning its parameters and the values of the state variables of the object instance. Or (b) the behavior of an accepting state machine, may also be defined by a regular expression. And (c), during system development, the reqirements document is more abstract than the design specification, and this is more abstract than the implementation. Also the regular expression, and the input-output assertions may be considered more abstract than the other specification, since it make abstraction from the internal states and variables of the specified component.

In the case of model checking, one considers two behavior descriptions, one usually in an "executable" description language, such as programming language, state machine, or similar, and the other given in Temporal Logic. As we have seen above, temproal logic includes the possibility of defining input-output assertions.

Here is a simple introduction to Model Checking by Girish Keshav Palshikar. This article describes the motivation and gives some examples using the branching time temporal logic CTL, as introduced by Ed Clarke. A PhD student of his team used models in the form of BDD (binary decision diagrams) << see tutorial T1 >>. CTL is also used in the UPPAAL tool (but with some restrictions) - the verification of some properties of an example system is described in Section 3.3 of this article (C). Model checking provides an execution sequence that does not satisfy the desired property as a counter example, if the property is not satisfied.

Recently, model checking using SAT (this is the problem of satisfying a boolean function by selecting appropriate values for the variables occuring as parameters in the function) has been proposed by different authors << see tutoriel  T2 by Clarke>>. In this case the function to be satisfied is the negation of the desired system property, and if the function can be satisfied, a counter-example will be found which shows that the desired property is cannot satisfied. If SAT is unsuccessful for a large space of explored possibilities, one may assume that the property holds. Note that the Alloy tool also uses the SAT technique; Aloy uses a notation related to UML class diagrams for defining models, and searches amoung all possible instantiations (object instant models - within a certain range that can be specified) whether an instant exists that contradicts the desired system property.

The Spin tool provides model checking for linear time temporal logic (see paper by Holzmann (C)). This paper also gives an introduction to linear temporal logic and to the Promela language used for defining models. It also presents some examples.

A good detailed explanation of model checking for CTL and LTL was given by Haddad (we will discuss some of these slides in the course). This tutorial was given within a series of tutorials on formalized modeling of distributed systems (C).

<< I wrote a paper on temporal logic discussing a more complex example involving linear-time temporal logic and specification with assumptions and guarantees [Bochmann 1982]. This was shortly after temporal logic was introduced Pnueli as specification formalism for reactive systems>

Created: September 22, 2014