We use cookies to improve your experience with our site.

Indexed in:

SCIE, EI, Scopus, INSPEC, DBLP, CSCD, etc.

Submission System
(Author / Reviewer / Editor)
Advanced Search
Volume 28 Issue 1
January  2013
Turn off MathJax
Article Contents
Abstract
References
Related Articles
Yu Zhou, Luciano Baresi, Matteo Rossi. Towards a Formal Semantics for UML/MARTE State Machines Based on Hierarchical Timed Automata[J]. Journal of Computer Science and Technology, 2013, 28(1): 188-202. DOI: 10.1007/s11390-013-1322-8
Citation: Yu Zhou, Luciano Baresi, Matteo Rossi. Towards a Formal Semantics for UML/MARTE State Machines Based on Hierarchical Timed Automata[J]. Journal of Computer Science and Technology, 2013, 28(1): 188-202. DOI: 10.1007/s11390-013-1322-8
shu

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

  • 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

Funds: 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.
More Information
  • Received Date: November 16, 2011
  • Revised Date: September 23, 2012
  • Published Date: January 04, 2013
    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.
    • FullText(HTML)
    • References (26)
  • [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.
    • Relative Articles

  • Related Articles

    [1]Inès Mouakher, Fatma Dhaou, J. Christian Attiogbé. Event-Based Semantics of UML 2.X Concurrent Sequence Diagrams for Formal Verification[J]. Journal of Computer Science and Technology, 2022, 37(1): 4-28. DOI: 10.1007/s11390-021-1673-5
    [2]CHEN Chuanfeng, LI Zengzhi, TANG Yazhe, LIU Kangping. Internet Network Resource Information Model[J]. Journal of Computer Science and Technology, 2002, 17(6).
    [3]XU Mingwei, WU Jianping. A Formal Approach to Protocol Performance Testing[J]. Journal of Computer Science and Technology, 1999, 14(1): 81-87.
    [4]Xue Jinyun. Formal Derivation of Graph AlgorithmicPrograms Using Partition-and-Recur[J]. Journal of Computer Science and Technology, 1998, 13(6): 553-561.
    [5]Hao Ruibing, Wu Jianping. A Formal Approach to Protocol Interoperability Testing[J]. Journal of Computer Science and Technology, 1998, 13(1): 79-90.
    [6]Xu Manwu, Lu Jianfeng, Zeng Fancong, Dai Jinwn. A Formal Semantics for DAI Language NUML[J]. Journal of Computer Science and Technology, 1995, 10(3): 227-238.
    [7]Zhang Xing er, Zhu Xiaojun, Li Jianxin, Dong Jianning. Source-to-Source Conversion Based on Formal Definition[J]. Journal of Computer Science and Technology, 1991, 6(2): 178-184.
    [8]Li Layuan. A New Formal Method for Communication Protocol Specification[J]. Journal of Computer Science and Technology, 1989, 4(1): 14-22.
    [9]Hou Luoming. A General and Formal Method for the Program Static Analysis[J]. Journal of Computer Science and Technology, 1987, 2(2): 115-123.
    [10]Tang Tonggao, Zhao Zhaokeng. Stack Method in Program Semantics[J]. Journal of Computer Science and Technology, 1987, 2(1): 51-63.
    • Supplements (0)

Catalog

    Get Citation
    PDF
    XML
    Article views (30) PDF downloads (1857) Cited by()
    Related

    Copyright ©2025 JCST, All Rights Reserved     京ICP备05002829号-1

    Institute of Computing Technology, Chinese Academy of Sciences
    P.O. Box 2704, Beijing 100190, P.R. China

    Tel.: 86-10-62610746 E-mail: jcst@ict.ac.cn

    /

    DownLoad:  Full-Size Img  PowerPoint
    Return
    Return