Journal of Computer Science and Technology
Quick Search in JCST
 Advanced Search 
      Home | PrePrint | SiteMap | Contact Us | FAQ
 
Indexed by   SCIE, EI ...
Bimonthly    Since 1986
Journal of Computer Science and Technology 2013, Vol. 28 Issue (1) :188-202    DOI: 10.1007/s11390-013-1322-8
Software Engineering Current Issue | Archive | Adv Search << 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. 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

Abstract
Reference
Related Articles
Download: [PDF 934KB]     Export: BibTeX or EndNote (RIS)  
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.
Articles by authors
Yu Zhou
Luciano Baresi
Matteo Rossi
Keywordstimed automata   state machine diagram   formal semantics     
Received 2011-11-17;
Fund:

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.

Cite this article:   
Yu Zhou, Luciano Baresi, and Matteo Rossi.Towards a Formal Semantics for UML/MARTE State Machines Based on Hierarchical Timed Automata[J]  Journal of Computer Science and Technology, 2013,V28(1): 188-202
URL:  
http://jcst.ict.ac.cn:8080/jcst/EN/10.1007/s11390-013-1322-8
Copyright 2010 by Journal of Computer Science and Technology