Synchronous block-diagram languages have long been formalized as fixpoints of equations defining stream functions. We apply this approach to a compiler verified in an interactive theorem prover, allowing us to restate its end-to-end correctness theorem: if a program is accepted and has no runtime errors, its input/output behavior is preserved in the generated code. In a functional semantics, it is necessary to model all possible behaviors, including erroneous ones. We show that static typing and dependency analyses correctly rule out all errors except those arising from logical and arithmetic operators. Our definitions supplement existing formal ones, especially for the reset operator, which is both useful in itself and a basis of advanced control structures.

We introduce a systematic approach for automatically creating a visual diagram, akin to the graphical Safety Critical Application Development Environment (SCADE) model, from a Lustre program. This not only saves tedious manual drawing effort but also enables modeling software to automatically provide the developer with different meaningful views for the same program. We also extend the Sequentially Constructive Charts (SCCharts) language with data-flow constructs that adhere to the Lustre semantics, which permits a translation from Lustre to graphical SCCharts. This allows using the SCCharts code generation, simulation, and visualization tooling also for Lustre programs, in addition to the already existing Lustre compilation techniques. Furthermore, we investigate how the sequentially constructive model of computation, used in SCCharts and other synchronous languages, can be used to conservatively extend Lustre. We have implemented and validated this work with the Eclipse-based open-source Kiel Integrated Environment for Layout Eclipse Rich Client (KIELER) framework.

We present an extension of the synchronous-reactive model for specifying multi-rate systems. A set of periodically executed components and their communication dependencies are expressed in a Lustre-like programming language with features for load balancing, resource limiting, and specifying end-to-end latencies. The language abstracts from execution time and phase offsets. This permits simple clock typing rules and a stream-based semantics, but requires each component to execute within an overall base period. A program is compiled to a single periodic task in two stages. First, Integer Linear Programming is used to determine phase offsets using standard encodings for dependencies and load balancing, and a novel encoding for end-to-end latency. Second, a code generation scheme is adapted to produce step functions. As a result, components are synchronous relative to their respective rates, but not necessarily simultaneous relative to the base period. This approach has been implemented in a prototype compiler and validated on an industrial application.

Safety-critical embedded software is routinely programmed in block-diagram languages. Recent work in the Vélus project specifies such a language and its compiler in the Coq proof assistant. It builds on the CompCert verified C compiler to give an end-to-end proof linking the dataflow semantics of source programs to traces of the generated assembly code. We extend this work with switched blocks, shared variables, reset blocks, and state machines; define a relational semantics to integrate these block- and mode-based constructions into the existing stream-based model; adapt the standard source-to-source rewriting scheme to compile the new constructions; and reestablish the correctness theorem.

Scade is a domain-specific synchronous functional language used to implement safety-critical real-time software for more than twenty years. Two main approaches have been considered for its semantics: (i) an indirect collapsing semantics based on a source-to-source translation of high-level constructs into a data-flow core language whose semantics is precisely specified and is the entry for code generation; a relational synchronous semantics , akin to Esterel, that applies directly to the source. It defines what is a valid synchronous reaction but hides, on purpose, if a semantics exists, is unique and can be computed; hence, it is not executable. This paper presents, for the first time, an executable , state-based semantics for a language that has the key constructs of Scade all together, in particular the arbitrary combination of data-flow equations and hierarchical state machines. It can apply directly to the source language before static checks and compilation steps. It is constructive in the sense that the language in which the semantics is defined is a statically typed functional language with call-by-value and strong normalization, e.g., it is expressible in a proof-assistant where all functions terminate. It leads to a reference, purely functional, interpreter. This semantics is modular and can account for possible errors, allowing to establish what property is ensured by each static verification performed by the compiler. It also clarifies how causality is treated in Scade compared with Esterel. This semantics can serve as an oracle for compiler testing and validation; to prototype novel language constructs before they are implemented, to execute possibly unfinished models or that are correct but rejected by the compiler; to prove the correctness of compilation steps. The semantics given in the paper is implemented as an interpreter in a purely functional style, in OCaml.

