|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:
- methods and models for distributed object-oriented software,
- new formal models for telecommunication software.
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
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