PAMPA project: overview

General overview of the research project

Computer networks are now everywhere. Their size and complexity continue to grow. Therefore the questions raised by the construction of software for these systems are of a great topicality. Even if spectacular progress were accomplished in software engineering methods, the intrinsically parallel and distributed character of the implemented software still poses difficult problems of design and programming. The most sensitive question in our eyes is that of
the control of the software reliability, i.e. the control of the conditions of sound correct operation. Mastering the development passes by the reinforcement of the activities of design, validation and test.

From the point of view of the design, priority is given to object-oriented environments and the invention of specialized "frameworks" for communicating systems integrating validation tools.

From the point of view of validation, the idea is to reinforce the impact of formal methods and analysis tools to allow the debugging of specifications and the generation of tests for the distributed codes.

The approach of the Pampa project consists in contributing to the development of new software technologies by the study of formal models of distributed software and the invention of associated tools. We privilege the design of automatic tools allowing to help the tasks of design, verification, code generation and test of real programs. These tools have vocation to be diseminated in the academic and/or industrial world. The development of models and tools is carried out within the framework of distributed applications located mainly in the field of telecommunication software.

The technical basis of the project is consisted of formal methods in telecommunication software, of the "model-checking " techniques based on efficient traversal of graphs, object-oriented design methods and distributed code generation techniques. The current scientific activity of the project can be structured in three research topics:

1. Verification and Test of Distributed Programs

Verification consists in making sure, that before any implementation, the application will behave correctly. This question is of particular importance for distributed programs, taking into account the complexity of behaviors they
generate. It is essential for critical software. The activity of verification is supplemented by testing the conformance of the implementations. We concentrate on model-based techniques (known as "model-checking"), and particularly on the
algorithmic aspects (on-the-fly algorithmic). We extended these techniques to be able automatically to generate test cases during theverification of prgrams, specified in languages like SDL or LOTOS. That led to an original tool by its algorithmic and its architecture (called TGV), which we develop in partnership with the Vérilog company. Another aspect of testing is the analysis of traces produced by the execution of the implementation under test. To model the phenomena of causality and concurrency, the theory of partial orders is our basic mathematical tool. We have several
applications like the on-the-fly detection of properties, the interoperability testing and the diagnosis of faults in networks. Lastly, to improve its impact, validation (verification/test) must be integrated in environments and existing methods of design. For that, the object paradigm and the UML notations are now impossible to circumvent.

2. Methods and Models for Distributed Object-Oriented Software

A difficult scientific question is to be able to build reliable and effective software architectures, while taking of account the problems involved in parallelism and distribution. Our approach, founded on the idea of re-use of tested solutions, is the identification of specific application models (example of the SPMD model for distributed scientific computing or of CORBA for the telecom objects), and the definition of design frameworks including validation tools.

3. New Formal Models for Telecommunication Software

The validation of object-oriented software, the need for formally reasoning on heterogeous high-level specifications, lead us to propose new semantics models will be able to then lead to new analyses or transformations. We focus ourselves on the behavioral aspects of the models which one represents by families of partial orders. We propose the BDL formalism, in collaboration with the EP-ATR group at IRISA, to study an synchronous-asynchronous mixed
semantics to be able to make profit distributed asynchronous systems from the synchronous technology of compilation.
The analysis of MSCs, the MaxPlus analysis form part of the reflexions of this topic upstream which has vocation to prepare the prototypes of the future. UML plays the role of a federator notation.