Dataflow languages allow the specification of reactive systems by mutually recursive stream equations, functions, and boolean activation conditions called clocks. Lustre and Scade are dataflow languages for programming embedded systems. Dataflow programs are compiled by a succession of passes. This article focuses on the normalization pass which rewrites programs into the simpler form required for code generation. Vélus is a compiler from a normalized form of Lustre to CompCert’s Clight language. Its specification in the Coq interactive theorem prover includes an end-to-end correctness proof that the values prescribed by the dataflow semantics of source programs are produced by executions of generated assembly code. We describe how to extend Vélus with a normalization pass and to allow subsampled node inputs and outputs. We propose semantic definitions for the unrestricted language, divide normalization into three steps to facilitate proofs, adapt the clock type system to handle richer node definitions, and extend the end-to-end correctness theorem to incorporate the new features. The proofs require reasoning about the relation between static clock annotations and the presence and absence of values in the dynamic semantics. The generalization of node inputs requires adding a compiler pass to ensure the initialization of variables passed in function calls.

We introduce a systematic approach for automatically creating a visual diagram, akin to a SCADE model, from a Lustre program. This not only saves tedious manual drawing effort but also allows the creation of different views for the same program. Furthermore, we present an extension of the SCCharts language with data-flow constructs that adhere to the Lustre semantics, which in turn permits a translation from Lustre to graphical SCCharts. This allows to use the SCCharts simulation and code synthesis machinery as an alternative to existing Lustre compilation techniques. Finally, we investigate how the sequentially constructive model of computation underlying SCCharts can be used to conservatively extend Lustre, thus providing a deterministic semantics to some Lustre programs that would be rejected under its original semantics. We have implemented and validated this work with the Eclipse-based open-source KIELER framework.

Synchronous modeling is at the heart of programming languages like Lustre, Esterel, or Scade used routinely for implementing safety critical control software, e.g., fly-by-wire and engine control in planes. However, to date these languages have had limited modern support for modeling uncertainty --- probabilistic aspects of the software's environment or behavior --- even though modeling uncertainty is a primary activity when designing a control system.

Specifications based on block diagrams and state machines are used to design control software, especially in the certified development of safety-critical applications. Tools like SCADE Suite and Simulink/Stateflow are equipped with compilers that translate such specifications into executable code. They provide programming languages for composing functions over streams as typified by Dataflow Synchronous Languages like Lustre. Recent work builds on CompCert to specify and verify a compiler for the core of Lustre in the Coq Interactive Theorem Prover. It formally links the stream-based semantics of the source language to the sequential memory manipulations of generated assembly code. We extend this work to treat a primitive for resetting subsystems. Our contributions include new semantic rules that are suitable for mechanized reasoning, a novel intermediate language for generating optimized code, and proofs of correctness for the associated compilation passes.

Synchronous Programming ( SP ) is a universal computational principle that provides deterministic concurrency. The same input sequence with the same timing always results in the same externally observable output sequence, even if the internal behaviour generates uncertainty in the scheduling of concurrent memory accesses. Consequently, SP languages have always been strongly founded on mathematical semantics that support formal program analysis. So far, however, communication has been constrained to a set of primitive clock-synchronised shared memory ( csm ) data types, such as data-flow registers, streams and signals with restricted read and write accesses that limit modularity and behavioural abstractions. This paper proposes an extension to the SP theory which retains the advantages of deterministic concurrency, but allows communication to occur at higher levels of abstraction than currently supported by SP data types. Our approach is as follows. To avoid data races, each csm type publishes a policy interface for specifying the admissibility and precedence of its access methods. Each instance of the csm type has to be policy-coherent, meaning it must behave deterministically under its own policy—a natural requirement if the goal is to build deterministic systems that use these types. In a policy-constructive system, all access methods can be scheduled in a policy-conformant way for all the types without deadlocking. In this paper, we show that a policy-constructive program exhibits deterministic concurrency in the sense that all policy-conformant interleavings produce the same input-output behaviour. Policies are conservative and support the csm types existing in current SP languages. Technically, we introduce a kernel SP language that uses arbitrary policy-driven csm types. A big-step fixed-point semantics for this language is developed for which we prove determinism and termination of constructive programs.

