Cyber-Physical Systems require distributed architectures to support safety critical real-time control. Kopetz' Time-Triggered Architectures (TTA) have been proposed as both an architecture and a comprehensive paradigm for systems architecture, for such systems. To relax the strict requirements on synchronization imposed by TTA, Loosely Time-Triggered Architectures (LTTA) have been recently proposed. In LTTA, computation and communication units at all triggered by autonomous, non synchronized, clocks. Communication media act as shared memories between writers and readers and communication is non blocking. In this paper we pursue our previous work by providing a unified presentation of the two variants of LTTA (token- and time-based), with simplified analyses. We compare these two variants regarding performance and robustness and we provide ways to combine them.

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.

Synchronous systems offer a clean semantics and an easy verification path at the expense of often inefficient implementations. Capturing design specifications as synchronous models and then implementing the specifications in a less restrictive platform allow to address a much larger design space. The key issue in this approach is maintaining semantic equivalence between the synchronous model and its implementation. We address this problem by showing how to map a synchronous model onto a loosely time-triggered architecture that is fairly straightforward to implement as it does not require global synchronization or blocking communication. We show how to maintain semantic equivalence between specification and implementation using an intermediate model (similar to a Kahn process network but with finite queues) that helps in defining the transformation. Performance of the semantic preserving implementation is studied for the general case as well as for a few special cases.

We present a compositional theory of heterogeneous reactive systems. The approach is based on the concept of tags marking the events of the signals of a system. Tags can be used for multiple purposes from indexing evolution in time (time stamping) to expressing relations among signals, like coordination (e.g., synchrony and asynchrony) and causal dependencies. The theory provides flexibility in system modeling because it can be used both as a unifying mathematical framework to relate heterogeneous models of computations and as a formal vehicle to implement complex systems by combining heterogeneous components. In particular, we introduce an algebra of tag structures to define heterogeneous parallel composition formally. Morphisms between tag structures are used to define relationships between heterogeneous models at different levels of abstraction. In particular, they can be used to represent design transformations from tightly synchronized specifications to loosely-synchronized implementations. The theory has an important application in the correct-by-construction deployment of synchronous design on distributed architectures.

We study the implementation of a synchronous program as a set of multiple tasks running on the same computer, and scheduled by a real-time operating system using some preemptive scheduling policy, such as fixed priority or earliest-deadline first. Multitask implementations are necessary, for instance, in multiperiodic applications, when the worst-case execution time of the program is larger than its smallest period. In this case, a single-task implementation violates the schedulability assumption and, therefore, the synchrony hypothesis does not hold. We are aiming at semantics-preserving implementations, where, for a given input sequence, the output sequence produced by the implementation is the same as that produced by the original synchronous program, and this under all possible executions of the implementation. Straightforward implementation techniques are not semantics-preserving. We present an intertask communication protocol, called DBP, that is semantics-preserving and memory-optimal. DBP guarantees semantical preservation under all possible triggering patterns of the synchronous program: thus, it is applicable not only to time-, but also event-triggered applications. DBP works under both fixed priority and earliest-deadline first scheduling. DBP is a nonblocking protocol based on the use of intermediate buffers and manipulations of write-to/read-from pointers to these buffers: these manipulations happen upon arrivals, rather than executions of tasks, which is a distinguishing feature of DBP. DBP is memory-optimal in the sense that it uses as few buffers as needed, for any given triggering pattern. In the worst case, DBP requires, at most, N + 2 buffers for each writer, where N is the number of readers for this writer.

We address the problem of mapping a set of processes which communicate synchronously on a distributed platform. The Time Triggered Architecture (TTA) proposed by Kopetz for the communication mechanism of a distributed platform offers a direct mapping that would preserve the semantics of the specification. However, its exact implementation may, at times, be problematic as it requires the distributed platform to have the clocks of its components perfectly synchronized. We propose as implementation architecture a relaxation of TTA called Loosely Time-Triggered Architecture (LTTA), in which computing units perform writes into and reads from the communication medium independently, triggered by local, quasi-periodic but non synchronized, clocks. LTTA offers some of the advantages of TTA with lower hardware cost and greater flexibility. So far LTTA was studied for single directional two-users communications over an LTT bus. General topology was not studied. In this paper we propose a design flow that ensures semantics preservation for an LTT communication network with arbitrary topology. Key elements are two new protocols for clock regeneration and predictive traffic shaping. Our approach relies on a mathematical Model of Communication (MoC) that we describe in detail.

