[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
Abstract
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
Hassen Saidi
In PhD thesis, obtained from Universite Joseph Fourier - Grenoble I, January 27, 1998 in Grenoble
Abstract
to come
[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.
Abstract
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
Hassen Saidi
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)
Abstractexperimental 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.
Abstract
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.
Abstract
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
Abstract
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
Abstract
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.