›› 2013, Vol. 28 ›› Issue (1): 188-202.doi: 10.1007/s11390-013-1322-8

• Software Engineering • Previous Articles     Next Articles

Towards a Formal Semantics for UML/MARTE State Machines Based on Hierarchical Timed Automata

Yu Zhou1,2 (周宇), Luciano Baresi3, and Matteo Rossi3   

  1. 1. College of Computer Science, Nanjing University of Aeronautics and Astronautics, Nanjing 210016, China;
    2. State Key Laboratory for Novel Software Technology, Nanjing University, Nanjing 210093, China;
    3. Department of Electronics and Information, Politecnico di Milano, Milan 20133, Italy
  • Received:2011-11-17 Revised:2012-09-24 Online:2013-01-05 Published:2013-01-05
  • Supported by:

    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.

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.

[1] OMG. UML profile for MARTE: Modeling and analysis ofreal-time embedded systems. Version 1.0, formal/2009-11-02,2009, http://www.omg.org/spec/MARTE/1.0/.
[2] Baresi L, Pezze M. On formalizing UML with high-level Petrinets. In Concurrent Object-Oriented Programming and PetriNets, Springer Verlag, 2001, pp.276-304.
[3] Crane M, Dingel J. Towards a formal account of a foundationalsubset for executable UML models. In Proc. the 11thInternational Conference on Model Driven Engineering Languagesand Systems, October 2008, pp.675-689.
[4] David A, Möller M, Yi W. Formal verification of UML statechartswith real-time extensions. In Proc. the 5th Int.Conf. Fundamental Approaches to Software Engineering,Apr. 2002, pp.218-232.
[5] Latella D, Majzik I, Massink M. Towards a formal operationalsemantics of UML statechart diagrams. In Proc. the3rd International Conference on Formal Methods for OpenObject-Based Distributed Systems, March 1999, p.465.
[6] Andr′e C, Mallet F, Peraldi-Frati M. A multiform time approachto real-time system modeling: Application to an automotivesystem. In Proc. the International Symposium onIndustrial Embedded Systems, July 2007, pp.234-241.
[7] Mallet F, de Simone F. MARTE: A profile for RT/E systemsmodeling, analysis-and simulation? In Proc. the 1st Simutools,June 2008, Article No.43.
[8] OMG. UML profile for MARTE: Modeling and analysis ofreal-time embedded systems. Version 1.1, formal/2011-06-02,2011, http://www.omg.org/spec/MARTE/1.1.
[9] Alur R, Dill D. A theory of timed automata. TheoreticalComputer Science, 1994, 126(2): 183-235.
[10] Berthomieu B, Ribet P, Vernadat F. The tool TINA-Construction of abstract state spaces for petri nets and timepetri nets. International Journal of Production Research,2004, 42(14): 2741-2756.
[11] Fecher H, Schönborn J, Kyas M, de Roever W. 29 new unclaritiesin the semantics of UML 2.0 state machines. In Proc. the7th International Conference on Formal Methods and SoftwareEngineering, November 2005, pp.52-65.
[12] OMG. OMG unified modeling languageTM (OMG UML), superstructure.Version 2.2, 2009, http://www.omg.org/spec/UML/2.2/Superstructure.
[13] Mikk E, Lakhnechi Y, Siegel M. Hierarchical automata asmodel for statecharts. In Proc. the 3rd Asian Computing ScienceConf. Advance in Computing Science, December 1997,pp.181-196.
[14] Behrmann G, David A, Larsen K. A tutorial on UPPAAL. InProc. the International Conference on Formal Methods forthe Design of Real-time Systems, July 2004, pp.33-35.
[15] Lamport L. Time, clocks, and the ordering of events in a distributedsystem. Communications of the ACM, 1978, 21(7):558-565.
[16] Mallet F, Andr′e C. On the semantics of UML/MARTEclock constraints. In Proc. the Int. Symp.Object/Component/Service-Oriented Real-Time DistributedComputing, Mar. 2009, pp.305-312.
[17] Ge N, Pantel M. Time properties dedicated semantics forUML-MARTE safety critical real-time system verification. InProc. the 8th European Conference on Modelling Foundationsand Applications, July 2012, pp.25-39.
[18] Crane M, Dingel J. On the semantics of UML state machines:Categorization and comparision. Technical Report 2005-501,Queen’s University, 2005.
[19] Harel D, Naamad A. The STATEMATE semantics of statecharts.ACM Transactions on Software Engineering andMethodology, 1996, 5(4): 293-333.
[20] David A, Möller M. From HUPPAAL to UPPAAL: A translationfrom hierarchical timed automata to flat timed automata.Technical Report, University of Aarhus, 2001.
[21] Giese H, Burmester S. Real-time statechart semantics. TechnicalReport TR-RI-03-239, University of Paderborn, 2003.
[22] Akshay S, Bollig B, Gastin P, Mukund M, Kumar K N. Distributedtimed automata with independently evolving clocks.In Proc. the 19th International Conference on ConcurrencyTheory, August 2008, pp.82-97.
[23] Hu Z, Shatz S. Explicit modeling of semantics associated withcomposite states in UML statecharts. Automated SoftwareEngineering, 2006, 13(4): 423-467.
[24] Hölscher K, Ziemann P, GogollaM. On translating UML modelsinto graph transformation systems. Journal of Visual Languages& Computing, 2006, 17(1): 78-105.
[25] Kong J, Zhang K, Dong J, Xu D. Specifying behavioral semanticsof UML diagrams through graph transformations.Journal of Systems and Software, 2009, 82(2): 292-306.
[26] Bindelli S, Di Nitto E, Furia C et al. Using compositionalityto formally model and analyze systems built of a high numberof components. In Proc. the 15th Int. Conf. Eng. ofComplex Computer Systems, Mar. 2010, pp.85-94.
No related articles found!
Full text



