Publications

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.

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.

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.

This article presents a compile-time analysis for tracking the size of data-structures in a statically typed and strict functional language. This information is valuable for static checking and code generation. Rather than relying on depen- dent types, we propose a type-system close to that of ML: polymorphism is used to define functions that are generic in types and sizes; both can be inferred. This approach is convenient, in particular for a language used to program critical embedded systems, where sizes are indeed known at compiletime. By using sizes that are multivariate polynomials, we obtain a good compromise between the expressiveness of the size language and its properties (verification, inference). The article defines a minimal functional language that is sufficient to capture size constraints in types. It presents its dynamic semantics, the type system and inference algorithm. Last, we sketch some practical extensions that matter for a more realistic language.

Vélus est une formalisation d'un langage synchrone à flots de données et de sa compilation dans l'assistant de preuve Coq. Il inclut une définition de la sémantique dynamique du langage, un compilateur produisant du code impératif, et une preuve de bout en bout que le compilateur préserve la sémantique des programmes.

Dans cet article, on spécifie dans Vélus la sémantique de deux structures d'activation présentes dans les compilateurs modernes: switch et déclarations locales. Ces nouvelles constructions nécessitent une adaptation de l'analyse statique de dépendance de Vélus, qui produit un graphe acyclique comme témoin de la bonne formation d'un programme. On utilise ce témoin pour construire un schéma d'induction propre aux programmes bien formés. Ce schéma permet de démontrer le déterminisme du modèle sémantique dans Coq.

Cet article présente un système de vérification et d'inférence statique des tailles de tableaux dans un langage fonctionnel strict statiquement typé. Plutôt que de s'en remettre à des types dépendants, nous proposons un système de types proche de celui de ML. Le polymorphisme sert à définir des fonctions génériques en type et en taille. L'inférence permet une écriture plus légère des opérations classiques de traitement du signal --- application point-à-point, accumulation, projection, transposée, convolution --- et de leur composition ; c'est un atout clef de la solution proposée. Pour obtenir un bon compromis entre expressivité du langage des tailles et décidabilité de la vérification et de l'inférence, notre solution repose sur deux éléments : (i) un langage de types où les tailles sont des polynômes multi-variés et (ii) l'insertion de points de coercition explicites entre tailles dans le programme source. Lorsque le programme est bien typé, il s'exécute sans erreur de taille en dehors de ces points de coercition. Deux usages de la proposition faite ici peuvent être envisagés : (i) la génération de code défensif aux points de coercition ou, (ii) pour les applications critiques ou intensives, la vérification statique des coercitions en les limitant à des expressions évaluables à la compilation ou par d'autres moyens de vérification formelle. L'article définit le langage d'entrée, sa sémantique dynamique, son système de types et montre sa correction. Il est accompagné d'une implémentation en OCaml, dont le code source est accessible publiquement.

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.

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.

In this paper we present ProbZelus the first synchronous probabilistic programming language. ProbZelus conservatively provides the facilities of a synchronous language to write control software, with probabilistic constructs to model uncertainties and perform inference-in-the-loop.

We present the design and implementation of the language. We propose a measure-theoretic semantics of probabilistic stream functions and a simple type discipline to separate deterministic and probabilistic expressions. We demonstrate a semantics-preserving compilation into a first-order functional language that lends itself to a simple presentation of inference algorithms for streaming models. We also redesign the delayed sampling inference algorithm to provide efficient streaming inference. Together with an evaluation on several reactive applications, our results demonstrate that ProbZelus enables the design of reactive probabilistic applications and efficient, bounded memory inference.

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.

Les langages synchrones ont été introduits pour concevoir des systèmes embarqués temps-réel. Ces langages dédiés permettent d'écrire une spécification précise du système, de la simuler, la valider par du test ou de la vérification formelle puis de la compiler vers du code exécutable. Cependant, ils offrent un support limité pour modéliser les comportements non-déterministes qui sont omniprésents dans les systèmes embarqués.

Dans cet article, nous présentons ProbZelus, une extension probabiliste d'un langage synchrone descendant de Lustre. ProbZelus permet de décrire des modèles probabilistes réactifs, c'est-à-dire, en interaction avec un environnement observable. Lors de l'exécution, un ensemble de techniques d'inférence peut être utilisé pour apprendre les distributions de paramètres du modèle à partir de données observées. Nous illustrons l'expressivité de Probzelus avec des exemples comme un détecteur de trajectoire à partir d'observations bruitées, ou un contrôleur de robot capable d'inférer à la fois sa position et une carte de son environnement.

