Methodes symboliques pour la verification de processus communicants : etude et mise en oeuvre
Alain Kerbrat · HAL (Le Centre pour la Communication Scientifique Directe) · 1994
This work deals with the formal verification of parallel programs. We are especially interested in methods based on the generation of a model of the program ; verification itself is done on this model. This approach is usually limited by the model size explosion, when we consider real life examples. Our aim is to study and implement techniques allowing to perform the verification despite this size explosion. The techniques presented in this work have in common the use of symbolic methods for the model representation. We first study model reduction techniques. This reduction is done with respect to equivalence relations based on the bisimulation principle. We are especially interested in an algorithm which performs the minimization of a model during its generation (Minimal Model Generation). In a second part, we study two symbolic techniques for model representation~: the first is Binary Decision Diagrams, which allow efficient representation and computations with boolean formulae. The second consists of linear inequalities systems, defined on the program variables ; this representation is known as convex polyhedra. Using these techniques allow to represent and work with models of size unmanageable by enumerative methods. We present the implementation of of comparison and reduction methods using Binary Decision Diagrams, in particular the Minimal Model Generation algorithm. The application of the subsequent tool on several \lotos\ programs allowed to discover the strong points, but also the limits of this symbolic representation. We finally present a static analysis method of protocols, using convex polyhedra. This analysis allows the computation of an upper approximation of program invariants and consequently to verify the truth of properties expressed in terms of program variables.