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: 

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

Home page IRISA homepage
Up Previous Next Franšais