Languages for reactive specifications: Synchrony vs asynchrony
The role of nondeterminism in the specification of the behaviour and realization of programs: A clear distinction between local and global nondeterminism enables us to distinguish between the implementational nondeterminism and environmental or input nondeterminism. The results in this direction would enable one to achieve observable determinism where the implementational choices can be hidden and thus, analyze the program behaviour with reference to the real environmental nondeterminism in the specification. This in turn leads to a proper refinement of specifications and programs and also aids in deriving distributed implementations of finite state transition systems which are not necessarily deterministic.
The implementability of asynchronous languages through synchronous languages: The synchrony hypothesis of the synchronous languages makes it closer to a perfect machine. Thus, the implementability of asynchronous languages in synchronous languages not only provides a realistic implementation but also provides other higher level abstractions (such as multi-process interactions) for reactive specifications using features such as broadcast, interrupts, exception handling mechanisms etc.
KeywordsInput Signal Execution Sequence Input Event Module Link Kernel Statement
Unable to display preview. Download preview PDF.
- [Be 92]G. Berry (1992), A hardware implementation of pure Esterel, SADHANA: Special Issue on Real Time edited by RK Shyamasundar, Academy Proceedings in Engineering Sciences, Indian Academy of Sciences, 17 (1):95–139, 1992.Google Scholar
- [BeGo 92]G. Berry and G. Gonthier (1988), The Esterel synchronous programming language: Design, semantics, Implementation, Rapport de Recherche 842, INRIA 1988, Science of Computer Programming, Vol. 19, No.2, Nov. 92, pp. 87–152.Google Scholar
- [BeRaSh 93]G. Berry, S. Ramesh and R.K. Shyamasundar (1993), Communicating Reactive Processes, 20th Acm Symposium on Principles of Programming Languages, South Carolina, Jan. 1993.Google Scholar
- [BRSV90]G. Boudol, V. Roy, R. de Simone, and D. Vergamini, Process Calculi, from theory to practice: Verification tools, In Automatic Verification Methods for Finite State Systems, LNCS 407, Springer-Verlag, 1990, pp. 1–10.Google Scholar
- [CG 92]P. Caspi and A. Girault (1992), An algorithm for distributing finite transition systems on a shared/distributed memory system, IMAG Report, L-17, Grenoble, France.Google Scholar
- [Hoa 78]C.A.R. Hoare (1978), Communicating Sequential Processes, CACM, August 1978.Google Scholar
- [MaPn 92]Z. Manna and A. Pnueli, Models for Reactivity, TR, Stanford, 1992 (an earlier version presented at the 25th Anniversary of INRIA).Google Scholar
- [OlHo 83]E.-R. Olderog and C.A.R. Hoare (1983), Specification-oriented semantics for communicating processes, 10th ICALP, Barcelona, LNCS, 154, Springer Verlag, pp. 561–572.Google Scholar