SCADE is an environment for developing critical embedded software that is used for more than twenty years in various application domains like avionics, nuclear plants, transportation, automotive. It comes with a language and a code generator which complies with the highest safety standards like DO-178C, IEC 61508, EN 50128, IEC 60880 and ISO 26262. The language has been founded on the pioneering work by Caspi and Halbwachs on Lustre. In 2008, a major revision of the language and compiler, named `Scade 6', was released. One of its novelty was a smooth integration of the traditional dataflow style of Lustre with control-structures inspired from those of Esterel and SyncCharts, with static/dynamic semantics and a compilation inspired from Lucid Synchrone. In particular, it relies on four dedicated type systems - typing, clock calculus, causality analysis, initialization analysis - and a compilation through source-to-source transformations into a minimal clocked data-flow language, based on a Kahn semantics, that is translated to imperative code. One ongoing work is the generation of code for multi-core architectures. Because of the intrinsic deterministic parallelism of Scade, we propose a solution that relies on annotations that specify what must be executed concurrently but do not change the semantics. The paper is a survey of past to ongoing work on Scade 6 lanzuaze definition and implementation.

This paper presents ongoing work to add a modular reset construct to a verified Lustre compiler. We present a novel formal specification for the construct and sketch our plans to integrate it into the compiler and its correctness proof.

Hybrid systems modeling languages that mix discrete and continuous time signals and systems are widely used to develop cyber-physical systems where control software interacts with physical devices. Compilers play a central role, statically checking source models, generating intermediate representations for testing and verification, and producing sequential code for simulation and execution on target platforms. This paper presents a novel approach to the design and implementation of a hybrid systems language, built on synchronous language principles and their proven compilation techniques. The result is a hybrid systems modeling language in which synchronous programming constructs can be mixed with ordinary differential equations (ODEs) and zero-crossing events, and a runtime that delegates their approximation to an off-the-shelf numerical solver. We propose an ideal semantics based on nonstandard analysis, which defines the execution of a hybrid model as an infinite sequence of infinitesimally small time steps. It is used to specify and prove correct three essential compilation steps: 1) a type system that guarantees that a continuous-time signal is never used where a discrete-time one is expected and conversely; 2) a type system that ensures the absence of combinatorial loops; and 3) the generation of statically scheduled code for efficient execution. Our approach has been evaluated in two implementations: the academic language Zélus, which extends a language reminiscent of Lustre with ODEs and zero-crossing events, and the industrial prototype Scade Hybrid, a conservative extension of Scade 6.

The synchronous language Lustre and its descendants have long been used to program and model discrete con-trollers. Recent work shows how to mix discrete and continuous elements in a Lustre-like language called Zélus. The resulting hybrid programs are deterministic and can be simulated with a numerical solver. In this article, we focus on a subset of hybrid programs where continuous behaviors are expressed using timers, nondeterministic guards, and invariants, as in Timed Safety Automata. We propose a source-to-source compilation pass to generate discrete code that, coupled with standard operations on Difference-Bound Matrices, produces symbolic traces that each represent a set of concrete traces.

Differential Algebraic Equation (DAE) systems constitute the mathematical model supporting physical modeling languages such as Modelica, VHDL-AMS, or Simscape. Unlike ODEs, they exhibit subtle issues because of their implicit latent equations and related differentiation index. Multi-mode DAE (mDAE) systems are much harder to deal with, not only because of their mode-dependent dynamics, but essentially because of the events and resets occurring at mode transitions. Unfortunately, the large literature devoted to the numerical analysis of DAEs does not cover the multi-mode case. It typically says nothing about mode changes. This lack of foundations cause numerous difficulties to the existing modeling tools. Some models are well handled, others are not, with no clear boundary between the two classes. In this paper we develop a comprehensive mathematical approach to the structural analysis of mDAE systems which properly extends the usual analysis of DAE systems. We define a constructive semantics based on nonstandard analysis and show how to produce execution schemes in a systematic way.

The correct compilation of block diagram languages like Lustre, Scade, and a discrete subset of Simulink is important since they are used to program critical embedded control software. We describe the specification and verification in an Interactive Theorem Prover of a compilation chain that treats the key aspects of Lustre: sampling, nodes, and delays. Building on CompCert, we show that repeated execution of the generated assembly code faithfully implements the dataflow semantics of source programs.

SCADE is a high-level language and environment for developing safety-critical embedded control software. It has been used for more than twenty years in various application domains like avionics, nuclear plants, transportation, and automotive. SCADE was founded on the synchronous data-flow language Lustre invented by Caspi and Halbwachs. In the early years, it was mainly seen as a graphical notation for Lustre but with the unique and key addition of a code generator qualified to the highest standards for safety-critical applications. In 2008, a major revision based on the new language `Scade 6' was released. This language is an original combination of the Lustre data-flow style with control structures borrowed from Esterel and SyncCharts, and compilation and static analyses from Lucid Synchrone for ensuring safety properties. This increase in expressiveness together with the qualified code generator have dramatically widened SCADE scope of applications. While previous publications have described some of its language constructs and compiler algorithms, no reference publication on `Scade 6' exists to date. In this paper, we recall the decisions made in its design, illustrate the main language features and static analyses, and describe the compiler organization developed to satisfy the qualification process.

