Clock-based Systems

In our opinion, clock-based systems (in other words: synchronous systems) are perfectly suited for a model-based design flow since they allow one to describe concurrent systems with an abstract notion of time. These languages have been developed for the design of reactive systems: A reactive system is thereby a system that continuously interacts with its environment such that the reaction of the system must be generated before a new interaction is triggered by the environment. Thus, reactive systems are hard real-time systems by nature.

The paradigm of synchronous languages is as follows: The computation of a synchronous program consists of macro steps where each macro step corresponds to an interaction with the environment, i.e., in each macro step all inputs are read, a new internal state is computed, and all outputs are provided in the same macro step. Since the execution of each macro steps is considered to require one unit of abstract time, synchronous systems running in parallel automatically synchronize after each macro step.

By construction of synchronous languages, each macro step consists of only finitely many atomic actions. For this reason, the estimation of the reaction time is much simpler than for other languages. One may either count the maximal number of micro steps in the original synchronous model or one may consider the physical execution time of each of the finitely many steps after the architecture has been selected. Fast reaction time belongs besides low energy consumption one of the most important criteria for the partitioning of the system.

Simulation greatly benefits from synchronous languages: While most concurrent languages produce nondeterminism e.g. due to process priorities or data races, synchronous programs enforce deterministic systems. Thus, simulation runs are reproducible so that so-called Heisenbugs are avoided.

Synchronous systems are also the basis of most system models used by formal verification methods including most model-checking procedures for temporal logics. It is not difficult to translate a synchronous program to a symbolic transition relation as required by these verification methods so that formal verification can be tightly integrated in the design flow. Moreover, the translation and simulation of synchronous programs themselves can be verified/certified against the operational semantics that is precisely defined for most synchronous languages.

Finally, it is possible to translate synchronous programs both to software and hardware descriptions, so that synchronous languages fulfill all requirements of a model-based design flow. The preferred input language of our design framework Averest is the programming language Quartz. This language has been derived from the Esterel language, but was extended in several ways, including a precise type systems for program expressions, delayed assignments, nondeterministic choices, analog/digital behaviors, as well as temporal logic specifications and modular design.

References

			[Halb93] N. Halbwachs Synchronous programming of reactive systems Kluwer
			[BCEH03] A. Benveniste and P. Caspi and S. Edwards and N. Halbwachs and P. Le Guernic and R. de Simone The Synchronous Languages Twelve Years Later Proceedings of the IEEE
			[BeBe91] A. Benveniste and G. Berry The synchronous approach to reactive real-time systems Proceedings of the IEEE
			[BeGu91] A. Benveniste and P. Le Guernic Synchronous programming with events and relations: the SIGNAL language and its semantics Science of Computer Programming
			[HCRP91] N. Halbwachs and P. Caspi and P. Raymond and D. Pilaud The Synchronous Dataflow Programming Language LUSTRE Proceedings of the IEEE
			[BoSi91] F. Boussinot and R. de Simone The Esterel language Proceedings of the IEEE