Abstract
Statecharts and Esterel are two formalisms that have been widely used in the development of reactive systems. Statecharts are a powerful graphical formalism for system specification. esterel is a rich synchronous programming language with supporting tools for formal verification. In this paper, we propose a translation of Statecharts to esterel and discuss such an implementation. A characteristic feature of the translation is that deterministic Statechart programs can be effectively translated to esterel and hence, the tools of verification of esterel can be used for verifying Statechart programs as well. The translation serves as a diagnostic tool for checking nondeterminism. The translation is syntax-directed and is applicable for synchronous and asynchronous (referred to as the superstep model) models. In the paper, we shall describe the main algorithms for translation and implementation and illustrate the same with examples. We have built a prototype system based on the translation. It has the advantages of the visual power usually liked by engineers reflected in Statecharts and of a language that has a good semantic and implementation basis such as esterel that can be gainfully exploited in the design of reliable reactive systems.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
AndrÉ, C. SyncCharts: A Visual Representation of Reactive Behaviors. Tech. Rep. RR 95-52, I3S, Sophia-Antipolis, France, 1995.
AndrÉ, C. Representation and Analysis of Reactive Behaviors: A Synchronous Approach. Tech. Rep. 96-28, Université de Nice, Sophia-Antipolis, France, 1996.
Beauvais, J.-R. et al. A Translation of Statecharts to Signal/DC+. Tech. rep., IRISA, 1997.
Berry, G. A Quick Guide to Esterel Version 5.10, release 1.0. Tech. rep., Ecoledes Mines and INRIA, February 1997.
Berry, G., Halbwachs, N., and Maraninchi, F. Unpublished note on Esterel and Argos. 1995.
Harel, D. Statecharts: A Visual Formalism for Complex Systems. Science of Computer Programming 8 (1987), 231–274.
Harel, D., and Naamad, A. The STATEMATE Semantics of StateCharts. ACM Transactions on Software Engineering and Methodology,4 (October 1996).
LeGuernic, P. et al. Programming Real-time applications with Signal. Proceedings of the IEEE 79, 9 (September 1991), 1321–1336.
Mikk, E., Lakhnech, Y., and Siegel, M. Hierarchical automata as model for statecharts. In LNCS (Dec. 1997), 1345, pp. 181–197.
Mikk, E., Lakhnech, Y., Siegel, M., and Holzmann, G. Implementing Statecharts in Promela/SPIN. In Proc. of the 2nd IEEE Workshop on Industrial-Strength Formal Specification Techniques (1999), IEEE Computer Society.
Puchol, C. et al. A Formal Approach to Reactive Systems Software: A Telecommunications Application in Esterel. In Proc. of the Workshop on Industrial Strength Formal Specification Techniques (April 1995).
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Seshia, S.A., Shyamasundar, R.K., Bhattacharjee, A.K., Dhodapkar, S.D. (1999). A translation of statecharts to esterel. In: Wing, J.M., Woodcock, J., Davies, J. (eds) FM’99 — Formal Methods. FM 1999. Lecture Notes in Computer Science, vol 1709. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48118-4_3
Download citation
DOI: https://doi.org/10.1007/3-540-48118-4_3
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66588-5
Online ISBN: 978-3-540-48118-8
eBook Packages: Springer Book Archive