Hybrid systems modelers like Simulink come with a rich collection of discrete-time and continuous-time blocks. Most blocks are not defined in terms of more elementary ones—and some cannot be—but are instead written in imperative code and explained informally in a reference manual. This raises the question of defining a minimal set of orthogonal programming constructs such that most blocks can be programmed directly and thereby given a specification that is mathematically precise, and whose compiled version performs comparably to handwritten code. In this paper, we show that a fairly large set of blocks of a standard library like the one provided by Simulink can be programmed in a precise, purely functional language using stream equations, hierarchical automata, Ordinary Differential Equations (ODEs), and deterministic synchronous parallel composition. Some blocks cannot be expressed in our setting as they mix discrete-time and continuous-time signals in unprincipled ways that are statically forbidden by the type checker. The experiment is conducted in Zélus, a synchronous language that conservatively extends L ustre with ODEs to program systems that mix discrete-time and continuous-time signals.

Many critical real-time embedded systems are implemented as a set of processes that execute periodically with bounded jitter and communicate with bounded transmission delay. The quasi-synchronous abstraction was introduced by P. Caspi for model-checking the safety properties of applications running on such systems. The simplicity of the abstraction is appealing: the only events are process activations; logical steps account for transmission delays; and no process may be activated more than twice between two successive activations of any other. We formalize the relation between the real-time model and the quasi-synchronous abstraction by introducing the notion of a unitary discretization. Even though the abstraction has been applied several times in the literature, we show, surprisingly, that it is not sound for general systems of more than two processes. Our central result is to propose necessary and sufficient conditions on both communication topologies and timing parameters to recover soundness.

Dataflow synchronous languages such as Lustre have a purely functional semantics. This incurs a high overhead when dealing with arrays, as they have to be copied at each update. We propose to tackle this problem at the source, by constraining programs so that every functional array definition can be optimized into an in-place update. Our solution handles aliasing between function arguments. It also allows more programs with in-place updates to be accepted thanks to a new retiming framework, effectively rescheduling computations across time steps. Our proposed language and compilation method enforces zero-copy purely functional arrays while preserving expressiveness and programmer control through explicit copies.

Hybrid systems modeling languages are widely used in the development of embedded systems. Two representatives are Simulink/Stateflow1that combine Ordinary Differential Equations (ODEs), data-flow and difference equations, hierarchical automata a la StateCharts [14] together with imperative features; and the Modelica language [1]2based on DAEs with features for modeling discrete components. Ptolemy II3is another example in which several models of computation are combined [15]. The formal verification of hybrid systems has been extensively studied [9]. Yet, we share the viewpoint of Lee and Zheng that hybrid modeling languages are best viewed as programming languages that happen to have a hybrid systems semantics [16, 17]. This raises important questions related to their design, semantics and implementation, to get efficient and reliable simulations as well as provably equivalent embedded target code. While sequential code generation in hybrid modeling tools is routinely used for efficient simulation, it is little used or not used at all to produce target embedded code in critical applications that are submitted to strong safety requirements. This results in a break in the development chain: parts of applications must be rewritten into sequential code and all properties verified on the source model cannot be trusted and have to be reverified on the target code.