In time-sensitive systems writing to and reading from the communication medium is on a purely time-triggered but asynchronous basis. Writes and reads can occur at any time and the data are stored and sustained until overwritten. We study how to maintain data semantics when the duration of the actions change from specification to implementation.In doing so, we rely on tag systems formerly introduced by the authors. The exibility of tag systems allows handling the problem in a formal, yet tractable way.

Recently, we have proposed a set of buffering schemes to preserve the semantics of a synchronous program when the latter is implemented as a set of multiple tasks running under preemptive scheduling. These schemes, however, are not optimal in terms of memory (buffer usage). In this paper we propose a new protocol which generalizes the previous schemes. The new protocol is not only semantics-preserving but also memory-optimal in two senses: first, in terms of the number of buffers required to preserve semantics in the worst case (i.e.,for the "worst" possible arrival/execution pattern of the tasks); second, in terms of the number of buffers required to preserve semantics for any arrival/execution pattern and at any time, assuming no knowledge of future arrivals.

In previous work, we have proposed a method of preserving the functional semantics of model-based designs by the use of static checks and a double-buffer protocol [12]. However, this is restricted to static, fixed-priority scheduling and for high-priority to low-priority communications requires a double buffer to be stored for each pair of communicating tasks. In this paper we extend the method to dynamic-priority scheduling in the form of earliest-deadline-first (EDF) scheduling and show that, although scheduling is dynamic, a static buffering scheme can still be used. We also suggest some memory optimizations of our protocol which still preserve the original functional semantics. Finally, we show how model checking can be used to prove correctness of the scheme.

In safety-critical control systems, the Scade/Lustre development environment has proved its value, with notable achievements such as the Hong-Kong subway signalling system and Airbus A380 flight controls. The interest of the approach comes from the synchronous data-flow style of the Lustre language which makes is well-adapted to the culture of control engineers. At the same time Lustre is endowed with simple formal semantics which makes it amenable to formal development.The currently running Flush project consists of building a formal system development tool on top of it, by taking advantage of the formal properties of the Lustre language. To this end, a refinement calculus is defined, encompassing both functional and temporal aspects. Refinement proof obligations are generated, and several proof approaches can be used to discharge them: model-checking, abstract interpretation, and theorem proving through repeated induction and, finally translation to PVS proof obligations. The resulting methodology is illustrated on the island example used by J.R. Abrial for presenting the B system method.

The design of embedded real-time systems requires skills from multiple specific disciplines, including, but not limited to, control, computer science, and electronics. This often involves experts from differing backgrounds, who do not recognize that they address similar, if not identical, issues from complementary angles. Design methodologies are lacking in rigor and discipline so that demonstrating correctness of an embedded design, if at all possible, is a very expensive proposition that may delay significantly the introduction of a critical product. While the economic importance of embedded systems is widely acknowledged, academia has not paid enough attention to the education of a community of high-quality embedded system designers, an obvious difficulty being the need of interdisciplinarity in a period where specialization has been the target of most education systems. This paper presents the reflections that took place in the European Network of Excellence Artist leading us to propose principles and structured contents for building curricula on embedded software and systems.

We present a method of translating discrete-time Simulink models to Lustre programs. Our method consists of three steps: type inference, clock inference, and hierarchical bottom-up translation. In the process, we explain and formalize the typing and timing mechanisms of Simulink. The method has been implemented in a prototype tool called S2L, which has been used in the context of a European research project to translate two automotive controller models provided by Audi.

We present an extension of a mathematical framework proposed by the authors to deal with the composition of heterogeneous reactive systems. Our extended framework encompasses diverse models of computation and communication such as synchronous, asynchronous, causality-based partial orders, and earliest execution times. We introduce an algebra of tag structures and morphisms between tag sets to define heterogeneous parallel composition formally and we use a result on pullbacks from category theory to handle properly the case of systems derived by composing many heterogeneous components. The extended framework allows us to establish theorems, from which design techniques for correct-by-construction deployment of abstract specifications can be derived. We illustrate this by providing a complete formal support for correct-by-construction distributed deployment of a synchronous design specification over an ltta medium.

