Model-checking

Documents and media

Download support

pdf (931.35 KB)

Abstract

This lecture concludes the general presentation of formal verification methods with model-checking. This method is quite different from the previous ones, in that it is primarily concerned with finite-state programs, those for which it is at least conceptually possible to completely unroll all possible executions in finite time and space. What's more, unlike the methods described above, model-checking is primarily concerned with parallel programs. Parallelism can be synchronous, as in the synchronous circuits and languages presented in previous years, or asynchronous, as in communication protocols, networks and distributed algorithms. Model-checking was born in the early 1980s, almost simultaneously in two places: Grenoble with J-P. Queille and J. Sifakis, who developed the CESAR system and its temporal logic, and the USA with E. Clarke and E. Emerson, who developed the CTL temporal logic and the EMV system. This work earned Clarke, Emerson and Sifakis the 2007 Turing Award. They themselves built on the work of Amir Pnueli (Turing Award 1996) on temporal logic. Model-checking has developed considerably since then, and is certainly the most widely used formal method in industry, particularly in circuit CAD.

The basic idea is to construct a graph of all possible executions of a program, called its model. This model can take the form of a Kripke structure (logician and philosopher of modal logic), i.e. a graph where states are labeled by elementary predicates, or a transition structure, where labels are carried by transitions between states. Once constructed, the model becomes independent of the language that generated it. A popular way of reasoning about a model is to use temporal logics, which define temporal properties using elementary properties of states or transitions and quantifiers on the states or paths of its graph. In this way, we can express and verify properties of safety (absence of bugs), such as "at no time can the elevator travel with the door open", absence of execution deadlocks, or liveliness, such as "the elevator will eventually respond to all passenger requests" or "each process will infinitely often obtain the shared resource if it requests it infinitely often".

First, we'll present the most general CTL* logic, which allows state and path quantizations to be arbitrarily nested on Kripke structures. But this highly expressive logic is difficult to use and computationally prohibitively expensive. Two different sub-logics are used: LTL(Linear Temporal Logic), which doesn't quantify on states and therefore only considers linear traces, and CTL, a tree logic that allows quantification on paths, but with restrictions compared to CTL*. These two logics have different expressivities and each has its own advantages and disadvantages, which we will briefly discuss. LTL is the most suitable logic for verifying liveness properties, as shown by L. Lamport (Turing Award 2014) with his TLA+ system. But, on the contrary, it does not allow us to express predicates on the existence of particular computations.

Modeling by transition systems, systematized by R. Milner (Turing Award 1992) in the study of communicating process computations, enables us to compose the executions of these parallel processes much better. A fundamental notion introduced by Milner is bisimulation, a behavioral equivalence that enables fine-grained comparison of what processes can and cannot do. We show that bisimulation reduction provides a very interesting and intuitive alternative to temporal logics for model checking, particularly in conjunction with synchronous languages.

A final way of conducting model checking is to replace temporal formulas with observer programs, which take as input the inputs and outputs of the program to be checked and are responsible for sending a bug signal if they detect an anomaly. In particular, this method is ideal for synchronous languages such as Esterel and Lustre studied in previous years, as observers can be written in these languages in a simpler way than in temporal logic, at least for the safety properties that are most important in their field of application. This method is in fact not disjoint from the previous ones, as temporal formulas are often translated into observer automata for verification purposes.

It should be noted that, in all cases, the program to be verified evolves in an environment which it is important, and often essential, to model using the same techniques. Modeling the environment is not necessarily simpler than modeling the program itself, and, particularly in temporal logic, we need to ensure that the environment model we build is not empty, otherwise all the properties to be verified will become trivially true. This requires us to study the satisfiability of environment formulas, which is not necessarily straightforward.

We conclude the lecture with a brief presentation of model-checking algorithms, which can be divided into two main classes of methods and associated systems. Explicit methods systematically enumerate possible states and transitions. As the size of the model can be gigantic, these methods use massively parallel machines and numerous ways of reducing the complexity of the analysis: on-the-fly calculation of the model and its properties, random exploration of the graph, reduction by symmetry or switching of independent actions, various abstractions, etc. Implicit methods, introduced later, use symbolic representations of state and transition spaces, e.g. using characteristic set functions. Their advantage is that the size of the formulas used to explore the model is no longer associated with the size of the state space, while their disadvantages are that their computation time is difficult to predict and their implementation on parallel machines problematic. Binary Decision Diagrams (BDDs), the oldest of the implicit representations in Boolean calculus, will be studied in the following lecture. Boolean satisfaction (SAT) or modulo theories (SMT) are increasingly becoming the method of choice for implicit model-checking. We'll illustrate this with the well-known example of Sudoku, relevant here even if its solution isn't really temporal model-checking. Like explicit methods, implicit methods call on a number of techniques to combat the exponential explosion in computation time and memory size. They will be studied in the following years.

Finally, we'll focus on two essential properties of model-checkers that make them attractive to users: the fact that they don't require the user to know precisely the techniques they employ, and their ability to produce minimal counterexamples for false properties, which is paramount for both debugging and test generation.