Synchronous reactive languages were introduced for designing and implementing real-time control software. These domain-specific languages allow for writing a modular and mathematically precise specification of the system, enabling a user to simulate, test, verify, and, finally, compile the system into executable code. 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. In this paper we extend Zelus, a synchronous programming language, to deliver ProbZelus, the first synchronous probabilistic programming language. ProbZelus is a probabilistic programming language in that it provides facilities for probabilistic models and inference: inferring latent model parameters from data. We present ProbZelus's measure-theoretic semantics in the setting of probabilistic, stateful stream functions. We then demonstrate a semantics-preserving compilation strategy to a first-order functional core calculus that lends itself to a simple semantic presentation of ProbZelus's inference algorithms. We also redesign the delayed sampling inference algorithm to provide bounded and streaming delayed sampling inference for ProbZelus models. Together with our evaluation on several reactive programs, our results demonstrate that ProbZelus provides efficient, bounded memory probabilistic inference.

Our objective is to model and simulate Cyber-Physical Systems (CPS) such as robots, vehicles, and power plants. The structure of CPS models may change during simulation due to the desired operation, due to failure situations or due to changes in physical conditions. Corresponding models are called multi-mode. We are interested in multi-domain, component-oriented modeling as performed, for example, with the modeling language Modelica that leads naturally to Differential Algebraic Equations (DAEs). This paper is thus about multi-mode DAE systems. In particular, new methods are discussed to overcome one key problem that was only solved for specific subclasses of systems before: How to switch from one mode to another one when the number of equations may change and variables may exhibit impulsive behavior? An evaluation is performed both with the experimental modeling and simulation system Modia, a domain specific language extension of the programming language Julia, and with SunDAE, a novel structural analysis library for multi-mode DAE systems.

Lustre est un langage synchrone pour programmer des systèmes avec des schémas-blocs desquels un code impératif de bas niveau est généré automatiquement. Des travaux récents utilisent l'assistant de preuve Coq pour spécifier un compilateur d'un noyau de Lustre vers le langage Clight de CompCert pour ensuite générer du code assembleur. La preuve de correction de l'ensemble relie la sémantique de flots de Lustre avec la sémantique impérative du code assembleur. Chaque flot dans un programme Lustre est associé avec une “horloge” statique qui représente ses instants d'activation. La compilation transforme les horloges en des instructions conditionnelles qui déterminent quand les valeurs associés sont calculées. Les travaux précédents faisaient l'hypothèse simplificatrice que toutes les entrées et sorties d'un bloc partagent la même horloge. Cet article décrit une façon de supprimer cette restriction. Elle exige d'abord d'enrichir les règles de typage des horloges et le modèle sémantique. Ensuite, pour satisfaire le modèle sémantique de Clight, on ajoute une étape de compilation pour assurer que chaque variable passée directement à un appel de fonction a été initialisée.

Depuis 1999, 39 articles et exposés liés à la programmation synchrone ont été présentés aux JFLA. Ces articles couvrent de nombreux aspects qui illustrent les liens étroits qui existent entre la programmation synchrone et les langages applicatifs : conception de langages, sémantique, typage, compilation, exécution, analyse de programmes, certification de compilateurs. Dans cet article nous revenons sur quelques uns de ces réesultats qui illustrent la proximité des deux domaines.

This paper describes the design and implementation of a comprehensive OCaml interface to the Sundials library of numeric solvers for ordinary differential equations, differential algebraic equations, and non-linear equations. The interface provides a convenient and memory-safe alternative to using Sundials directly from C and facilitates application development by integrating with higher-level language features, like garbage-collected memory management, algebraic data types, and exceptions. Our benchmark results suggest that the interface overhead is acceptable: the standard examples are rarely twice as slow in OCaml than in C, and often less than 50% slower. The challenges in interfacing with Sundials are to efficiently and safely share data structures between OCaml and C, to support multiple implementations of vector operations and linear solvers through a common interface, and to manage calls and error signalling to and from OCaml. We explain how we overcame these difficulties using a combination of standard techniques such as phantom types and polymorphic variants, and carefully crafted data representations.

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 non standard 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; (3) the generation of statically scheduled code for efficient execution.

Our approach has been evaluated in two implementations: the academic language Zelus, 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.

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.

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 from the Simulink standard library 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 as they mix discrete-time and continuous-time signals in unprincipled ways and so are statically forbidden by the type checker.

