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]Yuan Li, Xing-Chen Wang, Lin Huang, Yun-Lei Zhao. Order-Revealing Encryption: File-Injection Attack and Forward Security[J]. Journal of Computer Science and Technology, 2021, 36(4): 877-895. DOI: 10.1007/s11390-020-0060-y
    [2]Yan-Hong Fan, Mei-Qin Wang, Yan-Bin Li, Kai Hu, Mu-Zhou Li. A Secure IoT Firmware Update Scheme Against SCPA and DoS Attacks[J]. Journal of Computer Science and Technology, 2021, 36(2): 419-433. DOI: 10.1007/s11390-020-9831-8
    [3]Qi-Qi Lai, Bo Yang, Yong Yu, Zhe Xia, Yan-Wei Zhou, Yuan Chen. Updatable Identity-Based Hash Proof System Based on Lattices and Its Application to Leakage-Resilient Public-Key Encryption Schemes[J]. Journal of Computer Science and Technology, 2018, 33(6): 1243-1260. DOI: 10.1007/s11390-018-1885-5
    [4]Jing Xu, Wen-Tao Zhu. A Generic Framework for Anonymous Authentication in Mobile Networks[J]. Journal of Computer Science and Technology, 2013, 28(4): 732-742. DOI: 10.1007/s11390-013-1371-z
    [5]Yan Zhu, Hong-Xin Hu, Gail-Joon Ahn, Huai-Xi Wang, Shan-Biao Wang. Provably Secure Role-Based Encryption with Revocation Mechanism[J]. Journal of Computer Science and Technology, 2011, 26(4): 697-710. DOI: 10.1007/s11390-011-1169-9
    [6]Hai-Bo Tian, Willy Susilo, Yang Ming, Yu-Min Wang. A Provable Secure ID-Based Explicit Authenticated Key Agreement Protocol Without Random Oracles[J]. Journal of Computer Science and Technology, 2008, 23(5): 832-842.
    [7]Yong-Dong Zhang, Sheng Tang, Jin-Tao Li. Secure and Incidental Distortion Tolerant Digital Signature for Image Authentication[J]. Journal of Computer Science and Technology, 2007, 22(4): 618-625.
    [8]Sin-Kyu Kim, Jae-Woo Choi, Dae-Hun Nyang, Gene-Beck Hahn, Joo-Seok Song. Smart Proactive Caching Scheme for Fast Authenticated Handoff in Wireless LAN[J]. Journal of Computer Science and Technology, 2007, 22(3): 476-480.
    [9]Qing-Hua Zheng, David L. Pepyne, Qing Wang. New Approach to WLAN Security with Synchronized Pseudo Random[J]. Journal of Computer Science and Technology, 2004, 19(6).
    [10]ZHENG Dong, CHEN Kefei, YOU Jinyuan. Multiparty Authentication Services and Key Agreement Protocols with Semi-Trusted Third Party[J]. Journal of Computer Science and Technology, 2002, 17(6).
    • Supplements (0)

Catalog

    Get Citation
    PDF
    XML
    Article views (27) 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