VERIMAG/Synchrone is led by Florence Maraninchi.
More than 20 years ago, the ``synchronous’’ team of 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. See the Lustre and SCADE history on the Esterel Technologies website, and this Wikipedia page.
On September 28th, 2004, Paul Caspi and Nicolas Halbwachs received the Monpetit price from the French Academy of Sciences, for their work on synchronous languages.
Apart from the definition of Lustre, the group 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.
During the last decade, the activities of the group have been extended outside the strict scope of synchronous languages and control systems, to cover most aspects of embedded system design, implementation and validation. The main application domains we are interested in now are: embedded control computer systems, systems-on-a-chip (or, more generally, hardware/software systems in which the hardware is not generic), and sensor networks (or, more generally, networks of embedded systems).
During the last decade, the "Synchrone" team of Verimag worked on stochastic extensions of the synchronous language Lustre. The motivation of synchronous stochastic languages is to simulate the (physical) environment of a reactive system. Reactive systems and programs are particular, in that they usually function in a closed loop with their environment. Simulating the environment is compulsory to be able to test reactive programs with realistic inputs. The industrial partners of the recent Minalogic Comon project have experimented with the tools developed at Verimag. A major result of the project is that our tools and methodology are useful, not only for automated testing, but also for requirement engineering.
The interest among the industrial partners generated by those tools contributed to the creation of the Argosim start-up company in 2013, which aims at industrializing the concepts (random-based simulations of environments, automated testing, and requirements engineering) and the associated technology (stochastic data-flow synchronous language, constraint solving based on BDDs and polyhedra).
The present activities of the group are organized into four long-term research topics:
The short-term projects are usually transverse to this structure.