Abstract
This paper presents a proposal for the definition of a step in the execution of a statechart. The proposed semantics maintains the synchrony hypothesis, by which the system is infinitely faster than its environment, and can always finish computing its response before the next stimulus arrives. However, it corrects some inconsistencies present in previous definitions, by requiring global consistency of the step.
A preliminary version of this paper appeared in [10]
Research supported in part by the European Community ESPRIT project 937 (DESCARTES) and Basic Research Action Project 3096 (SPEC). This paper has been written while the author was visiting INRIA-IRISA, Rennes, France, whose hospitality is most gratefully acknowledged.
Research done as part of a M.Sc. thesis at the Weizmann Institute.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
G. Berry and G. Gonthier. The Synchronous Programming Language Esterel, Design, Semantics, Implementation. Technical Report, Technical Report 327, INRIA, 1988. to Appear in Science of Computer Programming.
P. Caspi, N. Halbwachs, D. Pilaud, and J. Plaice. Lustre, a declarative language for programming synchronous systems. In Proc. 14th ACM Symp. Princ. of Prog. Lang., pages 178–188, 1987.
D. Harel. Statecharts: A visual formalism for complex systems. Sci. Comp. Prog., 8:231–274, 1987.
D. Harel, H. Lachover, A. Naamad, A. Pnueli, M. Politi, R. Sherman, A. Shtull-Trauring, and M. Trakhtenbrot. Statemate: a working environment for the development of complex reactive systems. IEEE Trans. Software Engin., 16:403–414, 1990.
D. Harel, A. Pnueli, J. Schmidt, and R. Sherman. On the formal semantics of statecharts. In Proc. First IEEE Symp. Logic in Comp. Sci., pages 54–64, 1986.
C. Huizing. Semantics of reactive systems: comparison and full abstraction. PhD thesis, Technical University Eindhoven, 1991.
C. Huizing and R. Gerth. On the Semantics of Reactive Systems. Technical Report, Eindhoven University of Technology, 1988.
C. Huizing, R. Gerth, and W. de Roever. Modeling statecharts behavior in a fully abstract way. In Proc. 13th CAAP, pages 271–294, Lecture Notes in Comp. Sci. 299, Springer-Verlag, 1988.
F. Maraninchi. Argonaute: graphical description, semantics and verification of reactive systems by using a process algebra. In J. Sifakis, editor, Automatic Verification Methods for Finite State Systems, Lecture Notes in Comp. Sci. 407, Springer-Verlag, 1989.
A. Pnueli and M. Shalev. What is in a step? In J. Klop, J. Meijer, and J. Rutten, editors, J.W. De Bakker, Liber Amicorum, pages 373–400, CWI, Amsterdam, 1989.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1991 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Pnueli, A., Shalev, M. (1991). What is in a step: On the semantics of statecharts. In: Ito, T., Meyer, A.R. (eds) Theoretical Aspects of Computer Software. TACS 1991. Lecture Notes in Computer Science, vol 526. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-54415-1_49
Download citation
DOI: https://doi.org/10.1007/3-540-54415-1_49
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-54415-9
Online ISBN: 978-3-540-47617-7
eBook Packages: Springer Book Archive