The experiment is conducted in Zélus, a synchronous language that conservatively extends Lustre with constructs for programming systems that mix discrete-time and continuous-time signals.

The synchronous language Lustre and its descendants have long been used to program and model discrete controllers. 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.

SCADE is a high-level language and environment for developing safety critical embedded control software. It is used for more than twenty years in various application domains like avionics, nuclear plants, transportation, automotive. SCADE has been 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 with the highest standards for safety critical applications.

In 2008, a major revision based on the new language `Scade 6' was released. This language originally combines the Lustre data-flow style with control structures borrowed from Esterel and SyncCharts, compilation and static analyses from Lucid Synchrone to ensure safety properties. This expressiveness increase for SCADE together with a qualified code generator have dramatically widened the scope of applications developed with.

While previous publications have described some of its language constructs and compiler algorithms, no reference publication on `Scade 6' existed so far. In this paper, we come back to the decisions made for its design, illustrate the main language features, static analyses, and the compiler organization in the context of a qualification process.

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. We resolve two key technical challenges. The first is the change from a synchronous dataflow semantics, where pro- grams manipulate streams of values, to an imperative one, where computations manipulate memory sequentially. The second is the verified compilation of an imperative language with encapsulated state to C code where the state is realized by nested records. We also treat a standard control optimiza- tion that eliminates unnecessary conditional statements.

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.

Explicit hybrid systems modelers like Simulink/Stateflow allow for programming both discrete- and continuous-time behaviors with complex interactions between them. An important step 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. This paper addresses this issue for a hybrid modeling language that combines synchronous data-flow equations with Ordinary Differential Equations (ODEs). We introduce the operator last(x) for the left-limit of a signal x. The last(x) operator is used to break causality loops and permits a uniform treatment of discrete and continuous state variables. The semantics of the language relies on non-standard analysis, defining an execution as a sequence of infinitesimally small steps. A signal is deemed causally correct when it can be computed sequentially and only changes infinitesimally outside of announced discrete events like zero-crossings. The causality analysis takes the form of a type system that expresses dependencies between signals. In well-typed programs, (i) signals are provably continuous during integration provided that imported external functions are also continuous, and (ii) sequential code can be generated. The effectiveness of the system is illustrated with several examples written in Zelus, a Lustre-like synchronous language extended with ODEs.

Les langages synchrones sont utilisés pour programmer des logiciels de contrôle-commande d'applications critiques. Le langage Scade, utilisé dans l'industrie pour ces applications, est fondé sur le langage Lustre introduit par Caspi et Halbwachs. On s'intéresse ici à la formalisation et la preuve, dans l'assistant de preuve Coq, d'une étape clef de la compilation : la traduction de programmes Lustre vers des programmes d'un langage impératif. Le défi est de passer d'une sémantique synchrone flot de données, où un programme manipule des flots, à une sémantique impérative, où un programme manipule la mémoire de façon séquentielle. Nous spécifions et vérifions un générateur de code simple qui gère les traits principaux de Lustre : l'échantillonnage, les noeuds et les délais. La preuve utilise un modèle sémantique intermédiaire qui mélange des traits flot de données et impératifs et permet de définir un invariant inductif essentiel. Nous exploitons la formalisation proposée pour vérifier une optimisation classique qui fusionne des structures conditionnelles dans le code impératif généré.

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 ab- straction 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 in- troducing 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 tim- ing parameters to recover soundness.

The paper describes a pragmatic solution to the parallel execution of hard real-time tasks on off-the-shelf embedded multiprocessors. We propose a simple timing isolation protocol allowing computational tasks to communicate with hard real-time ones. Excellent parallel resource utilization can be achieved while preserving timing compositionality. An extension to a synchronous language enables the correct-by-construction compilation to efficient parallel code. We do not explicitly address certification issues at this stage, yet our approach is designed to enable full system certification at the highest safety standards, such as SIL 4 in IEC 61508 or DAL A in DO-178B.