Ten years ago we introduced ReactiveML, an extension of a strict ML language with synchronous parallelism à la Esterel to program reactive applications. Our purpose was to demonstrate that synchronous language principles, originally invented and used for critical real-time control software, would integrate well with ML and prove useful in a wider context: reactive applications with complex data structures and sequential algorithms, organized as a dynamically evolving set of tightly synchronized parallel tasks.

Explicit hybrid systems modelers like Simulink/Stateflow allow for programming both discrete- and continuous-time behaviors with complex interactions between them. A key issue in their compilation is the static detection of algebraic or causality loops. Such loops can cause simulations to deadlock and prevent the generation of statically scheduled code.

Antescofo is recently developed software for musical score following and mixed music: it automatically, and in real-time, synchronizes electronic instruments with a musician playing on a classical instrument. Therefore, it faces some of the same major challenges as embedded systems. The system provides a programming language used by composers to specify musical pieces that mix interacting electronic and classical instruments. This language is developed with and for musicians and it continues to evolve according to their needs. Yet its semantics has only recently been formally defined. This paper presents a synchronous semantics for the core language of Antescofo and an alternative implementation based on an embedding inside an existing synchronous language, namely ReactiveML. The semantics reduces to a few rules, is mathematically precise and leads to an interpretor of only a few hundred lines. The efficiency of this interpretor compares well with that of the actual implementation: on all musical pieces we have tested, response times have been less than the reaction time of the human ear. Moreover, this embedding permitted the prototyping of several new programming constructs, some of which are described in this paper.

Zélus is a new programming language for modeling systems that mix discrete logical time and continuous time behaviors. From a user's perspective, its main originality is to extend an existing Lustre-like synchronous language with Ordinary Differential Equations (ODEs). The extension is conservative: any synchronous program expressed as data-flow equations and hierarchical automata can be composed arbitrarily with ODEs in the same source code. A dedicated type system and causality analysis ensure that all discrete changes are aligned with zero-crossing events so that no side effects or discontinuities occur during integration. Programs are statically scheduled and translated into sequential code that, by construction, runs in bounded time and space. Compilation is effected by source-to-source translation into a small synchronous subset which is processed by a standard synchronous compiler architecture. The resultant code is paired with an off-the-shelf numeric solver.

Concurrent and reactive systems often exhibit multiple time scales. For instance, in a discrete simulation, the scale at which agents communicate might be very different from the scale used to model the internals of each agent.

This session is dedicated to Paul Caspi. It is made of five talks, each of them addressing one aspect of Paul Caspi's contributions to the development of safe embedded software and systems: synchronous languages and models, the implementation of synchronous languages, the relation between functional and synchronous languages, the relation between continuous and discrete models, and the definition of embedded software and systems master curricula. This session is only a selection of recent work; Paul Caspi also worked on dependability and fault-tolerance, code distribution, and formal verification with theorem provers.

Efficiently distributing synchronous programs is a challenging and long-standing subject. This paper introduces the use of futures in a LUSTRE-like language, giving the programmer control over the expression of parallelism. In the synchronous model where computations are considered instantaneous, futures increase expressiveness by decoupling the beginning from the end of a computation.

The generation of efficient sequential code for synchronous data-flow languages raises two intertwined issues: control and memory optimization. While the former has been extensively studied, for instance in the compilation of Lustre and Signal, the latter has only been addressed in a restricted manner. Yet, memory optimization becomes a pressing issue when arrays are added to such languages.

Hybrid modeling tools like Simulink have evolved from simulation platforms into development platforms on which testing, verification and code generation are also performed. It is critical to ensure that the results of simulation, compilation and verification are consistent. Synchronous languages have addressed these issues but only for discrete systems.

Hybrid modelers such as Simulink have become corner stones of embedded systems development. They allow both discrete controllers and their continuous environments to be expressed in a single language. Despite the availability of such tools, there remain a number of issues related to the lack of reproducibility of simulations and to the separation of the continuous part, which has to be exercised by a numerical solver, from the discrete part, which must be guaranteed not to evolve during a step.

This paper addresses the question of producing modular sequential imperative code from synchronous data-flow networks. Precisely, given a system with several input and output flows, how to decompose it into a minimal number of sub-systems executed atomically and statically scheduled without restricting possible feedback loops between input and output?

