The synchronous group
Research Topics
Dissemination
Cooperation
Teaching & Administration
Hot topics
|
|
 |
20 years ago, the ``synchronous'' team at the Verimag laboratory
proposed the formally-defined synchronous language Lustre, for the
development of critical control software. In 1993, Lustre was
transferred successfully to industry. It is now the core of the
industrial tool SCADE
provided by Esterel-Technologies. SCADE is
used by Airbus, Schneider Electric, and Eurocopter, among others
[more on the story of Lustre/SCADE].
In parallel, the team has worked on general validation techniques such as
model-checking, abstract interpretation,
test, simulation, and debugging.
These techniques have been implemented in tools connected to Lustre, and applied to industrial case-studies.
Lustre and these tools can now be used as a validation tool-box for a
wide variety of embedded systems.
This verification tool-box can be used for various (not necessarily synchronous)
formalisms provided that they can be given a semantics in Lustre.
For example, gateways to Lustre exist for
Simulink, Stateflow,
and SystemC.
The tools are connected to each other
via textual formats.
The present activities of the team are organised into five
long-term research topics, listed below. The short-term projects are
usually transverse to this structure
[more on projects].
On September 28th, 2004, Paul
Caspi and Nicolas Halbwachs received the
Monpetit price from the Academy of Sciences, for their work on
synchronous languages.
|
 |
Language Design
Based on our experience in proposing languages that are both formally
defined and adapted to industrial practices, part of our work is
devoted to language design: Lustre extensions, new synchronous languages
mixing control and dataflow, languages for the description of
non-deterministic environments, aspect-oriented programming for reactive
systems, etc.
[more on this topic].
Verification Techniques
The team develops and distributes the model-checker Lesar. The
abstract-interpretation tool Nbac was originally developed by the
team. We still work on general verification techniques, mixing
model-checking and abstract interpretation
[more on this topic].
|
 |
Implementation for Distributed Architectures
The problem of compiling synchronous languages efficiently for
simple mono-processor architectures without operating systems was
solved several years ago, and is implemented in several tools (the
SCADE certified compiler, our academic compiler, etc.) The team now
works on non-classical implementations, typically for distributed
architectures. We study new implementation techniques mixing
time-triggered and event-triggered execution schemes. We also study
the problems due to the implementation of a discrete controller in a
continuous world. The latter point is done in cooperation with the
Timed and Hybrid Systems group
[more on this topic].
|
Test, Simulation and Early Execution
Testing is complementary to formal verification. We are developing a
complete solution for embedded systems, covering: the formal
description of the non-deterministic environments, the automatic
generation of realistic test sequences, the description of oracles,
and the automatic execution of tests. Recently, this testing
activity has been opened to include general simulation mechanisms for
non-deterministic parallel processes and early-execution techniques
[more on this topic].
|
 |
Heterogeneous Components for Embedded Systems and model-driven Development
This last topic studies the use of the Lustre tool-box, together with
several other formal specification languages, for the development of
heterogeneous components for embedded systems. Heterogeneous means
that we deal with hardware or software components, that can be detailed
or abstract in time, detailed or abstract in data, synchronous or
asynchronous.
We propose a notion of ``contract'' for embedded components, and study
a notion of comparison between levels of abstraction. All the
design techniques proposed here are based on the tools
provided by the two previous topics.
For example, Lustre is used as a target for other languages such as
Simulink, Stateflow,
or SystemC.
This work is carried out particularly in the framework of the
RISE
IST and the ALIDECS ACI projects.
[more on this topic].
|
Last modified: Mon Feb 19 10:10:37 MET 2007
|