Ten years ago we introduced ReactiveML, an extension of a strict ML language with synchronous parallelism a` 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.

While all ReactiveML programs presented at PPDP'05 still compile, the language has evolved continuously to incorporate novel programming constructs, compilation techniques and dedicated static analyses. ReactiveML has been used for applications that we never anticipated: the simulation of large-scale ad-hoc and sensor networks, an interactive debugger, and interactive mixed music. These applications were only possible due to the efficient compilation of ReactiveML into sequential code, which we present here for the first time. We also present a parallel implementation that uses work-stealing techniques through shared memory. Finally, we give a retrospective view on ReactiveML over the past ten years.

Modeling languages for hybrid systems are cornerstones of embedded systems development in which software interacts with a physical environment. Sequential code generation from such languages is important for simulation efficiency and for producing code for embedded targets. Despite being routinely used in industrial compilers, code generation is rarely, if ever, described in full detail, much less formalized. Yet formalization is an essential step in building trustable compilers for critical embedded software development.

This paper presents a novel approach for generating code from a hybrid systems modeling language. By building on top of an existing synchronous language and compiler, it reuses almost all the existing infrastructure with only a few modifications. Starting from an existing synchronous data-flow language conservatively extended with Ordinary Differential Equations (ODEs), this paper details the sequence of source-to-source transformations that ultimately yield sequential code. A generic intermediate language is introduced to represent transition functions. The versatility of this approach is exhibited by treating two classical simulation targets: code that complies with the FMI standard and code directly linked with an off-the-shelf numerical solver (Sundials CVODE).

The presented material has been implemented in the Zélus compiler and the industrial KCG code generator of SCADE 6.

Concurrent and reactive systems often exhibit multiple time scales. This situation occurs, for instance, in the discrete simulation of a sensor network where the time scale at which agents communicate is very different from the time scale used to model the internals of an agent.

The paper presents reactive domains to simplify the programming of such systems. Reactive domains allow for several time scales to be defined and they enable time refinement, that is, the replacement of a system with a more detailed version, without changing its observed behavior.

Our work applies to the ReactiveML language, which extends an ML language with synchronous programming constructs à la Esterel. We present an operational semantics for the extended language, a type system that ensures the soundness of programs, and a sequential implementation. We discuss how reactive domains can be used in a parallel implementation.

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.

This paper addresses this issue for a hybrid modeling language that combines synchronous Lustre-like data-flow equations with Ordinary Differential Equations (ODEs). We introduce the operator last(x) for the left-limit of a signal x. This operator is used to break causality loops and permits a uniform treatment of discrete and continuous state variables. The semantics relies on non-standard analysis, defining an execution as a sequence of infinitesimally small steps. A signal is deemed causally correct when it can be computed sequentially and only progresses by infinitesimal steps outside of discrete events. The causality analysis takes the form of a simple type system. In well-typed programs, signals are proved continuous during integration.

The effectiveness of this system is illustrated with several examples written in Zélus, a Lustre-like synchronous language extended with hierarchical automata and ODEs.

Antescofo is a 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 the composers to specify musical pieces that mix interacting electronic and classical instruments. This language is developed with and for musicians, it continues to evolve according to their needs. Yet, its formal 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 a few hundred lines whose efficiency compares well with that of the current 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.

Mixed music is about live musicians interacting with electronic parts which are controlled by a computer during the performance. It allows composers to use and combine traditional instruments with complex synthesis sounds and other electronic devices. There are several languages dedicated to the writing of mixed music scores. Among them, the Antescofo language coupled with an advanced score follower allows a composer to manage the reactive aspects of musical performances: how electronic parts interact with a musician. However these domain specific languages do not offer the expressiveness of functional programming. We embed the Antescofo language in a reactive functional pro- gramming language, ReactiveML. This approach offers to the com- poser recursivity, higher order, inductive types, among others as well as a simple way to program complex reactive behaviors thanks to the synchronous parallel model on which ReactiveML is built. This article presents how to program mixed music in ReactiveML through several examples.

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. We propose an extension of the synchronous model of concurrency, called reactive domains, to simplify the pro- gramming of such systems. Reactive domains allow the creation of local time scales and enable refinement, that is, the replacement of an approximation of a system with a more detailed version without changing its behavior as observed by the rest of the program. Our work is applied to the ReactiveML language, which extends ML with synchronous language constructs. We pre- sent an operational semantics for the extended language and a type system that ensures the soundness of programs.

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 which, 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 resulting code is paired with an off-the-shelf numeric solver.

This experiment show that it is possible to build a modeler for explicit hybrid systems à la Simulink/Stateflow on top of an existing synchronous language, using it both as a semantic basis and as a target for code generation.

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.

Through a number of examples, we show how to desynchronize long computations and implement parallel patterns such as fork-join, pipelining and data parallelism. The proposed extension preserves the main static properties of the base language, including static resource bounds and the absence of deadlock, livelock and races. Moreover, we prove that adding or removing futures preserves the underlying synchronous semantics.

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 been only addressed in a restricted manner. Yet, memory optimization becomes a pressing issue when arrays are added to such languages.

This article presents a two-levels solution to the memory optimization problem. It combines a compile-time optimization algorithm, reminiscent of register allocation, paired with language annotations on the source given by the designer. Annotations express in-place modifications and control where allocation is performed. Moreover, they allow external functions performing in-place modifications to be imported safely. Soundness of annotations is guaranteed by a semilinear type system and additional scheduling constraints. A key feature is that annotations for well-typed programs do not change the semantics of the language: removing them may lead to a less efficient code but with the very same semantics.

The method has been implemented in a new compiler for a Lustre-like synchronous language extended with hierarchical automata and arrays. Experiments show that the proposed approach removes most of the unnecessary array copies, resulting in faster code that uses less memory.

Hybrid system modelers have become a corner stone of complex embedded system development. Embedded systems include not only control components and software, but also physical devices. In this area, Simulink is a de facto standard design framework, and Modelica a new player. However, such tools raise several issues related to the lack of reproducibility of simulations (sensitivity to simulation parameters and to the choice of a simulation engine).

In this paper we propose using techniques from non-standard analysis to define a semantic domain for hybrid systems. Non-standard analysis is an extension of classical analysis in which infinitesimal (the ε and η in the celebrated generic sentence for allεthere existsη... of college maths) can be manipulated as first class citizens. This approach allows us to define both a denotational semantics, a constructive semantics, and a Kahn Process Network semantics for hybrid systems, thus establishing simulation engines on a sound but flexible mathematical foundation. These semantics offer a clear distinction between the concerns of the numerical analyst (solving differential equations) and those of the computer scientist (generating execution schemes).

We also discuss a number of practical and fundamental issues in hybrid system modelers that give rise to non reproducibility of results, nondeterminism, and undesirable side effects. Of particular importance are cascaded mode changes (also called “zero-crossings” in the context of hybrid systems modelers).

Lucy-n is a data-flow programming language similar to Lustre extended with a buffer operator. It is based on the n-synchronous model which was initially introduced for programming multimedia streaming applications. In this article, we show that Lucy-n is also applicable to model Latency Insensitive Designs (LID). In order to model latency introduced by wires, we add a delay operator. Thanks to this new operator, a LID can be described by a Lucy-n program. Then, the Lucy-n compiler automatically provides static schedules for computation nodes and buffer sizes needed in shell wrappers.

Hybrid modeling tools such as Simulink have evolved from simulation platforms into development platforms on which simulation, testing, formal verification and code generation are performed. It is thus critical to place them on a firm semantical basis where it can be proven that the results of simulation, compilation and verification are mutually consistent. Synchronous languages have addressed these issues but only for discrete systems. They cannot be used to model hybrid systems with both efficiency and precision.

Following the approach of Benveniste et al., we present the design of a hybrid modeler built from a synchronous language and an off-the-shelf numerical solver. The main novelty is a language which includes control structures, such as hierarchical automata, for both continuous and discrete contexts. These constructs can be arbitrarily mixed with data-flow and ordinary differential equations (ODEs). A type system is required to statically ensure that all discrete state changes are aligned with zero-crossing events and that the function passed to the numerical solver is free of side-effects during integration. We show that well-typed programs can be compiled through a source-to-source translation into synchronous code which is then translated into sequential code using an existing synchronous language compiler.

Based on the presented material, a compiler for a new synchronous language with hybrid features has been developed. We demonstrate its effectiveness on some examples.

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.

Starting from a minimal, yet full-featured, Lustre-like synchronous language, this paper presents a conservative extension where data-flow equations can be mixed with ordinary differential equations (ODEs) with possible reset. A type system is proposed to statically distinguish discrete computations from continuous ones and to ensure that signals are used in their proper domains. We propose a semantics based on non-standard analysis which gives a synchronous interpretation to the whole language, clarifies the discrete/continuous interaction and the treatment of zero-crossings, and also allows the correctness of the type system to be established.

The extended data-flow language is realized through a source-to-source transformation into a synchronous subset, which can then be compiled using existing tools into routines that are both efficient and bounded in their use of memory. These routines are orchestrated with a single off-the-shelf numerical solver using a simple but precise algorithm which treats causally-related cascades of zero-crossings. We have validated the viability of the approach through experiments with the SUNDIALS library.

Hybrid systems modelers have become the corner stone of embedded system development, with Simulink a de facto standard and Modelica a new player. Such tools still raise a number of issues that, we believe, require more fundamental understanding.

In this paper we propose using non standard analysis as a semantic domain for hybrid systems --- non standard analysis is an extension of classical analysis in which infinitesimals (the ε and η in the celebrated generic sentence for allε. there existsη... in college maths) can be manipulated as first class citizens. This allows us to provide a denotational semantics and a constructive semantics for hybrid systems, thus establishing simulation engines on a firm mathematical basis. In passing, we cleanly separate the job of the numerical analyst (solving differential equations) from that of the computer scientist (generating execution schemes).

Synchronous functional languages such as Lustre or Lucid Synchrone define a restricted class of Kahn Process Networks which can be executed with no buffer. Every expression is associated to a clock indicating the instants when a value is present. A dedicated type system, the clock calculus, checks that the actual clock of a stream equals its expected clock and thus does not need to be buffered. The n-synchrony relaxes synchrony by allowing the communication through bounded buffers whose size is computed at compile-time. It is obtained by extending the clock calculus with a subtyping rule which defines buffering points.

This paper presents the first implementation of the n-synchronous model inside a Lustre-like language called LucyN. The language extends Lustre with an explicit "buffer" construct whose size is automatically computed during the clock calculus. This clock calculus is defined as an inference type system and is parametrized by the clock language and the algorithm used to solve subtyping constraints. We detail here one algorithm based on the abstraction of clocks, an idea originally introduced in [60]. The paper presents a simpler, yet more precise, clock abstraction for which the main algebraic properties have been proved in Coq. Finally, we illustrate the language on various examples including a video application.

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 classes executed atomically and statically scheduled without restricting possible feedback loops between input and output? Though this question has been identified by Raymond in the early years of LUSTRE, it has almost been left aside until the recent work of Lublinerman, Szegedy and Tripakis. The problem is proven to be intractable, in the sense that it belongs to the family of optimization problems where the corresponding decision problem --- there exists a solution with size c --- is NP-complete. Then, the authors derive an iterative algorithm looking for solutions for c = 1, 2,... where each step is encoded as a satisfiability (SAT) problem.

Despite the apparent intractability of the problem, our experience is that real programs do not exhibit such a complexity. Based on earlier work by Raymond, the current paper presents a new encoding of the problem in terms of input/output relations. This encoding simplifies the problem, in the sense that it rejects some solutions, while keeping all the optimal ones. It allows, in polynomial time, (1) to identify nodes for which several schedules are feasible and thus are possible sources of combinatorial explosion; (2) to obtain solutions which in some cases are already optimal; (3) otherwise, to get a non trivial lower bound for c to start an iterative combinatorial search. The method has been validated on several industrial examples.

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 classes executed atomically and statically scheduled without restricting possible feedback loops between input and output? Though this question has been identified by Raymond in the early years of Lustre, it has almost been left aside until the recent work of Lublinerman, Szegedy and Tripakis. The problem is proven to be intractable, in the sense that it belongs to the family of optimization problems where the corresponding decision problem --- there exists a solution with size c --- is NP-complete. Then, the authors derive an iterative algorithm looking for solutions for c = 1,2,... where each step is encoded as a SAT problem.

Despite the apparent intractability of the problem, our experience is that real programs do not exhibit such a complexity. Based on earlier work by Raymond, this paper presents a new symbolic encoding of the problem in terms of input/output relations. This encoding simplifies the problem, in the sense that it rejects solutions, while keeping all the optimal ones. It allows, in polynomial time, (1) to identify nodes for which several schedules are feasible and thus are possible sources of combinatorial explosion; (2) to obtain solutions which in some cases are already optimal; (3) otherwise, to get a non trivial lower bound for c to start an iterative combinatorial search.

The solution applies to a large class of block-diagram formalisms based on atomic computations and a delay operator, ranging from synchronous languages such as Lustre or SCADE to modeling tools such as Simulink.

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.

In this paper, we introduce a conservative extension of a synchronous data-flow language close to Lustre, in order to be able to define systems with modes in a more modular way, while insuring the absence of data-races. We show that such a system can be viewed as an object where modes are methods acting on a shared memory. The object is associated to a scheduling policy which specifies the ways methods can be called to build a valid synchronous reaction. We show that the verification of the proper use of an object reduces to a type inference problem using row types introduced by Wand, Rémy and Vouillon. We define the semantics of the extended synchronous language and the type system. The proposed extension has been implemented and we illustrate its use through several examples.

Synchronous data-flow languages such as Lustre manage infinite sequences or streams as basic values. Each stream is associated to a clock which defines the instants where the current value of the stream is present. This clock is a type information and a dedicated type system --- the so-called clock-calculus --- statically rejects programs which cannot be executed synchronously. In existing synchronous languages, it amounts at asking whether two streams have the same clocks and thus relies on clock equality only. Recent works have shown the interest of introducing some relaxed notion of synchrony, where two streams can be composed as soon as they can be synchronized through the introduction of a finite buffer (as done in the SDF model of Edward Lee). This technically consists in replacing typing by sub-typing. The present paper introduces a simple way to achieve this relaxed model through the use of clock envelopes. These clock envelopes are set of concrete clocks which are not necessarily periodic. This allows to model various features in real-time embedded software such as bounded jitter as found in video-systems, execution time of real-time processes and scheduling resources or the communication through buffers. We present the algebra of clock envelopes and its main theoretical properties.

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, 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.

This article presents in full detail the modular compilation of synchronous block diagrams into sequential code. We consider a first-order functional language reminiscent of Lustre, which it extends with a general n-ary merge operator, a reset construct, and a richer notion of clocks. The clocks are used to express activation of computations in the program and are specifically taken into account during the compilation process to produce efficient imperative code. We introduce a generic machine-based intermediate language to represent transition functions, and we present a concise clock-directed translation from the source to this intermediate language. We address the target code generation phase by describing a translation from the intermediate language to Java and C.

We address the design of distributed systems with synchronous dataflow programming languages. As modular design entails handling both architecture 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.

This paper presents a programming experiment of complex network routing protocols for mobile ad hoc networks within the reactive language ReactiveML.

Mobile ad hoc networks are highly dynamic networks characterized by the absence of physical infrastructure. In such networks, nodes are able to move, evolve concurrently and synchronize continuously with their neighbors. Due to mobility, connections in the network can change dynamically and nodes can be added or removed at any time. All these characteristics --- concurrency with many communications and the need of complex data-structure --- combined to our routing protocol specifications make the use of standard simulation tools (e.g., NS-2, OPNET) inadequate. Moreover network protocols appear to be very hard to program efficiently in conventional programming languages.

In this paper, we show that the synchronous reactive model as introduced in the pioneering work of Boussinot matters for programming such systems. This model provides adequate programming constructs --- namely synchronous parallel composition, broadcast communication and dynamic creation --- which allow a natural implementation of the hard part of the simulation. This thesis is supported by two concrete examples: the first example is a routing protocol in mobile ad hoc networks and the simulation focuses only on the network layer. The second one is a routing protocol for sensors networks and the wholes layers are faithfully simulated (hardware, MAC and network layers). More importantly, the physical environment (e.g., clouds) has also been integrated into the simulation using the tool Lucky.

The implementation has been done in ReactiveML, an embedding of the reactive model inside a statically typed, strict functional language. ReactiveML provides reactive programming constructs together with most of the features of Ocaml. Moreover, it provides an efficient execution scheme for reactive constructs which made the simulation of real-size examples (with several thousand of nodes) feasible.

Lucid Synchrone is a programming language dedicated to the design of reactive systems. It is based on the synchronous model of Lustre which it extends with features usually found in functional languages such as higher-order or constructed data-types. The language is equipped with several static analysis, all expressed as special type-systems and used to ensure the absence of certain run-time errors on the final application. It provides, in particular, automatic type and clock inference and statically detects initialization issues or dead-locks. Finally, the language offers both data-flow and automata-based programming inside a unique framework.

Synchronous data-flow languages such as SCADE/Lustre manage infinite sequences or streams as primitive values making them naturally adapted to the description of data-dominated systems. Their conservative extension with means to define control-structures or modes have been a long-term research topic and 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 data-flow languages. Together, they allow for a much more direct and natural programming of systems that combine data-flow and state-machines.

The proposed extension is fully implemented in the new Lucid Synchrone compiler.

Ce chapitre présente Lucid Synchrone, un langage dédié à la programmation de systèmes réactifs. Il est fondé sur le modèle synchrone de Lustre qu'il étend avec des caractéristiques présentes dans les langages fonctionnels tels que l'ordre supérieur ou l'inférence des types. Il offre un mécanisme de synthèse automatique des horloges et permet de décrire, dans un cadre unifié, une programmation flot de données et une programmation par automates.

Ce chapitre est une présentation du langage, destinée à la fois au programmeur cherchant à se familiariser avec celui-ci, mais aussi au chercheur s'intéressant aux systèmes réactifs et aux techniques qui peuvent être appliquées au niveau d'un langage, pour faciliter les activités de spécification, de programmation et de vérification.

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.

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).

Nous présentons ReactiveML, un langage dédié à la programmation de systèmes réactifs complexes tels que les interfaces graphiques, les jeux vidéo ou les problèmes de simulation. Le langage est basé sur le modèle réactif synchrone introduit dans les années 90 par Frédéric Boussinot. Ce modèle combine les principes du modèle synchrone avec la possibilité de créer dynamiquement des processus.

ReactiveML est une extension conservative d'un langage ML avec appel par valeur. Il ajoute des constructions supplémentaires pour décrire les comportements temporels des systèmes. Nous illustrons l'expressivité du langage sur des exemples et donnons une sémantique formelle du noyau du langage. La sémantique exprime les interactions entre les expressions ML et les constructions réactives. Le langage est statiquement typé avec un système d'inférence de type à la Milner.

This paper presents a programming experiment of a complex network routing protocol for mobile ad hoc networks within the ReactiveML language.

Mobile ad hoc networks are highly dynamic networks characterized by the absence of physical infrastructure. In such networks, nodes are able to move, evolve concurrently and synchronize continuously with their neighbors. Due to mobility, connections in the network can change dynamically and nodes can be added or removed at any time. All these characteristics --- concurrency with many communications and the need of complex data-structure --- combined to our routing protocol specifications make the use of standard simulation tools (e.g., NS, OPNET) inadequate. Moreover network protocols appear to be very hard to program efficiently in conventional programming languages.

In this paper, we show that the synchronous reactive model, as introduced in the pioneering work of Boussinot, matters for programming such systems. This model provides adequate programming constructs --- namely synchronous parallel composition, broadcast communication and dynamic creation --- which allow a natural implementation of the hard part of the simulation.

The implementation has been done in ReactiveML, an embedding of the reactive model inside a statically typed, strict functional language. ReactiveML provides reactive programming constructs together with most of the features of Ocaml. Moreover, it provides an efficient execution scheme for reactive constructs which made the simulation of real-size examples feasible. Experimental results show that the ReactiveML implementation is two orders of magnitude faster than the original C version; it was able to simulate more than 1000 nodes where the original C version failed (after 200 nodes) and compares favorably with the version programmed in NAB.

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 Lucid Synchrone. 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.

Clocks in synchronous data-flow languages are the natural way to define several time scales in reactive systems. They play a fundamental role during the specification of the system and are largely used in the compilation process to generate efficient sequential code. Based on the formulation of clocks as dependent types, the paper presents a simpler clock calculus reminiscent to ML type systems with first order abstract types à la Laufer & Odersky. Not only this system provides clock inference, it shares efficient implementations of ML type systems and appears to be expressive enough for many real applications.

One of the appreciated features of the synchronous data-flow approach is that a program defines a perfectly deterministic behavior. But the use of the delay primitive leads to undefined values at the first cycle; thus a data-flow program is really deterministic only if it can be shown that such undefined values do not affect the behavior of the system.

This paper presents an initialization analysis that guarantees the deterministic behavior of programs. This property being undecidable in general, the paper proposes a safe approximation of the property, precise enough for most data-flow programs. This analysis is a one-bit analysis --- expressions are either initialized or uninitialized --- and is defined as an inference type system with sub-typing constraints. This analysis has been implemented in the Lucid Synchrone compiler and in a new Scade-Lustre prototype compiler. It gives very good results in practice.

We express reactive programs in Coq using data-flow synchronous operators. Following Lucid Synchrone approach, synchronous static constraints are here expressed using dependent types. Hence, our analysis of synchrony is here directly performed by Coq typechecker.

This article presents a causality analysis for a synchronous stream language with higher-order functions. This analysis takes the shape of a type system with rows. Rows were originally designed to add extensible records to the ML type system (Didier Rémy, Mitchell Wand). We also restate briefly the coiterative semantics for synchronous streams (Paul Caspi, Marc Pouzet), and prove the correctness of our analysis with respect to this semantics.

This paper presents an extension of a synchronous data-flow language providing full functionality with a modular reset operator. This operator can be considered as a basic primitive for describing dynamic reconfigurations in a purely data-flow framework. The extension proposed here is conservative with respect to the fundamental properties of the initial language: reactivity (i.e, execution in bounded memory and time) and referential transparency are kept. The reset operator is thus compatible with higher-order. This is obtained by extending the clock calculus of the initial language and providing a compilation method. We illustrate the use of this operator by describing an automatic encoding of Mode-automata. All the experiments presented in the paper has been done with Lucid Synchrone, an ML extension of Lustre.