Work on verification is a central activity of the Laboratory. It aims
at producing methods and tools for the comparison of programs with specifications
which are either given by a set of properties or by a more abstract program
with which the concrete program is compared modulo some implementation
preorder. The methods studied are based on the analysis of a semantic model
extracted from the program to be verified. Our aim is to provide methods
making the verification process as
Three important criteria have determined our design and implementation choices for verification tools:
Work is performed in the following directions :
A set of complementary enumerative verification techniques have been integrated in the ALDEBARAN verification tool. All these techniques allow to compare an explicit or implicit representation of the transition relation of a program against different types of specifications modulo some appropriate relation. In particular, this tool has efficient decision methods for the comparison modulo various behavioural equivalence or preorder relations defined in process algebras (strong or weak bisimulation, branching bisimulation, simulation relations etc.). These relations are based on abstraction criteria and can be used for compositional reasoning. Thus verifying that a given complex system satisfies a specification can be reduced to the verifying that some abstraction of it obtained by composition of abstractions of its components satisfies the specification. This approach has been successfully applied to the verification of complex systems. ALDEBARAN can be used for the verification of different models such as interpreted Petri nets, transition systems in different formats, in particular the compact format BCG ( Binary Coded Graphs). Furthermore, the OPEN/CAESAR environment allows the guided execution of a C implementation of LOTOS programs covering in that manner the hole spectrum of possibilities between complete verification on the fly and simulation.
In order to know more about these tools click here
Symbolic verification methods use a symbolic representation of the transition relation. The symbolic representations that we have considered so far are
These symbolic representations are used in different tools developed at VERIMAG:
An important research direction is the application of abstract interpretation techniques for verification. These techniques are necessary in the case of infinite state systems but also when the size of the problem makes the application of exact verification methods problematic. Several applications of them are experimented.
An application example is the analysis of timed systems when exact verification methods are not applicable. For instance, decidability is lost for timed systems with multiform time or for most trivial extensions of timed automata. It is shown by using POLKA , that abstract interpretation techniques for properties described as linear constraints on variables give interesting results not only for timed systems but also for some classes of hybrid systems.
Another example of application of abstract interpretation techniques
is the study of abstractions that preserve classes of properties described
in temporal logics. These abstractions correspond to simulation relations
parameterized by a relation between the data domains of a concrete and
an abstract system. The results developed provide conditions for the preservation
of classes of properties from the abstract to the concrete system. This
allows a reduction of the verification of a complex system to some (simpler)
abstraction of it. The method has been experimented by the verification
of complex LOTOS programs using CAESAR/ALDEBARAN.
In case that the verification problem cannot be expressed in a decidable
theory (or the decision procedure for the theory is too expensive), it
can be interesting to use deductive methods, even if it is impossible to
have at once a complete method and complete automatisation. Work done in
this domain aims more for maximal automation than for completeness.
We have implemented a tool that, given a program (a parallel composition
of sequential components) and a safety property (an invariance property)
The structural invariants found in the first step allow very often to decrease significantly the number of iterations necessary in order to find the required predicate.
Each time the tool needs to know the validity of a predicate, it submits this predicate to the theorem prover PVS developed at SRI in which we have implemented tactics allowing to automatize most "simple" proofs (including some very simple tactics doing automatic inductions).
If you want to know more on this tool try here
The generation of test sequences is often one of the most effort and time consuming part in a system development. Classical test generation involves hand writing of the test suites, and no clear-cut interpretation of the test results.
Our work in this domain concerns the formalization of the testing activities and the design and application of tools for automatic test suites generation. The results of these works is illustrated by TGV, which uses formal verification techniques for efficient and automatic generation of conformance test suites.