Skip to main content
main-content

Über dieses Buch

This book will attempt to give a first synthesis of recent works con­ cerning reactive system design. The term "reactive system" has been introduced in order to at'oid the ambiguities often associated with by the term "real-time system," which, although best known and more sugges­ tive, has been given so many different meanings that it is almost in­ evitably misunderstood. Industrial process control systems, transporta­ tion control and supervision systems, signal-processing systems, are ex­ amples of the systems we have in mind. Although these systems are more and more computerized, it is sur­ prising to notice that the problem of time in computer science has been studied only recently by "pure" computer scientists. Until the early 1980s, time problems were regarded as the concern of performance evalu­ ation, or of some (unjustly scorned) "industrial computer engineering," or, at best, of operating systems. A second surprising fact, in contrast, is the growth of research con­ cerning timed systems during the last decade. The handling of time has suddenly become a fundamental goal for most models of concurrency. In particular, Robin Alilner 's pioneering works about synchronous process algebras gave rise to a school of thought adopting the following abstract point of view: As soon as one admits that a system can instantaneously react to events, i. e.

Inhaltsverzeichnis

Frontmatter

Introduction

Chapter 1. Introduction

Abstract
Reactive systems are computer systems that continuously react to their environment at a speed determined by this environment. This class of systems has been introduced [HP85, Ber89] in order to distinguish these systems, on the one hand, from transformational systems — i.e., classical systems, whose inputs are available at the beginning of the execution and which deliver their outputs when terminating — and, on the other hand, from interactive systems, which continuously interact with their environment, but at their own rate (e.g., operating systems). Most industrial “real-time” systems are reactive — control, supervision and signal-processing systems — but other examples concern communication protocols or man-machine interfaces.
Nicolas Halbwachs

Four Synchronous Languages

Frontmatter

Chapter 2. The imperative language Esterel

Abstract
Among the languages we will present, Esterel is the oldest, since its design started in the early 1980s. It was developed in Gerard Berry’s group and is a common project of INRIA and ENSMP in Sophia-Antipolis.
Nicolas Halbwachs

Chapter 3. Graphic formalisms: the language Argos

Abstract
This chapter is devoted to graphical formalisms based on parallel and hierarchic automata. The best known of such formalisms is probably Statecharts [Har87], which have been defined by D. Harel and A. Pnueli. However, we prefer to describe another formalism, apparently very close to Statecharts: the language Argos [Mar89, Mar90], under development at IMAG (Grenoble). This choice is motivated by the following reasons:
  • The Statecharts semantics seems to still be under discussion [HPSS86, HGd88]. On the other hand, the given semantics is not completely synchronous, since parallel composition may give rise to nondeterministic behaviors.
  • Argos solves some problems existing in Statecharts, in particular those concerning modularity and causality loops. It is a simpler language, whose semantics is completely formalized and thoroughly compatible with the synchronous point of view adopted in Esterel.
Nicolas Halbwachs

Chapter 4. Declarative languages: Lustre and Signal

Abstract
Reactive systems belong to a field in which many users come from control science or electronics rather than from computer science. It is therefore appealing to provide these users with description tools that are similar to the traditional tools used in control theory: these traditional tools often consist, at a higher level, of equational formalisms (differential or finite-difference equations, Boolean equations, etc...), and at a lower level, of various graphic formalisms to describe operator networks (block diagrams, analog schémas, switch or gate diagrams, etc...). All these formalisms belong to the “data-flow” model, which is well known in computer science [Kah74, Gra82]. In this model, a system is a network of interconnected operators, running in parallel and activated by input arrivals (cf. Figure 4.1). This model was initially proposed for general programming. However, it has not enjoyed much success in this context, on the one hand because it goes against uses that are firmly rooted in users’mind, and on the other hand because no reasonably efficient implementations have been proposed for data-flow languages.
Nicolas Halbwachs

Compilation

Frontmatter

Chapter 5. Static verifications

Abstract
As seen in §2.5, an Esterel program can raise some temporal paradoxes, which involve either the absence of any behavior or a non-deterministic behavior. This phenomenon, which appears in all really synchronous languages, comes from the fact that a program reaction, while considered instantaneous, is made up of a sequence of elementary actions (sometimes called “microsteps” [HPSS86]) that are performed in fixed order 1: the first statement of a sequence is performed “before” the second one, a “present S do <stat>” statement checks the presence of S “before” any signal emission involved by “<stat>,” and so forth.
Nicolas Halbwachs

Chapter 6. Sequential code generation

Abstract
The compiling method that synthesizes the sequential code control struc-ture as a finite automaton was first introduced in the Esterel compiler. This method was applied later on to Lustre and Argos. Our presen-tation basically follows [BCG87].
Nicolas Halbwachs

Chapter 7. Distributed code generation

Abstract
Reactive systems are often implemented on distributed architectures, for several reasons:
  • the code distribution is imposed by the physical architecture (sensor and actuator localization, protocols, etc);
  • the code is implemented concurrently to improve its performances; and
  • the code distribution is performed to achieve fault-tolerance (redundancy, degraded behavior, etc).
Nicolas Halbwachs

Chapter 8. Circuit generation from synchronous programs

Abstract
As noted in the first chapter, the problem of time constraints in synchronous programming reduces to the property that the maximum reaction time of a program is shorter than the minimum delay separating two successive external events. Minimizing this reaction time is therefore a basic goal in compiling a synchronous program. The compilation into extended automata is a software approach to that goal. Another, more radical approach to obtain very short reaction times consists in implementing a synchronous program on a circuit. Synchronous languages are good candidates for silicon compiling, since most circuits can be considered as synchronous machines from some level of abstraction. Some synchronous languages [BC85, BL85] have been designed to describe hardware.
Nicolas Halbwachs

Program Verification

Frontmatter

Chapter 9. Lustre program verification: the tool Lesar

Abstract
As noted in the introduction, reactive systems often concern critical applications, and thus program verification is a key issue. However, many practitioners in the field are skeptical about the use of formal verification methods, and convincing arguments need to be provided in order to support the claim that such methods are indeed of practical interest. This is the object of the following discussion.
Nicolas Halbwachs

Chapter 10. Using Auto for Esterel program verification

Abstract
Another approach to program verification, also based on automata, has been applied to Esterel. It starts from the statement that program specification is a difïicult task, almost as error-prone as program writing. The basic idea, therefore, is not to write a specification, but rather simply to observe the behavior of the generated automaton. Of course, a complete automaton cannot be manually analyzed; even a small automaton, of about ten states, can be quite complex. The proposed approach offers reduction methods, providing partial views on the automaton, on which one can easily detect anomalies and check properties. The verification tooi Auto [Ver86, BRdSV90, RdS90] has been developed at INRIA, in order to perform such reductions. The graphic editor Autograph [RS89, Roy90] allows (reduced) automata to be visualized.
Nicolas Halbwachs

Chapter 11. Conclusion

Abstract
The Esterel, Lustre, and Signal compilers are now commercial products (see the industrial contacts given in the Foreword). The industrialisation of Argos will start soon
Nicolas Halbwachs

Backmatter

Weitere Informationen