Skip to main content
SpringerLink
Log in

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

  • Regular Paper
  • Published:
Journal of Computer Science and Technology Aims and scope Submit manuscript

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.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  1. 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/.

  2. 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.

  3. 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.

  4. 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.

  5. 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.

  6. 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.

  7. 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.

  8. 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.

  9. Alur R, Dill D. A theory of timed automata. Theoretical Computer Science, 1994, 126(2): 183–235.

    Article  MathSciNet  MATH  Google Scholar 

  10. 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.

    Article  MATH  Google Scholar 

  11. 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.

  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 as model for statecharts. In Proc. the 3rd Asian Computing Science Conf. Advance in Computing Science, December 1997, pp.181–196.

  14. 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.

  15. Lamport L. Time, clocks, and the ordering of events in a distributed system. Communications of the ACM, 1978, 21(7): 558–565.

    Article  MATH  Google Scholar 

  16. 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.

  17. 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.

  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 and Methodology, 1996, 5(4): 293–333.

    Article  Google Scholar 

  20. 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.

  21. Giese H, Burmester S. Real-time statechart semantics. Technical Report TR-RI-03-239, University of Paderborn, 2003.

  22. 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.

  23. Hu Z, Shatz S. Explicit modeling of semantics associated with composite states in UML statecharts. Automated Software Engineering, 2006, 13(4): 423–467.

    Article  Google Scholar 

  24. 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.

    Article  Google Scholar 

  25. 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.

    Article  Google Scholar 

  26. 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.

Download references

Author information

Authors and Affiliations

  1. College of Computer Science, Nanjing University of Aeronautics and Astronautics, Nanjing, 210016, China

    Yu Zhou

  2. State Key Laboratory for Novel Software Technology, Nanjing University, Nanjing, 210093, China

    Yu Zhou

  3. Department of Electronics and Information, Politecnico di Milano, Milan, 20133, Italy

    Luciano Baresi & Matteo Rossi

Authors
  1. Yu Zhou
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Luciano Baresi
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Matteo Rossi
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Yu Zhou.

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.

(DOC 26.5 kb)

Rights and permissions

Reprints 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

Download citation

  • Received:

  • Revised:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s11390-013-1322-8

Keywords

Search

Navigation