Abstract
UML is a widely-used, general purpose modeling language. But its lack of a rigorous semantics forbids the thorough analysis of designed solution, and thus precludes the discovery of significant problems at design time. To bridge the gap, the paper investigates the underlying semantics of UML state machine diagrams, along with the time-related modeling elements of MARTE, the profile for modeling and analysis of real-time embedded systems, and proposes a formal operational semantics based on extended hierarchical timed automata. The approach is exemplified on a simple example taken from the automotive domain. Verification is accomplished by translating designed models into the input language of the UPPAAL model checker.
Similar content being viewed by others
Explore related subjects
Discover the latest articles, news and stories from top researchers in related subjects.References
OMG. UML profile for MARTE: Modeling and analysis of real-time embedded systems. Version 1.0, formal/2009-11-02, 2009, http://www.omg.org/spec/MARTE/1.0/.
Baresi L, Pezze M. On formalizing UML with high-level Petri nets. In Concurrent Object-Oriented Programming and Petri Nets, Springer Verlag, 2001, pp.276–304.
Crane M, Dingel J. Towards a formal account of a foundational subset for executable UML models. In Proc. the 11th International Conference on Model Driven Engineering Languages and Systems, October 2008, pp.675–689.
David A, Möller M, Yi W. Formal verification of UML statecharts with real-time extensions. In Proc. the 5th Int. Conf. Fundamental Approaches to Software Engineering, Apr. 2002, pp.218–232.
Latella D, Majzik I, Massink M. Towards a formal operational semantics of UML statechart diagrams. In Proc. the 3rd International Conference on Formal Methods for Open Object-Based Distributed Systems, March 1999, p.465.
André C, Mallet F, Peraldi-Frati M. A multiform time approach to real-time system modeling: Application to an automotive system. In Proc. the International Symposium on Industrial Embedded Systems, July 2007, pp.234–241.
Mallet F, de Simone F. MARTE: A profile for RT/E systems modeling, analysis–and simulation? In Proc. the 1st Simutools, June 2008, Article No.43.
OMG. UML profile for MARTE: Modeling and analysis of real-time embedded systems. Version 1.1, formal/2011-06-02, 2011, http://www.omg.org/spec/MARTE/1.1.
Alur R, Dill D. A theory of timed automata. Theoretical Computer Science, 1994, 126(2): 183–235.
Berthomieu B, Ribet P, Vernadat F. The tool TINA–Construction of abstract state spaces for petri nets and time petri nets. International Journal of Production Research, 2004, 42(14): 2741–2756.
Fecher H, Schönborn J, Kyas M, de Roever W. 29 new unclarities in the semantics of UML 2.0 state machines. In Proc. the 7th International Conference on Formal Methods and Software Engineering, November 2005, pp.52–65.
OMG. OMG unified modeling languageTM (OMG UML), superstructure. Version 2.2, 2009, http://www.omg.org/spec/UML/2.2/Superstructure.
Mikk E, Lakhnechi Y, Siegel M. Hierarchical automata as model for statecharts. In Proc. the 3rd Asian Computing Science Conf. Advance in Computing Science, December 1997, pp.181–196.
Behrmann G, David A, Larsen K. A tutorial on UPPAAL. In Proc. the International Conference on Formal Methods for the Design of Real-time Systems, July 2004, pp.33–35.
Lamport L. Time, clocks, and the ordering of events in a distributed system. Communications of the ACM, 1978, 21(7): 558–565.
Mallet F, Andr´e C. On the semantics of UML/MARTE clock constraints. In Proc. the Int. Symp. Object/Component/Service-Oriented Real-Time Distributed Computing, Mar. 2009, pp.305–312.
Ge N, Pantel M. Time properties dedicated semantics for UML-MARTE safety critical real-time system verification. In Proc. the 8th European Conference on Modelling Foundations and Applications, July 2012, pp.25–39.
Crane M, Dingel J. On the semantics of UML state machines: Categorization and comparision. Technical Report 2005-501, Queen’s University, 2005.
Harel D, Naamad A. The STATEMATE semantics of statecharts. ACM Transactions on Software Engineering and Methodology, 1996, 5(4): 293–333.
David A, Möller M. From HUPPAAL to UPPAAL: A translation from hierarchical timed automata to flat timed automata. Technical Report, University of Aarhus, 2001.
Giese H, Burmester S. Real-time statechart semantics. Technical Report TR-RI-03-239, University of Paderborn, 2003.
Akshay S, Bollig B, Gastin P, Mukund M, Kumar K N. Distributed timed automata with independently evolving clocks. In Proc. the 19th International Conference on Concurrency Theory, August 2008, pp.82–97.
Hu Z, Shatz S. Explicit modeling of semantics associated with composite states in UML statecharts. Automated Software Engineering, 2006, 13(4): 423–467.
Hölscher K, Ziemann P, Gogolla M. On translating UML models into graph transformation systems. Journal of Visual Languages & Computing, 2006, 17(1): 78–105.
Kong J, Zhang K, Dong J, Xu D. Specifying behavioral semantics of UML diagrams through graph transformations. Journal of Systems and Software, 2009, 82(2): 292–306.
Bindelli S, Di Nitto E, Furia C et al. Using compositionality to formally model and analyze systems built of a high number of components. In Proc. the 15th Int. Conf. Eng. of Complex Computer Systems, Mar. 2010, pp.85–94.
Author information
Authors and Affiliations
Corresponding author
Additional information
This work was supported by the European Community 7th Framework Program (FP7/2007-2013) under Grant agreement No. 248864 (MADES) and the National Natural Science Foundation of China under Grant No. 61202002.
Electronic Supplementary Material
Below is the link to the electronic supplementary material.
Rights and permissions
About this article
Cite this article
Zhou, Y., Baresi, L. & Rossi, M. Towards a Formal Semantics for UML/MARTE State Machines Based on Hierarchical Timed Automata. J. Comput. Sci. Technol. 28, 188–202 (2013). https://doi.org/10.1007/s11390-013-1322-8
Received:
Revised:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s11390-013-1322-8