S4 Project

Research Themes


Activity reports





System Synthesis and Supervision, Scenarios

Research Themes

Joint project-team with University of Rennes-1, INSA-Rennes and CNRS.

The objective of the project is the realization by algorithmic methods of reactive and distributed systems from partial and heterogeneous specifications. Methods, algorithms and tools are developed to synthesize reactive software from one or several incomplete descriptions of the system's expected behavior, regarding functionality (synchronization, conflicts, communication), control (safety, reachability, liveness), deployment architecture (mapping, partitioning, segregation), or even quantitative performances (response time, communication cost, throughput).

These techniques are better understood on fundamental models, such as automata, Petri nets, event structures and their timed extensions. The results obtained on these basic models are then adapted to those realistic but complex models commonly used to design embedded and telecommunication systems.

The behavioral views of the Unified Modeling Language (sequence diagrams and statecharts), the High-Level Message Sequence Charts and the synchronous reactive language Signal are the heart of the software prototypes being developed and the core of the technology transfer strategy of the project.

The scientific objectives of the project can be characterized by the following elements:

A focus on a precise type of applications:

The design of real-time embedded software to be deployed over dedicated distributed architectures. Engineers in this field face two important challenges. The first one is related to system specification. Behavioral descriptions should be adaptable and composable. Specifications are expressed as requirements on the system to be designed. These requirements fall into four categories: (i) functional (synchronization, conflict, communication), (ii) control (safety, reachability, liveness), (iii) architectural (mapping, segregation) and (iv) quantitative (response time, communication cost, throughput, etc). The second challenge is the deployment of the design on a distributed architecture. Domain specific software platforms, known as middleware or real-time operating systems or communication layers, are now part of the usual software design process in industry. They provide a specialized and platform-independent distributed environment to higher-level software components. Deployment of software components and services should be done in a safe and efficient manner.

A specific methodology:

The development of methods and tools which assist engineers since the very first design steps of reactive distributive software. The main difficulty being the adequacy of the proposed methods with standard design methods based on components and model engineering, which most often rely on heterogeneous formalisms and require correct by construction component assembly.

Scientific and technological foundations:

Those models and methods which encompass (i) the distributed nature of the systems being considered, (ii) true concurrency, and (iii) real-time.

Team S4 contributes methods, algorithms and tools producing distributed reactive software from partial heterogeneous specifications of the system to be synthesized (functionality, control, architecture, quantitative performances). This means that several heterogeneous specifications (for instance, sequence diagrams and state machines) can be combined, analyzed (are the specifications inconsistent?) and mapped to lower level specifications (for instance, communicating automata, or Petri nets).

The scientific method of Team S4 begins with a rigorous modeling of problems and the development of sound theoretical foundations. This not only allows to prove the correctness (functionality and control) of the proposed transformations or analysis; but can also guarantee the optimality of the quantitative performances of the systems produced with our methods (communication cost, response time).

Synthesis and verification methods are best studied within fundamental models, such as automata, Petri nets, event structures, synchronous transition systems. Then, results can be adapted to more realistic but complex formalisms, such as the UML. The research work of Team S4 is divided in five tracks:

Petri net theory:

This track follows up the main research theme of the former Team Paragraphe at Inria Rennes. In addition to further developments on topics related to the theory of regions, an algebraic theory of nets has been developed.

Scenario languages:

Current research work concentrates on the composition of system views expressed in scenario formalisms such as High-Level Message Sequence Charts (HMSC).

Heterogeneous systems:

This track contributes to the extension, to distributed systems, of the well-established synchronous paradigm. The aim is to provide a unified framework in which both synchronous systems, and particular asynchronous systems (so-called weakly-synchronous systems) can be expressed, combined, analyzed and transformed.

Reactive components:

The design of reusable components calls for rich specification formalisms, with which the interactions of a component with its environment combines expectations of the component about its environment, with guarantees offered in return by the component to its environment.We are investigating questions related to reactive component refinement and composition. We are also investigating a component-based language development environment, where attribute grammars are used to define executable specifications of software components.

Discrete event system synthesis and supervisory control:

Many synthesis and supervisory control problems can be expressed, with full generality, in the quantified mu-calculus, including the existence of optimal solutions to such problems. Algorithms computing winning strategies in parity games (associated with formulas in this logic) provide effective methods for solving such control problems. This framework offers means of classifying control problems, according to their decidability or undecidability, but also according to their algorithmic complexity.


former members of the project


Team Leader

Benoît Caillaud
tél : +33 2 99 84 74 07


Last update: 01 12 2004


version française

--- webmaster@irisa.fr --- ©copyright --