Abstract
Statechart Diagrams are a notation for describing behaviours in the framework of UML, the Unified Modeling Language of object-oriented systems. UML is a semi-formal language, with a precisely defined syntax and static semantics but with an only informally specified dynamic semantics. UML Statechart Diagrams differ from classical statecharts, as defined by Harel, for which formalizations and results are available in the literature. This paper sets the basis for the development of a formal semantics for UML Statechart Diagrams based on Kripke structures. This forms the first step towards model checking of UML Statechart Diagrams. We follow the approach proposed by Mikk and others: we first map Statechart Diagrams to the intermediate format of extended hierarchical automata and then we define an operational semantics for these automata. We prove a number of properties of such semantics which reflect the design choices of UML Statechart Diagrams.
The work described in this paper has been performed in the context of the ESPRIT Project n. 27439 — HIDE
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
D. Harel. Statecharts: A visual formalism for complex systems. Science of Computer Programming. Elsevier, 8 (3): 231–274, 1987.
D. Harel. The STATEMATE semantics of statecharts. ACM Transactions on Software Engineering and Methodology,5(4):293–333.
G. Holzmann. The model checker SPIN. IEEE Transactions on Software Engineering, 23 (5): 279–295, 1997.
Rational Software * Microsoft * Hewlett-Packard * Oracle * Sterling Software * MCI Systemhouse * Unisys * ICON Computing * IntelliCorp * i Logix * IBM * ObjecTime * Platinum Technology * Ptech * Taskon * Reich Technologies * Softeam. UML Semantics, version 1.1,1997.
Rational Software * Microsoft * Hewlett-Packard * Oracle * Sterling Software * MCI Systemhouse * Unisys * ICON Computing * IntelliCorp * i Logix * IBM * ObjecTime * Platinum Technology * Ptech * Taskon * Reich Technologies * Softeam. UML Notation Guide, version 1.1,1997.
D. Latella, M. Massink, and I. Majzik. A Simplified Formal Semantics for a Subset of UML Statechart Diagrams. Technical Report HIDE/T1.2/PDCC/5/v1, ESPRIT Project n. 27439 - High-Level Integrated Design Environemnt for Dependability HIDE, 1998. Available in the HIDE Project Public Repository (http://asterix. mit/).bme.hu:998
Z. Manna, S. Ness, and J. Vuillemin. Inductive methods for proving properties of programs. Communications of the ACM, 16 (8), 1973.
E. Mikk, Y. Lakhnech, and M. Siegel. Hierarchical automata as model for state-charts. In R. Shyamasundar and K. Euda, editors, Third Asian Computing Science Conference. Advances in Computing Sience - ASIAN’97, volume 1345 of Lecture Notes in Computer Science, pages 181–196. Springer-Verlag, 1997.
R. Milner. Communication and Concurrency. Series in Computer Science. Prentice Hall, 1989.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer Science+Business Media New York
About this paper
Cite this paper
Latella, D., Majzik, I., Massink, M. (1999). Towards a Formal Operational Semantics of UML Statechart Diagrams. In: Ciancarini, P., Fantechi, A., Gorrieri, R. (eds) Formal Methods for Open Object-Based Distributed Systems. FMOODS 1999. IFIP — The International Federation for Information Processing, vol 10. Springer, Boston, MA. https://doi.org/10.1007/978-0-387-35562-7_25
Download citation
DOI: https://doi.org/10.1007/978-0-387-35562-7_25
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-4757-5266-3
Online ISBN: 978-0-387-35562-7
eBook Packages: Springer Book Archive