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

• Special Section on Selected Paper from NPC 2011 • 上一篇    下一篇

基于层次式时间自动机的UML/MARTE状态机图的形式语义

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

  • 收稿日期:2011-11-17 修回日期:2012-09-24 出版日期:2013-01-05 发布日期:2013-01-05
  • 基金资助:

    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.

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.

PDF (PC)

1878

UML是一种通用的建模语言,但是其缺少一种严格的形式化语义基础,从而无法对其所建模型进行形式化的分析以发现设计阶段的问题.本文结合了最新的MARTE规范中引入的时间相关模型元素,研究了UML状态机图的语义基础,提出一种基于扩展层次式时间自动机的形式操作语义方法.该方法通过一个汽车工业领域用例加以说明.基于该语义基础,提出一种算法,通过模型转换,自动地将UML/MARTE模型转换为模型检测工具UPPAAL的建模语言,验证了所提方法的正确性.

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.

[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!
Viewed
Full text


Abstract

Cited
  Shared   
  Discussed   
[1] 张钹; 张铃;. Statistical Heuristic Search[J]. , 1987, 2(1): 1 -11 .
[2] 孟力明; 徐晓飞; 常会友; 陈光熙; 胡铭曾; 李生;. A Tree-Structured Database Machine for Large Relational Database Systems[J]. , 1987, 2(4): 265 -275 .
[3] 林琦; 夏培肃;. The Design and Implementation of a Very Fast Experimental Pipelining Computer[J]. , 1988, 3(1): 1 -6 .
[4] 孙成政; 慈云桂;. A New Method for Describing the AND-OR-Parallel Execution of Logic Programs[J]. , 1988, 3(2): 102 -112 .
[5] 张钹; 张恬; 张建伟; 张铃;. Motion Planning for Robots with Topological Dimension Reduction Method[J]. , 1990, 5(1): 1 -16 .
[6] 王鼎兴; 郑纬民; 杜晓黎; 郭毅可;. On the Execution Mechanisms of Parallel Graph Reduction[J]. , 1990, 5(4): 333 -346 .
[7] 周权; 魏道政;. A Complete Critical Path Algorithm for Test Generation of Combinational Circuits[J]. , 1991, 6(1): 74 -82 .
[8] 赵靓海; 刘慎权;. An Environment for Rapid Prototyping of Interactive Systems[J]. , 1991, 6(2): 135 -144 .
[9] 商陆军; 许立辉;. Notes on the Design of an Integrated Object-Oriented DBMS Family[J]. , 1991, 6(4): 389 -394 .
[10] 许建国; 郭玉钗; 林宗楷;. HEPAPS:A PCB Automatic Placement System[J]. , 1992, 7(1): 39 -46 .
版权所有 © 《计算机科学技术学报》编辑部
本系统由北京玛格泰克科技发展有限公司设计开发 技术支持：support@magtech.com.cn
总访问量：