We present a formal approach to implement fault-tolerance in real-time embedded systems. The fault-intolerant initial system consists of a set of independent periodic tasks scheduled onto a set of fail-silent processors. We transform the tasks such that, assuming the availability of an additional spare processor, the system tolerates one failure at a time (transient or permanent). Failure detection is implemented using heartbeating, and failure masking using checkpointing and roll-back. These techniques are described and implemented by automatic program transformations on the tasks' source programs. The proposed formal approach to fault-tolerance by program transformation highlights the benefits of separation of concerns and allows us to show whether the implementation satisfies real-time constraints.

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.

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.

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

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.

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

This paper reports on an experiment to add concurrency to the Cyclone programming language, in order to get a safe concurrent language. The basic model considered is that of FairThreads in which synchronous and asynchronous aspects are mixed. The language Loft implements the FairThreads model in C. In this paper, one uses Cyclone instead of C in the implementation of Loft. Using the multi-threaded version of Boehm's GC, one gets an extension of Cyclone to concurrency which is as safe as Cyclone for sequential code, with some additional safety verifications for concurrent code.

The man-machine interface of a small electronic device like a wristwatch is a crucial component, as more and more functions have to be controlled using a small set of buttons. We propose to use Argos, an automaton-based language for reactive systems, and Larissa, its aspect- oriented extension, to show that several interfaces can be obtained from the same set of basic components, assembled in various ways. This is the basis of a quite general component-based development method for man-machine interfaces.

Aspect-Oriented Programming (AOP) has emerged recently as a language concept for expressing cross-cutting concerns, mainly in ob ject-oriented software. Since then, the concept has been applied to a wide variety of other contexts. In this paper, we explore some cross-cutting concerns for parallel programs of reactive systems: we propose an aspect language, Larissa, and a weaving mechanism, in a core language based on parallel communicating Mealy machines.

Aspect Oriented Programming is a programming language concept for expressing cross-cutting concerns. A key point when dealing with aspects is the notion of interference. Ap- plying several aspects to the same program may lead to un- intended results because of conflicts between the aspects. In this paper, we study the notion of interference for Larissa, a formally defined language. Larissa is the aspect extension of Argos, a StateChart-like automata language designed to program reactive systems. We present a way to weave sev- eral aspects in a less conflict-prone manner, and a means to detect remaining conflicts statically, at a low complexity.

We present an operational model for describing random reactive systems. Some models have already been proposed for this purpose, but they generally aim at performing global reasoning on systems, such as stochastic analysis, or formal proofs. Our goal is somehow less ambitious, since we are rather interested in executing such models, for test- ing or prototyping. But on the other hand, the proposed model is not restricted by decidability issues. Therefore it can be more expressive: in particular, our model is not restricted to finite-state descriptions. The proposed model is rather general: systems are described as implicit state/transition machines, possibly infi- nite, where probabilities are expressed by means of relative weights. The model itself is more an abstract machine than a programming language. The idea is then to propose high-level, user-friendly languages that can be compiled into the model. We present such a language, based on regular expressions, together with its translation into the model.

Lurette is an automated testing tool dedicated to reactive programs. The test process is automated at two levels: given a formal description of the System Under Test (SUT) environment, Lurette generates realistic input sequences; and, given a formal description of expected properties, Lurette performs the test results analysis. Lurette has been re-implemented from scratch. In this new version, the main novelty lies in the way the SUT environment is described. This is done by means of a new language called Lucky, dedicated to the programming of probabilistic reactive systems. This article recalls the principles of Lurette, briefly presents the Lucky language, and describes some cases studies from the IST pro ject Safeair II. The ob jective is to illustrate the usefulness of Lurette on real case studies, and the expressiveness of Lucky in accurately describing SUT environments. We show in particular how Lurette can be used to test a typical fault-tolerant system; we also present case studies conducted with Hispano-Suiza and Renault.

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 al l the pro- grams from the basic language still make sense in the ex- tended 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 seman- tics for the extension, it is light to implement in an exist- ing 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.

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 has been a long-term research topic through which several solutions have emerged. In this paper, we pursue this effort and generalize exist- ing 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.

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 process- ing. 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 de- lays 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.

In this paper, we advocate for a seamless design-flow for embedded reactive programs. We particularly concentrate on the use of assume-guarantee contracts (as a form of non-deterministic specification) and present how these can be used for early execution of reactive specifications. We illustrate the approach on a case-study taken from an avionic application, trying to show the implications of this simulation method on the design-flow.

La programmation de systèmes réactifs tels que les simulateurs de systèmes dynamiques ou les jeux vidéo est une tâche difficile. Les techniques classiques pour programmer ces systèmes sont fondées sur l'utilisation de bibliothèques de threads ou de programmation événementielle. Nous introduisons ici le langage ReactiveML comme une alternative à ces pratiques. Le langage est une extension de OCaml fondée sur le modèle réactif synchrone de Boussinot. Ce modèle reprend des principes du synchrone tels que la composition parallèle déterministe et la communication par diffusion. Il les combine à des mécanismes de création dynamique de processus. Cet article présente le langage, son système de type et sa sémantique.