Task T1.1: Abstraction

Abstraction techniques are used to construct faithful models which can be analyzed automatically. Abstraction is necessary in order (1) to reduce the validation problem of complex systems to the analysis of manageable (may be infinite-state) models and (2) to tackle the state explosion problem. Abstraction techniques have been developed in our project for various kinds of systems. Theses techniques are combined with other techniques such as symbolic reachability analysis and static analysis techniques (e.g., program slicing).

1. In [ABLS01] (D1,D2), abstraction techniques based on symbolic reachability analysis are introduced in order to verify safety and liveness properties of infinite-state models which are timed counter automata with parametric guards.
2. In [BLS01,BSBL01] (D2), abstraction techniques are introduced in order to analyze classes of parametrized networks with an arbitrary number of components.
3. In [LBOB01] (D1), a methodology for constructing abstractions and refining them by analyzing counter-examples. The paper show also a novel and uniform verification method based on combining abstraction, model-checking and deductive techniques.
4. In [BFG01,GJ01] (D1) abstraction techniques inspired from static analysis techniques, such as live variable analysis and program slicing, are used in the framework of the validation (verification and test case generation) of real industrial case studies.
5. In [PRZ01,APR+01] (D2), a method is presented where techniques based on abstraction and finite state model-checking are used both in deriving automatically candidate induction assertions, and to prove that the candidate assertions are indeed inductive. The efficiency of the method is demonstrated through verification of several types of parametrized systems such as mutual exclusion protocols and cache coherence protocols.