Dagstuhl Seminar 9448
Synchronous Languages
( Nov 28 – Dec 02, 1994 )
Permalink
Organizers
- A. Pnueli
- A. Poigné
- G. Berry
- W.P. de Roever
Contact
Synchronous Languages such as LUSTRE, ESTEREL and SIGNAL were conceived in the first half of the eighties by mainly French researchers. Independently, Harel & Pnueli worked on an almost synchronous language, STATECHARTS, as part of the STATEMATE system for the specification of real-time embedded systems (mainly concerning software for the aircraft industry). Independently, Ward & Mellor published in 1985 their 3-volume approach "Structured Development of Real-time Systems", containing important synchronous elements.
The second half of the 1980's was used to:
- Obtain efficient implementations for these languages and to convince users that the resulting systems make sense for specifying real-time embedded systems.
- To resolve semantic problems which are a consequence of the synchronous approach (which states in essence that a system responds in zero time to environmental requests - Berry's "synchrony hypothesis"). On the latter foundational research by Berry & co-workers on the semantics of ESTEREL, Halbwachs & co-workers on LUSTRE, Le Guernic & Benveniste on SIGNAL, Pnueli, Huizing et al on the semantics of STATECHARTS, stands out.
At the beginning of the nineties the picture changes. Rather than investigating what's there, it is investigated and formulated what should be there, i.e., improvements and alternatives are suggested. E.g., Florence Maraninchi (at Grenoble) proposes a semantics for a new version of STATECHARTS called ARGOS (and implements this) which yields a truly modular notion of refinement of modes (or states) and does away with a number of ``paradoxes" due to the synchronous nature of such languages (which require complicated semantical notions for their solution). However, on the other hand the following becomes clear:
- There is no way in these languages to specify that an implementation should satisfy real-time constraints (e.g. in STATECHARTS it is impossible to express that an implementation of a state should run in less than 10 nano seconds).
- Traditional data structures are not integrated, and neither is their refinement, or any notion of refinement, suitably described for those languages.
- There is no notion of object-orientation for such languages. Solutions are proposed (by Rumbaugh et al) and projects applied for to find these (Pnueli & Harel).
Also it becomes clear that ESTEREL/LUSTRE on the one hand, and STATEMATE on the other, serve different purposes. E/L aims at specifying the minimal timed automaton to control a component of a real-time embedded system and become therefore equipped/connected with silicon compilers, while STATEMATE aims at specifying an overall distributed system with many components which are geometrically spread (through their notion of Activity charts). Rather than competing, as done in the period 1985-1990, their complementary roles get accepted and their general relevance to industrial purposes becomes known in wider circles than only aircraft manufactures (DST/Kiel, Siemens/Müunchen, Ahlstom-Alcatel/Paris).
Joseph Sifakis gets allotted a complete laboratory - VERIMAG - (about 15 engineers in addition to his own equipe) to build a future specification system for the AIRBUS software in which ARGOS/STATEMATE at the high level of specification where truly distributed processes count are combined with LUSTRE/ESTEREL on a lower level of specification where single chips are specified. Model checkers are combined with the structured automata generated by these systems, e.g. by Werner Damm and co-workers at Oldenburg. Siemens starts collaborating with the SIGNAL group (Benveniste). (Siemens builds the fastest BDD model checker at present and may want to couple it with such systems).
The (mixed) description of combinations of such formalisms becomes a recognized topic of research (e.g. by Poigné & co-workers who have started to combine all the synchronous languages in a modular way). Proof systems and (decidable) assertion languages for the underlying formalisms are developed (de Roever et al., Damm et al.), versions are formulated to truly specify real-time (Huizing, Pnueli).
In Germany independent groups working as these issues meet for the first time jointly (GI Fachgespräch, June 16/17th, 1994, Kiel). DST/Kiel starts funding a synchronous languages based project in combination with a funding agency (Technologiestiftung Schleswig-Holstein) to obtain a tool supporting the design of safety critical systems.
It is in this context of emerging industrial and academic interest within Germany in the specification, prototyping, verification and testing capabilities of real-time embedded systems through the use of synchronous languages and their coupling with advanced tools that we have applied for a Dagstuhl seminar on this topic to bring academia and industry together in Germany and abroad in order to exchange ideas, to discuss their research and to foster collaboration.
This Dagstuhl meeting was a first effort to get together researchers concerned with the different synchronous formalisms to provide a state-of-the-art overview of the field.
Since then the industrial impact of synchronous formalisms has increased. Several industrial applications have been developed being based on the synchronous paradigm and more and more industries have spent considerable time and efforts in evaluating and applying the synchronous approach, e.g.:
- Dassault-Aviation is using extensively ESTEREL for their Rafale airplane.
- Cadence uses ESTEREL as a front-end for their POLIS experimental codesign system.
- Daimler-Benz is making rather extensive experiments with ESTEREL.
- AT&T R&D Indian Hill lab has made successful experiments with ESTEREL and has built a verification system for ESTEREL programs.
- The new generation of Airbus airplanes is programmed in LUSTRE.
- The Hong-Kong subway has been re-engineered in LUSTRE.
- Part of the French nuclear plant safety system is programmed in LUSTRE.
- DASA has developed an environment, called HOSTESS, based on the synchronous data-flow model; they are evaluating the commercial version of lustre, SAO+/LUSTRE, which is also a strong candidate to be used for the development of the software of the Airbus A3XX.
- SNECMA, one of the world's most important manufacturers of jet engines, considers using SILDEX (the professional SIGNAL environment) for next generation development of engine control systems.
- Electricité de France has carried out extensive experiments with SIGNAL.
- A. Pnueli
- A. Poigné
- G. Berry
- W.P. de Roever
Related Seminars
- Dagstuhl Seminar 9650: Synchronous Languages (1996-12-09 - 1996-12-13) (Details)
- Dagstuhl Seminar 01491: Synchronous Languages (2001-12-02 - 2001-12-07) (Details)
- Dagstuhl Seminar 04491: Synchronous Programming - SYNCHRON'04 (2004-11-28 - 2004-12-03) (Details)
- Dagstuhl Seminar 09481: SYNCHRON 2009 (2009-11-22 - 2009-11-27) (Details)
- Dagstuhl Seminar 13471: Synchronous Programming (2013-11-17 - 2013-11-22) (Details)