Synchronous approach


This section presents a brief description of the main syncronous languages as well as pointers to documentation, online information and people. In general the description was taken from the home web page.

Esterel

Esterel is a programming language dedicated to control-dominated reactive systems, such as control circuits, embedded systems, human-machine interface, or communication protocols. It is also a compiler which translates Esterel programs into finite-state machines. It belongs to the family of synchronous languages, which also includes Lustre, Signal, and SyncCharts. Esterel has been developed since 1983 at CMA (Applied Mathematics Center, Ecole des Mines de Paris), and INRIA in Sophia-Antipolis.

The language has a rigorous mathematical semantics. The toolset includes a compiler to software or hardware, a graphical simulator, a verification system, and optimizers.�In particular the Esterel v5 compiler can be used to generate a software or hardware implementation of a reactive program. It can generate C-code to be embedded as a reactive kernel in a larger program that handles the interface and data manipulations. It can also generate hardware in the form of netlists of gates, which can then be embedded in a larger system. Extensive optimization is available. We provide a graphical symbolic debugger for Esterel. We also provide support for explicit or BDD-based verification tools that perform either bisimulation reduction or safety property checking.

Esterel is now experimentally used by several companies and taught in several universities. Esterel and SyncCharts are commercialized by the Simulog company. They are used by companies such as Dassault Aviation for avionics, Thomson for telecommunication, Texas Instruments for DSP circuits development, etc. Cadence and University of California Berkeley are using Esterel in their Polis hardware / software codesign environment. CMA and INRIA also cooperate with Synopsys and Intel on Esterel.

HOME page      http://www.esterel.org/, http://www-sop.inria.fr/meije/esterel/esterel-eng.html.

Information      ps, ps2.

People                   

                             Gerard BERRY

Lustre

LUSTRE is a synchronous declarative language for programming reactive systems. It is declarative because a description is a set of equations that must be always verified by the program variables. This approach was inspired by formalisms familiar to control engineers, like systems of differential equations or synchronous operator networks (block diagrams). A program variable in LUSTRE is considered to be a function of multiform time: it has an associated clock which defines the sequence of instants where the variable takes its values. LUSTRE is the kernel language of the SCADE (formerly SAO+/SAGA) industrial environment developped by Telelogic.

The design of LUSTRE started in 1984. Since then, the following topics have been studied:

  • Compilation: The compiler Lustre-V4 produces sequential code by synthesizing the control structure of the object code in the form of an extended finite automaton. Several levels of details of this control structure (ranging from a single loop structure to a very detailed automaton) can be chosen.

  • Code Distribution: A tool for the distribution of sequential code produced by the LUSTRE compiler according to directives of the programmer, has been developed in cooperation with Merlin Gerin. The tool will be integrated in an execution environment for distributed programs. Finally, a partial order semantics for LUSTRE is under study to provide the user of the tool a better insight about the meaning of distributed synchronous systems based on a relaxation of the synchrony assumption.
  • Verification: It has been shown that LUSTRE can be considered as a temporal logic allowing the expression of safety properties. This allows the description of both the program and the specifications in the same language. The verification tool LESAR is a model-checker for verifying Lustre programs specified in that way. It considers a finite model of the program, similar to the automaton produced by the compiler. So it is only able to verify properties depending on the control (i.e., the Boolean part) of the program. Some extensions towards numerical properties are also studied.
  • Automatic Testing: Given the same kind of specification than for verification, the tool LURETTE is able to generate an arbitrary number of arbitrarily long input sequences to a program, satisfying specified assumptions, while testing that the specifyed properties are satisfied.

HOME page      http://www-verimag.imag.fr/SYNCHRONE/lustre-english.html

Information      ps.

People                                      

                              Paul CASPI     Pascal RAYMOND     Nicolas HALBWACH

 

Signal