This paper addresses the problem of designing and implementing complex control systems for real-time embedded software. Typical applications involve different control laws corresponding to different phases or modes, e.g., take-off, full flight and landing in a fly-by-wire control system. On one hand, existing methods such as the combination of Simulink/Stateflow provide powerful but unsafe mechanisms by means of imperative updates of shared variables. On the other hand, synchronous languages and tools such as Esterel or SCADE/Lustre are too restrictive and forbid to fully separate the specification of modes from their actual instantiation with a particular control automaton.

The compilation of synchronous block diagrams into sequential imperative code has been addressed in the early eighties and can now be considered as folklore. However, separate, or modular, code generation, though largely used in existing compilers and particularly in industrial ones, has never been precisely described or entirely formalized. Such a formalization is now fundamental in the long-term goal to develop a mathematically certified compiler for a synchronous language as well as in simplifying existing implementations.

We address the design of distributed systems with synchronous dataflow programming languages. As modular design entails handling both architectural and functional modularity, our first contribution is to extend an existing synchronous dataflow programming language with primitives allowing the description of a distributed architecture and the localization of some expressions onto some processors. We also present a distributed semantics to formalize the distributed execution of synchronous programs. Our second contribution is to provide a type system, in order to infer the localization of non-annotated values by means of type inference and to ensure, at compilation time, the consistency of the distribution. Our third contribution is to provide a type-directed projection operation to obtain automatically, from a centralized typed program, the local program to be executed by each computing resource. The type system as well as the automatic distribution mechanism has been fully implemented in the compiler of an existing synchronous data-flow programming language.

Synchronous data-flow languages such as SCADE LUSTRE manage infinite sequences, or streams, as primitive values making them naturally adapted to the description of dominated systems. Their conservative extension with means to define control-structures or modes has been a long-term research topic through which several solutions have emerged.In this paper, we pursue this effort and generalize existing solutions by providing two constructs: a general form of state machines called parameterized state machines, and valued signals, as can be found in ESTEREL. Parameterized state machines greatly reduce the reliance on error-prone mechanisms such as shared memory in automaton-based programming. Signals provide a new way of programming with multi-rate data in synchronous dataflow languages. Together, they allow for a much more direct and natural programming of systems that combine dataflow and state-machines.The proposed extension is fully implemented in the new LUCID SYNCHRONE compiler.

The design of high-performance stream-processing systems is a fast growing domain, driven by markets such like high-end TV, gaming, 3D animation and medical imaging. It is also a surprisingly demanding task, with respect to the algorithmic and conceptual simplicity of streaming applications. It needs the close cooperation between numerical analysts, parallel programming experts, real-time control experts and computer architects, and incurs a very high level of quality insurance and optimization.In search for improved productivity, we propose a programming model and language dedicated to high-performance stream processing. This language builds on the synchronous programming model and on domain knowledge -- the periodic evolution of streams -- to allow correct-by-construction properties to be proven by the compiler. These properties include resource requirements and delays between input and output streams. Automating this task avoids tedious and error-prone engineering, due to the combinatorics of the composition of filters with multiple data rates and formats. Correctness of the implementation is also difficult to assess with traditional (asynchronous, simulation-based) approaches. This language is thus provided with a relaxed notion of synchronous composition, called n-synchrony: two processes are n-synchronous if they can communicate in the ordinary (0-)synchronous model with a FIFO buffer of size n.Technically, we extend a core synchronous data-flow language with a notion of periodic clocks, and design a relaxed clock calculus (a type system for clocks) to allow non strictly synchronous processes to be composed or correlated. This relaxation is associated with two sub-typing rules in the clock calculus. Delay, buffer insertion and control code for these buffers are automatically inferred from the clock types through a systematic transformation into a standard synchronous program. We formally define the semantics of the language and prove the soundness and completeness of its clock calculus and synchronization transformation. Finally, the language is compared with existing formalisms.