[1] Zhang Bo; Zhang Ling;. Statistical Heuristic Search[J]. , 1987, 2(1): 1 -11 .
[2] Meng Liming; Xu Xiaofei; Chang Huiyou; Chen Guangxi; Hu Mingzeng; Li Sheng;. A Tree-Structured Database Machine for Large Relational Database Systems[J]. , 1987, 2(4): 265 -275 .
[3] Lin Qi; Xia Peisu;. The Design and Implementation of a Very Fast Experimental Pipelining Computer[J]. , 1988, 3(1): 1 -6 .
[4] Sun Chengzheng; Tzu Yungui;. A New Method for Describing the AND-OR-Parallel Execution of Logic Programs[J]. , 1988, 3(2): 102 -112 .
[5] Zhang Bo; Zhang Tian; Zhang Jianwei; Zhang Ling;. Motion Planning for Robots with Topological Dimension Reduction Method[J]. , 1990, 5(1): 1 -16 .
[6] Wang Dingxing; Zheng Weimin; Du Xiaoli; Guo Yike;. On the Execution Mechanisms of Parallel Graph Reduction[J]. , 1990, 5(4): 333 -346 .
[7] Zhou Quan; Wei Daozheng;. A Complete Critical Path Algorithm for Test Generation of Combinational Circuits[J]. , 1991, 6(1): 74 -82 .
[8] Zhao Jinghai; Liu Shenquan;. An Environment for Rapid Prototyping of Interactive Systems[J]. , 1991, 6(2): 135 -144 .
[9] Shang Lujun; Xu Lihui;. Notes on the Design of an Integrated Object-Oriented DBMS Family[J]. , 1991, 6(4): 389 -394 .
[10] Xu Jianguo; Gou Yuchai; Lin Zongkai;. HEPAPS:A PCB Automatic Placement System[J]. , 1992, 7(1): 39 -46 .

ISSN 1000-9000(Print)

CN 11-2296/TP

Editorial Board
Author Guidelines
Journal of Computer Science and Technology
Institute of Computing Technology, Chinese Academy of Sciences
P.O. Box 2704, Beijing 100190 P.R. China
E-mail: jcst@ict.ac.cn
  Copyright ©2015 JCST, All Rights Reserved