Model-checking

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.