The rate-synchronous model formalizes an industrial approach for composing Lustre nodes that execute at different rates. Such programs are compiled to cyclic sequential code in two steps. First, an integer linear program is solved to assign each component to a phase relative to its period. Second, the corresponding step functions are ordered for execution within a cycle of the generated code. By default, programs are deterministic: for any valid schedule, the generated code calculates the values decreed by the source dataflow semantics at the specified rates. In practice, though, specifying precise values in the source program is sometimes unnecessary, impracticable, and overly constraining. In this case, the integer linear programming constraints can be relaxed, though not necessarily completely, and their solution decides which dataflow semantics applies. Care is still required to ensure that code generation remains deterministic.

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 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. 2012 ACM Subject Classification Computer systems organization → Real-time languages; Computer systems organization → Embedded software

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.

V´elus [1] is a formally verified compiler for the Lustre synchronous programming language. It is developed in Coq and uses the CompCert C compiler as a back-end. The correctness theorem links the dataflow semantics of the source language to the semantics of the generated assembly code. Its proof is a composition of the individual proofs of each compilation pass. For V´elus it has been proved that repeated execution of the generated assembly code faith-fully implements the dataflow semantics of source programs. To facilitate the compilation correctness proof, the choice was made to model the input language with a relational-style semantics, as shown in the following statement.

Embedded control systems have long been designed using block diagrams and state machines. These models often simply guide the manual implementation of software. But in Model-Based Design they are treated as programs and compiled automatically into low-level code. This is the approach taken in academic languages like Lustre and commercial tools like Simulink and SCADE Suite. This talk presents results from the ongoing Vélus project that aims to specify a compiler for Model-Based Design (Lustre with features from Scade 6) in an Interactive Theorem Prover (Coq). It will describe the model of synchronous streams that gives a semantics to the input language and features of the proof that links this model to the step-by-step model of the generated assembly code. Our prototype builds on the CompCert C compiler and we will talk about some of the challenges of interfacing with such a low-level model of the underlying machine.

Lustre est un langage synchrone a flots de donnees concu pour programmer des systemes embarques. Dans le cadre du projet Velus, nous avons developpe et formalise dans Coq un compilateur qui accepte une forme normalisee du langage et la compile vers du code imperatif. Si cette forme reduite prend en charge un code genere depuis une interface utilisateur basee sur les schemas-blocs, nous voulons offrir au programmeur la possibilite de manipuler le langage complet. Dans cet article nous presentons l'etape de normalisation, qui transforme le langage de programmation en langage normalise. Cette transformation est decomposee en trois etapes afin de simplifier les preuves de correction. Pour etablir la preservation de la semantique, il est necessaire de demontrer que les trois passes preservent certaines proprietes statiques et dynamiques du langage. En particulier, il faut prouver le lien entre le typage des horloges et la semantique dynamique pour pouvoir raisonner sur la suite de la compilation.

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.

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.

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.

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.

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.

This poster presents ongoing research on automatic generation and execution of embedded parallel C code. We target safety-critical avionics programs specified in the synchronous language Lustre. The work described is part of the ITEA 3 project ASSUME (September 2015 - August 2018). ASSUME focuses mainly on embedded software engineering for multi-/many-core platforms. Both synthesis, e.g., automatic code generation, and verification, e.g., static analysis, of programs are addressed in the project. ASSUME is driven by the use cases of its industrial partners. One of these use cases consists in the parallelization of an avionics application comprising about 5500 Lustre nodes. After an overview of the ASSUME project, both parallel code generation and execution on a many-core platform will be presented and demonstrated.

Les langages synchrones sont utilises pour programmer des logiciels de controle-commande d'applications critiques. Le langage Scade, utilise dans l'industrie pour ces applications, est fonde sur le langage Lustre introduit par Caspi et Halbwachs. On s'interesse ici a la formalisation et la preuve, dans l'assistant de preuve Coq, d'une etape clef de la compilation : la traduction de programmes Lustre vers des programmes d'un langage imperatif. Le defi est de passer d'une semantique synchrone flot de donnees, ou un programme manipule des flots, a une semantique imperative, ou un programme manipule la memoire de facon sequentielle. Nous specifions et verifions un generateur de code simple qui gere les traits principaux de Lustre : l'echantillonnage, les noeuds et les delais. La preuve utilise un modele semantique intermediaire qui melange des traits flot de donnees et imperatifs et permet de definir un invariant inductif essentiel. Nous exploitons la formalisation proposee pour verifier une optimisation classique qui fusionne des structures conditionnelles dans le code imperatif genere.