Speaker: Marc Pouzet and Louis Mandel

Title: （A) Synchrony:what is it (in hardware and software) ?

 （B）Synchrony:programming languages and verification tools

     （C)Synchrony: the challenges

 

 

 

 

We shall first introduce the notion of synchrony in hardware and software, before to describe a synchronous programming language and its verification tools based on SCADE, which is used, in particular, for the development of software for airplanes all over the world, including China. We shall then describe the main current challenges, in particular, the integration of time models in synchronous languages.

Title: Some recent developments and extensions of Synchronous Languages

 

Abstract: Synchronous languages has been introduced in the 80's for programming embedded control software. The purpose was to allow the designer to model control-systems in a high-level language --- mainly data-flow equations, hierarchical automata and their parallel composition ---, built on a mathematically

precise semantics, and to associate it with static analysis and code generation mechanism insuring that the

target code is equivalent to the source model. All these language share the "synchronous model of time", namely that computations

can be neglected at modeling time because the compiler is

able to generate target code which is proved to run in bounded time and space. Several academic languages were developed, notably Esterel, Lustre, Signal, 

and Lucid Synchrone. The industrial language SCADE 6, based on Lustre and Lucid Synchrone, is now used for the development

of the most critical parts of software in various domains, notably,

avionics, power generation, railways, circuits, etc.

 

The success of the original synchronous languages has spurred the development of new languages, based on the same principles, that increase modularity, expressiveness and that address new applications like real-time video streaming, latency-insensitive designs, large scale simulations, hybrid (continuous/discrete) systems.

 

Lucid Synchrone is one of these new languages. It has served as a basis for experiment with several novel extensions including,

higher-order functions, type systems for the clock calculus,

hierarchical state machines with shared variables, signals and new compilation methods. Many of these ideas have been adopted in commercial tools, notably SCADE 6. New topics include techniques for allowing bounded desynchronisation through buffers (N-synchrony) and extensions for modeling continuous systems.

 

During my talk, I will present the mathematical principles of synchronous languages, the major extensions that

has been done in the past, notably the mix of data-flow with hierarchical automata. Then, I will detail two 

recent research development: (i) the extension of synchronous languages to deal with computer intensive applications

that communicate through bounded FIFOs (e.g., TV boxes); (ii) the treatment of discrete and continuous-time

to model, in a unified manner, both a discrete controller and its physical environment described by Ordinary Differential Equations (ODEs).

 

 

Marc Pouzet is Professor at Université Pierre et Marie Curie in the Computer Science Department of École normale supérieure, Paris, France. He is also junior member at Institut Universitaire de France. His main research activity concerns programming languages for real-time systems with particular interest in synchronous languages, semantics, type-systems and compilation. He was the main architect and developper of the language Lucid Synchrone and several of his works have been transfered into industrial tools (e.g., SCADE 6). His recent works focus on programming models for computer intensive real-time systems (e.g., TV boxes) and the

extension of synchronous languages with continuous time. In particular, he is interested in the semantics and implementation of hybrid modelers (Simulink, Modelica), the design of a synchronous language with mixed (discrete/continuous signals, and the certification of a Lustre compiler in Coq.