Signal is a data-flow language (although not in the exact sense of Kahn's process networks). So the objects are flows, i.e., infinite sequences of values. They are called signals. Each signal has a clock which is the sequence of instants where the signal has a value. At any instant of its clock, a signal can be present and have a defined value, or be absent and have the value bot.

Signal is a declarative language. So signals are defined by equations that specify their properties. The order of the equations is irrelevant.

Signal is a synchronous language. So all the events (i.e., the values of all the signals) are totally ordered.

Signal is a relational language. So the way a signal is used can have consequences on the signal itself (actually on its clock).

Unlike in Lustre, there is no global clock. Instead, the notion of clock is local. If two signals have the same clock, then whenever one has a value, the other one must also have one, and when one has no value (i.e., a bot), the other one must also have a bot.

Information      html1,   french web pages html2html3,  html4, html5, ps.

Lucid Synchrone

Lucid Synchrone is a synchronous stream language dedicated to the implementation of reactive systems. It combines features of Lustre and ML languages. The name Lucid Synchrone is built from Lucid a data-flow language managing streams and from the French word ''synchrone'' (for ''synchronous''). The main features of the language are the following:

  • It is a strongly typed, higher-order functional language managing infinite sequences or streams as primitive values. These streams are used for representing input and output signals of reactive systems. These streams are combined with a set of synchronous data-flow operators in the spirit of Lustre.

  • Several static analysis (e.g, type inference, clock calculus, causality, initialization check) are provided. In particular, the language is founded on the notion of clocks as a way to specify different execution rates in a program. The program must in turn verify some clocking rules, insuring reactivity (i.e, compilation into a finite transition system).

  • The language is built above Ocaml: programs are written in a sub-set of Ocaml syntax; combinatorial values are imported from Ocaml; programs are compiled into Ocaml code.

  • A simple module system is provided for importing values from the host language Ocaml or from other synchronous modules.

HOME page      http://www-spi.lip6.fr/softs/lucid-synchrone.html/

Information       html, ps, ps.gz, pdf.

People                  Marc POUZET, Grégoire HAMON

StateCharts

David Harel introduced statecharts to extend finite state machine for complex behavior and to describe a visual formalism. Objectcharts were then presented by Derek Coleman et.al. as an extension to describe how to use statecharts in object-oriented environment to describe the lifecycle of an object. Statecharts were used by Bran Selic as an implementation mechanism for Recursive Control. Alternatively, we perceive that statecharts are frequently used as a behavior description technique and using an object-oriented design of statechart provides flexibility at the design level and facilitates the design maintainability.

Statechart is a specification language which enables you to construct a model and further check it. Some case tools allow you to genertae code from your specification. Using the generated code might not be useful because it is usually bulky and not comprenhensible for the designer. Thus you want to translate the specification into design that allow you to have a higher level of maintenance and to embed this design into your overall application design.

StateCharts adds four elements to finite state machine: depth, orthogonality, broadcasting and history, thus

                        Statecharts = State Machine + Depth + Orthogonality + Broadcasting + History

Information       html, pdf.

People                   

                             David HAREL

SyncChart

SyncCharts is a graphical formalism dedicated to reactive System Modeling. � Many features are inherited from StateCharts (D. Harel) and Argos (F. Maraninchi). SyncCharts allows the specification of reactive behavior, as well as the synchronous programming of applications. SyncCharts adheres to the "Synchronous Paradigm". It supports

  • Hierarchy: nested macrostates

  • Concurrency: orthogonal constellations (kinds of state graphs)
  • Communication: instantaneous broadcasting of signals
  • Preemption: abortion and suspension

Any syncChart can be automatically translated into an Esterel program (esterel v5), so that, the user can take advantage of the software environment developed for synchronous programming.

HOME page      http://www-sop.inria.fr/meije/esterel/syncCharts/

Information       ps.gz, pdf

People                   

                           Charles ANDRE

Argos

Argos is an imperative synchronous language developped at the VERIMAG laboratory. Argonaute is the programming environment based upon Argos, which provides a compiler and several connections to verification tools.

Argos is first inspired by D. Harel statecharts. It offers both a graphical and a textual syntaxes. The main differences with statecharts are the use of a truly hierarchical composition operator which does away with inter-level transitions used in statecharts, and the application of a strict synchrony assumption. Argos is the basis of the programming environment Argonaute which provides a compiler and allows a lot of connections to verification tools. Developments on Argos are carried out in the following directions:

  • Compilation: Several efficient compilation techniques have been studied. The current version of the compiler produces labeled transition systems in different formats that can be used for code generation, simulation or verification. A new version is under development: Argos programs are now compiled into sets of structured equations. This symbolic compiling technique is much more efficient than the explicit generation of labeled transition systems.

  • Connections to tool : The compiler may produces several output formats.

    • The common oc format for code generation and simulation
    • An automaton format that can be used for verification with Aldebaran
    • Timed automata that can be verified by using Kronos. This model is generated from Timed ARGOS, an extension of the language by adding a timeout construct.
  • Multilanguage Programming: The aim is to study and implement two mixed languages: Argos + Esterel and Argos + Lustre. Mixing Lustre and Argos would allow a mixed imperative/declarative style for programming reactive systems. Mixing Argos and Esterel can be viewed as a way of introducing a automaton-like control structure in Esterel.

HOME page      http://www-verimag.imag.fr//SYNCHRONE/argonaute-english.html

Information       ps.gz.

People                   

                         Florence MARANINCHI

SL

The SL language is a synchronous language in which reactions are instantaneous. Its syntax is close to esterel, but in SL hypotheses about signal presence/absence are disallowed. One decides that a signal is absent during an instant only at the end of this instant, and so reaction to the absence is delayed to the next instant.

Sources of causal circularities (the so-called causality cycles) are avoided, and the main features of the synchronous approach still remain: the expressive simplicity and power of parallelism, the ease of specification and debugging for deterministic programs, and the power and modularity of broadcast and instantaneous dialogs. However, "strong" preemptions are not possible in SL, and only "weak" ones can be used.

Forbidding immediate reactions to signal absences simplifies the implementation to a large extent (the existing implementation is less than 1000 Reactive-C lines). In addition to directly execute programs, the implementation can also be used to produce automata by symbolic evaluation.

Information       html1   html2/ps.gz.

People                   

                          Robert DeSimone

ECL

ECL is a language for embedded system specification. ECL stands for Esterel-C Language; the term is used both for the language and its compiler. The language is ANSI-C with added constructs inspired by Esterel for specifying reactivity (signal communication, pre-emption, and concurrency). It conveniently supports specification of mixed control/data modules. The compilation is performed by splitting the source code into reactive Esterel code and data-dominated C code. The reactive portion can be robustly optimized and synthesized to either hardware or software, while the C residual code must be implemented in software as is.

ECL was developed by Luciano Lavagno, Roberto Passerone, and Ellen Sentovich.

HOME page      http://ecl.sourceforge.net/    http://www.sourceforge.net/projects/ecl

Information      ps.

People                                        

                         Luciano LAVAGNO Ellen M. SENTOVICH  Roberto PASSERONE

Reactive-C

The project started in 1988 with the idea of allowing a programming style close to C, in which program behaviors are defined in terms of reactions to activations. Reactive-C (RC) programs can react differently when activated for the first time, for the second time, and so on. Thus a new dimension appears for the programmer: the logical time induced by the sequence of activations. Each pair of activation/reaction is called an instant, and the reactive approach is thus an approach in which one reasons by reference to instants.

The present RC compiler is the rcc version 3 compiler. It works as a pre-processor of C, and is about 2500 lines of Ansi-C. It runs on several Unix platforms and also on DOS/PC. It is free software. Actually, Reactive-C appeared rapidly as being a kind of reactive assembly language that could be used to implement higher level formalisms based on the notion of an instant. Several formalisms have been implemented using RC: Nets of Reactive Processes, SL.

HOME page      http://www-sop.inria.fr/meije/rc/general-presentation.html

Information       ps1, ps2.

People                  Fréderic BOUSSINOT

SugarCubes/Junior

SugarCubes is a set of Java classes for implementing:

  • event based systems, especially those where events are instantly broadcast throughout the system. Communicating in this framework is like in radio transmissions, where emitters send information that is instantaneously received by all receivers.

  • concurrent systems, in particular thread-less ones. Here, parallelism is a logical programming construct to implement activities which are supposed to proceed concurrently, and not one after the other.
  • reactive systems, which continuously react to activations.

SugarCubes is used to implement Reactive Scripts and Icobj Programming on top of the Java language.

Junior (Jr, J for Java and r for reactive) is a kernel for reactive programming in Java. It is closely related to SugarCubes, and can be seen as kernel of it. Junior is developped jointly by EMP-CMA, Inria, and France Telecom/ R&D. Junior is available for programming through an API called Jr. Junior has a formal semantics (expressed with rewriting rules in the format of strutural operational semantics) and several implementations.

A first implementation, called REWRITE, is the direct implementation of the semantics. It is thus the reference implementation. In REWRITE, the program syntax tree is analysed and rebuilt at each activation. A second implementation, called REPLACE, avoids program rebuildings and is thus much more efficient than REWRITE. The technics used by REPLACE is actually very close to the one of SugarCubes. A third implementation, called SIMPLE, avoids the traversal of the whole program at each activation. Instructions waiting for an event are posted in a file associated to the event. Thus, posted instruction are no more processed until the firing event becomes generated. This leads to the possibility of using huge numbers of events while preserving good response time.

Junior is presently used in several contexts: implementation of Rhum, a language for reactive programming developped at France Telecom R&D; implementation of icobj programming and of the REJO/ROS reactive agents system developped at CMA/Inria. Junior is also used in the Ping IST Project.

HOME page      http://www-sop.inria.fr/mimosa/rp/

Information       pdf (Jr), pdf (SC).

People                  Jean-Ferdinand SUSINI