[BGL03] Abstraction as the Key for Invariant Verification
Saddek Bensalem, Susanne Graf, Yassine Lakhnech
In Int. Symposium on Verification celebrating Zohar Manna's 64th Birthday , LNCS 2772, Springer Verlag 2003
We present a methodology for constructing abstractions and refining them by analyzing counter-examples. We also present a uniform verification method that combines abstraction, model-checking and deductive verification. In particular, we show how to use the abstract system in a deductive proof even when the abstract model does not satisfy the specification but simulates the concrete system with respect to a weaker notion of simulation than Milner's.
[Sai98] Combinaison de Methodes Deductives et Algorithmiques pour la Verication
In PhD thesis, obtained from Universite Joseph Fourier - Grenoble I, January 27, 1998 in Grenoble
[GS97] Construction of abstract state graphs with PVS
Susanne Graf and Hassen Saidi
In Proceedings of the 9th Conference on Computer-Aided Verification (CAV'97), Haifa, Israel, June 1997.
In this paper, we propose a method for the automatic construction of an abstract state graph of an arbitrary system using the PVS theorem prover. Given a parallel composition of sequential processes and predicates $p_1 ... p_n$ on the program variables defining an abstract domain, we construct an abstract state graph, starting in the state defined by the values of the predicates $p_1 ... p_n$ in the initial state. The possible successors of a state are computed using the PVS theorem prover by verifying for each $p_i$ if $p_i$ or $\neg p_i$ is a postcondition of it. This allows an abstract state space exploration for arbitrary programs. Using this method, we have automatically verified a bounded retransmission protocol which cannot be proved using backward analysis without providing strong auxiliary invariants.
[Sai97] The Invariant-Checker : Automated Deductive Verification of Reactive Systems
In The Invariant-Checker : Automated Deductive Verification of Reactive Systems , Haifa, Israel, June 1997.Abstract
[LS97] Automatic Verification of Parameterized Networks of Processes by Abstraction
David Lesens and Hassen Saidi
In Proceedings of the 2nd International Workshop on the Verification of Infinite State Systems (INFINITY'97) , Bologna, Italy, July 1997 (appeared in ENTCS)Abstract
experimental results (no more available)
[GS96] Verifying Invariants Using Theorem Proving
Susanne Graf and Hassen Saidi
In Proceedings of 8th Computer-Aided Verification, July 1996, New Brunswick, NJ. LNCS, Springer-Verlag.
We are interested in using a theorem prover in order to verify invariance properties of systems in a systematic ``model checking like'' manner. A system is described as a set of sequential components, each one given by a transition relation and a predicate Init defining the set of initial states. In order to verify that P is an invariant of system S, we try to compute, in an iterative model checking like manner, a predicate P' stronger than P and weaker than Init which is an inductive invariant, that is, whenever P' is true in some state , then P' remains true after the execution of any possible transition. The fact that P' is inductive can be expressed by a set of predicates (having no more quantifiers than P) on the set of program variables, one for every possible transition of the system. In order to prove that P' is inductive, we use either automatic or assisted theorem proving depending on the nature of the formulas to prove. We show in this paper how this can be done in an efficient way. The prover we use is the Prototype Verification System PVS. A tool implementing this verification method is presented.
[BLS96] Powerful Techniques for the Automatic Generation of Invariants
Saddek Bensalem, Yassine Lakhnech, Hassen Saidi
In Proceedings of 8th Computer-Aided Verification , July 1996, New Brunswick, NJ. LNCS, Springer-Verlag.
When proving invariance properties of programs one is faced with two problems. The first problem is related to the necessity of proving tautologies of the considered assertion language, whereas the second manifests in the need of finding sufficiently strong invariants. This paper focuses on the second problem and describes techniques for the automatic generation of invariants. The first set of these techniques is applicable on sequential transition systems and allows to derive so-called local invariants, i.e. predicates which are invariant at some control location. The second is applicable on networks of transition systems and allows to combine local invariants of the sequential components to obtain local invariants of the global systems. Furthermore, a refined strengthening technique is presented that allows to avoid the problem of size-increase of the considered predicates which is the main drawback of the usual strengthening technique. The proposed techniques are illustrated by examples.
[LGBBS95] Property Preserving Abstractions for the Verification of Concurrent Systems
C. Loiseaux, S. Graf, J. Sifakis, A. Bouajjani, S. Bensalem
In Formal Methods in System Design , Vol 6, Iss 1, January 1995
We study property preserving transformations for reactive systems. The main idea is the use of simulations parameterized by Galois connections (alpha,gamma), relating the lattices of properties of two systems. We propose and study a notion of preservation of properties expressed by formulas of a logic, by a function alpha mapping sets of states of a system S into sets of states of a system S'. Roughly speaking, alpha preserves f if the satisfaction of f at some state of S implies that f is satisfied by any state in the image of this state by alpha. We give results on the preservation of properties expressed in sublanguages of the branching time mu-calculus when two systems S and S' are related via (alpha,gamma)-simulations. They can be used in particular to verify a property for a system by proving this property on a simpler system which is an abstraction of it. We show also under which conditions abstraction of concurrent systems can be computed from the abstraction of their components. This allows a compositional application of the proposed verification method. This is a revised version of the papers that appeared in CAV'92 [BensalemBouajjaniLoiseauxSifakis92] and in TAPSOFT'93 [GrafLoiseaux92]; the results are fully developed in the thesis of Claire Loiseaux (in french).
[GL93] Program Verification using compositional Abstraction
S. Graf, C. Loiseaux
In TAPSOFT 93, joint conference CAAP/FASE ,LNCS 668, Springer Verlag
In this paper we describe a method for the obtention of the minimal transition system, representing a communicating system given by a set of parallel processes, avoiding the complexity of the non minimal transition system. We consider minimization with respect to observational equivalence, but the method may be adapted to any other equivalence. An interesting method to achieve this goal is to proceed by stepwise composition and minimization of the components of the system. However, if no precautions are taken, the intermediate state graphs generated by this method may contain a lot of transitions which are impossible in the whole context. We give here a variant of this method which allows to avoid these impossible transitions by taking into account at each composition step a guess of the interface behaviour of the context. This ``interface specification'' must be provided by the user. The method is based on a reduction operator for the composition of a subsystem with its interface specification, which is similar to the parallel operator but introduces undefinedness predicates whereever the interface ``cuts off'' a transition. The parallel operator is defined in a way that these undefinedness predicates disappear again in the full context if and only if the corresponding transition is in fact impossible in the whole system. The efficiency of the method depends in fact on the accuracy with which the designer is able to approximate the possible sequences of the context, but its correctness does not. The proof of the correctness of the method is based on a preorder relation similar to the one defined by Walker.