A deterministic logical semantics for pure Esterel

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

A deterministic logical semantics for pure Esterel

Full text

Pdf (527 KB)

Source

ACM Transactions on Programming Languages and Systems (TOPLAS) archive
Volume 29 , Issue 2 (April 2007) table of contents

Article No. 8

Year of Publication: 2007

ISSN:0164-0925

Author

Olivier Tardieu

Columbia University, New York, NY

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 6, Downloads (12 Months): 62, Citation Count: 0

Additional Information:

abstract references index terms collaborative colleagues

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/1216374.1216376 What is a DOI?

ABSTRACT

Esterel is a synchronous design language for the specification of reactive systems. There exist two main semantics for Esterel. On the one hand, the logical behavioral semantics provides a simple and compact formalization of the behavior of programs using SOS rules. But it does not ensure deterministic deadlock-free executions, as it may define zero, one, or many possible behaviors for a given program and input sequence. Since nondeterministic programs have to be rejected by compilers, this means that it defines behaviors for incorrect programs, which is awkward. On the other hand, the constructive semantics is deterministic (amongst other properties) but at the expense of a much more complex formalism. In this work, we build and thoroughly analyze a new deterministic semantics for Esterel that retains the simplicity of the logical behavioral semantics from which it derives. It defines, at most, one behavior per program and input sequence. We further extend this semantics with the ability to deal with errors so that incorrect programs are no longer (negatively) characterized by a lack of behavior, but (positively) by the existence of an incorrect behavior. In our view, this new semantics, with or without explicit errors, provides a better framework for formal and automated reasoning about Esterel programs.

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	Benveniste, A. and Berry, G. 1991. The synchronous approach to reactive real-time systems. Proc. IEEE 79, 9, 1270--1282.
	2	Benveniste, A., Caspi, P., Edwards, S., Halbwachs, N., Le Guernic, P., and de Simone, R. 2003. The synchronous languages twelve years later. Proc. IEEE 91, 1, 64--83.
	3	Gérard Berry, Preemption in Concurrent Systems, Proceedings of the 13th Conference on Foundations of Software Technology and Theoretical Computer Science, p.72-93, December 15-17, 1993
	4	Berry, G. 1999. The constructive semantics of pure Esterel. http://www-sop.inria.fr/esterel.org/.
	5	Berry, G. 2000a. The Esterel language primer v5_91. http://www-sop.inria.fr/esterel.org/.
	6	Gérard Berry, The foundations of Esterel, Proof, language, and interaction: essays in honour of Robin Milner, MIT Press, Cambridge, MA, 2000
	7	Gérard Berry , Laurent Cosserat, The ESTEREL Synchronous Programming Language and its Mathematical Semantics, Seminar on Concurrency, Carnegie-Mellon University, p.389-448, July 09-11, 1984
	8	Gérard Berry , Georges Gonthier, The ESTEREL synchronous programming language: design, semantics, implementation, Science of Computer Programming, v.19 n.2, p.87-152, Nov. 1992 [doi>10.1016/0167-6423(92)90005-V]
	9	Boussinot, F. and de Simone, R. 1991. The Esterel language. Proc. IEEE 79, 1293--1304.
	10	Stephen A. Edwards, Languages for Digital Embedded Systems, Kluwer Academic Publishers, Norwell, MA, 2000
	11	Edwards, S. A., Kapadia, V., and Halas, M. 2004. Compiling Esterel into static discrete-event code. In Proceedings of the Synchronous Languages, Applications, and Programming Workshop (Barcelona, Spain). Electronic Notes in Theoretical Computer Science. Elsevier.
	12	Gonthier, G. 1988. Sémantique et modèles d'exécution des langages réactifs synchrones: Application à Esterel. Ph.D. thesis, Université d'Orsay.
	13	Jan Friso Groote, Transition system specifications with negative premises, Theoretical Computer Science, v.118 n.2, p.263-299, Sept. 27, 1993 [doi>10.1016/0304-3975(93)90111-6]
	14	Nicolas Halbwachs, Synchronous Programming of Reactive Systems, Kluwer Academic Publishers, Norwell, MA, 1992
	15	Halbwachs, N., Caspi, P., Raymond, P., and Pilaud, D. 1991. The synchronous dataflow programming language Lustre. Proc. IEEE 79, 9, 1305--1320.
	16	INRIA, ENSMP, and ARMINES. 2000. The Esterel v5_92 compiler. http://www-sop.inria.fr/esterel.org/.
	17	Le Guernic, P., Le Borgne, M., Gauthier, T., and Lemaire, C. 1991. Programming real time applications with Signal. Proc. IEEE 79, 9, 1321--1336.
	18	Sharad Malik, Analysis of cyclic combinational circuits, Proceedings of the 1993 IEEE/ACM international conference on Computer-aided design, p.618-625, November 07-11, 1993, Santa Clara, California, United States
	19	R. Milner, Communication and Concurrency, Prentice-Hall, Inc., Upper Saddle River, NJ, 1989
	20	Plotkin, G. 1981. A structural approach to operational semantics. Rep. DAIMI FN-19, Aarhus University, Denmark.
	21	Potop-Butucaru, D. 2002. Optimizations for faster execution of Esterel programs. Ph.D. thesis, Ecole des Mines de Paris.
	22	Tardieu, O. 2004. Loops in Esterel: From operational semantics to formally specified compilers. Ph.D. thesis, Ecole des Mines de Paris. http://olivier.tardieu.free.fr/papers/these.pdf.
	23	Tardieu, O. and de Simone, R. 2003. Instantaneous termination in pure Esterel. In Proceedings of the 10th International Static Analysis Symposium (San Diego, CA). Lecture Notes in Computer Science, vol. 2694. Springer Verlag. 91--108.