Extending Esterel by Asynchronous Concurrency1
Michael Baldamus · 1999
Synchronous languages like Esterel and PURR have been introduced to support the development of concurrent reactive systems. These languages have an easily understood semantics that lends itself well for efficient implementations and also for a formal verification of the designs. We show how to enrich Esterel or PURR by two important features, namely asynchronous concurrency and nondeterminism. These features are important for (1) describing asynchronous systems and (2) for using PURR as a modeling language. We introduce the new constructs on the basis of a compilation oriented transition semantics of a core portion of PURR. 1 Introduction 1.1 Synchronous Programming Many systems maintain an ongoing interaction with their environment and are forced to do this at the speed determined by the environment. Harel [15] therefore distinguishes transformational, interactive and reactive systems: Transformational systems read their inputs once at starting time, compute the outputs, and termin...