Many embedded reactive programs perform computations at different rates, while still requiring the overall application to satisfy very tight temporal constraints. We propose a method to automatically distribute programs such that the obtained parts can be run at different rates, which we call rate desynchronization . We consider general programs whose control structure is a finite state automaton and with a DAG of actions in each state. The motivation is to take into account long-duration tasks inside the programs: these are tasks whose execution time is long compared to the other computations in the application, and whose maximal execution rate is known and bounded. Merely scheduling such a long duration task at a slow rate would not work since the whole program would be slowed down if compiled into sequential code. It would thus be impossible to meet the temporal constraints, unless such long duration tasks could be desynchronized from the remaining computations. This is precisely what our method achieves: it distributes the initial program into several parts, so that the parts performing the slow computations can be run at an appropriate rate, therefore not impairing the global reaction time of the program. We present in detail our method, all the involved algorithms, and a small running example. We also compare our method with the related work.

We propose a programming model dedicated to real-time video-streaming applications for embedded media devices, including high-definition TVs. This model is built on the synchronous programming model extended with domain-specific knowledge --- periodic evolution of streams --- to allow correct-by-construction properties of the application to be proven by the compiler. These properties include buffer requirements and delays between input and output streams.Such properties are tedious to analyze by hand, due to the combinatorics of video filters, multiple data rates and formats. We show how to extend a core synchronous data-flow language with a notion of periodic clocks, and to design a relaxed clock calculus (a type system for clocks) to allow non strictly synchronous processes to be composed. This relaxation is associated with a subtyping rule in the clock calculus. Delay, buffer insertion and control code for these buffers are automatically inferred from the clock types through a systematic program transformation.

This paper presents an extension of a synchronous data-flow language such as Lustre with imperative features expressed in terms of powerful state machine à la SyncChart. This extension is fully conservative in the sense that all the programs from the basic language still make sense in the extended language and their semantics is preserved.From a syntactical point of view this extension consists in hierarchical state machines that may carry at each hierarchy level a bunch of equations. This proposition is an alternative to the joint use of Simulink and Stateflow but improves it by allowing a fine grain mix of both styles.The central idea of the paper is to base this extension on the use of clocks, translating imperative constructs into well clocked data-flow programs from the basic language. This clock directed approach is an easy way to define a semantics for the extension, it is light to implement in an existing compiler and experiments show that the generated code compete favorably with ad-hoc techniques. The proposed extension has been implemented in the ReLuC compiler of Scade/Lustre and in the Lucid Synchrone compiler.

We present ReactiveML, a programming language dedicated to the implementation of complex reactive systems as found in graphical user interfaces, video games or simulation problems. The language is based on the reactive model introduced by Boussinot. This model combines the so-called synchronous model found in Esterel which provides instantaneous communication and parallel composition with classical features found in asynchronous models like dynamic creation of processes.The language comes as a conservative extension of an existing call-by-value ML language and it provides additional constructs for describing the temporal part of a system. The language receives a behavioral semantics á la Esterel and a transition semantics describing precisely the interaction between ML values and reactive constructs. It is statically typed through a Milner type inference system and programs are compiled into regular ML programs. The language has been used for programming several complex simulation problems (e.g., routing protocols in mobile ad-hoc networks).

The paper introduces a higher-order synchronous data-flow language in which communication channels may themselves transport programs. This provides a mean to dynamically reconfigure data-flow processes. The language comes as a natural and strict extension of both lustre and lucy. This extension is conservative, in the sense that a first-order restriction of the language can receive the same semantics.We illustrate the expressivity of the language with some examples, before giving the formal semantics of the underlying calculus. The language is equipped with a polymorphic type system allowing types to be automatically inferred and a clock calculus rejecting programs for which synchronous execution cannot be statically guaranteed. To our knowledge, this is the first higher-order synchronous data-flow language where stream functions are first class citizens.

International audience

Synchronous data-flow is a programming paradigm which has been successfully applied in reactive systems. In this context, it can be characterized as some class of static bounded memory data-flow networks. In particular, these networks are not recursively defined, and obey some kind of "synchronous" constraints (clock calculus). Based on Kahn's relationship between data-flow and stream functions, the synchronous constraints can be related to Wadler's listlessness, and can be seen as sufficient conditions ensuring listless evaluation. As a by-product, those networks enjoy efficient compiling techniques. In this paper, we show that it is possible to extend the class of static synchronous data-flow to higher order and dynamical networks, thus giving sense to a larger class of synchronous data-flow networks.This is done by extending both the synchronous operational semantics, the clock calculus and the compiling technique of static data-flow networks, to these more general networks.