The Simulink/Stateflow toolset is an integrated suite enabling model-based design and has become popular in the automotive and aeronautics industries. We have previously developed a translator called Simtolus from Simulink to the synchronous language Lustre and we build upon that work by encompassing Stateflow as well. Stateflow is problematical for synchronous languages because of its unbounded behaviour so we propose analysis techniques to define a subset of Stateflow for which we can define a synchronous semantics. We go further and define a "safe" subset of Stateflow which elides features which are potential sources of errors in Stateflow designs. We give an informal presentation of the Stateflow to Lustre translation process and show how our model-checking tool Lesar can be used to verify some of the semantical checks we have proposed. Finally, we present a small case-study.

We present a layered end-to-end approach for the design and implementation of embedded software on a distributed platform. The approach comprises a high-level modeling and simulation layer (Simulink), a middle-level programming and validation layer (SCADE/Lustre) and a low-level execution layer (TTA). We provide algorithms and tools to pass from one layer to the next. First, a translator from Simulink to Lustre. Second, a set of real-time and code-distribution extensions to Lustre. Third, implementation techniques for decomposing a Lustre program into tasks and messages, scheduling the tasks and messages on the processors and the bus, distributing the Lustre code on the execution platform, and generating the necessary "glue" code.

Twelve years ago, Proceedings of the IEEE devoted a special section to the synchronous languages. This paper discusses the improvements, difficulties, and successes that have occured with the synchronous languages since then. Today, synchronous languages have been established as a technology of choice for modeling, specifying, validating, and implementing real-time embedded applications. The paradigm of synchrony has emerged as an engineer-friendly design method based on mathematically sound tools.

In this article, we definetimed regular expressions, a formalism for specifying discrete behaviors augmented with timing information, and prove that its expressive power is equivalent to thetimed automataof Alur and Dill. This result is the timed analogue of Kleene Theorem and, similarly to that result, the hard part in the proof is the translation from automata to expressions. This result is extended from finite to infinite (in the sense of Büchi) behaviors. In addition to these fundamental results, we give a clean algebraic framework for two commonly accepted formalisms for timed behaviors, time-event sequences and piecewise-constant signals.

The paper addresses the problem of automatically distributing reactive systems. We first show that the use of synchronous languages allows a natural parallel description of such systems, regardless of any distribution problems. Then, a desired distribution can be easily specified, and achieved with the algorithm presented here. This distribution technique provides distributed programs with the same safety, test, and debug facilities as ordinary sequential programs. Finally, the implementation of such distributed programs only requires a very simple communication protocol ("first in first out" queues), thereby reducing the need for large distributed real time executives.

In this paper we define timed regular expressions, and extension of regular expressions for specifying sets of dense-time discrete-valued signals. We show that this formalism is equivalent in expressive power to the timed automata of Alur and Dill by providing a translation procedure from expressions to automata and vice versa. the result is extended to /spl omega/-regular expressions (Buchi's theorem).

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

The authors describe LUSTRE, a data flow synchronous language designed for programming reactive systems-such as automatic control and monitoring systems-as well as for describing hardware. The data flow aspect of LUSTRE makes it very close to usual description tools in these domains (block-diagrams, networks of operators, dynamical sample-systems, etc.), and its synchronous interpretation makes it well suited for handling time in programs. Moreover, this synchronous interpretation allows it to be compiled into an efficient sequential program. The LUSTRE formalism is very similar to temporal logics. This allows the language to be used for both writing programs and expressing program properties, which results in an original program verification methodology.>

LUSTRE is a synchronous data-flow language for programming systems which interact with their environments in real-time. After an informal presentation of the language, we describe its semantics by means of structural inference rules. Moreover, we show how to use this semantics in order to generate efficient sequential code, namely, a finite state automaton which represents the control of the program. Formal rules for program transformation are also presented.