| |
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.
Members
- Eric Badouel,
research associate, INRIA
- Albert
Benveniste, senior researcher, INRIA
- Benoît
Caillaud, research associate, INRIA, team leader
- Philippe Darondeau,
senior researcher, INRIA
- Laurence Dinh,
administrative assistant
- Bastien Maubert, PhD student, ENS Cachan, Ker
Lann branch,
- Sophie
Pinchinat, Professor, University of Rennes 1
former members of the
project
Software
Team Leader
Benoît Caillaud
tél : +33 2 99 84 74 07
Benoit.Caillaud@irisa.fr
|
