UML Statecharts' PTL Formal Semantics

被引:0
|
作者
Zhang, PengFei [1 ]
Duan, ZhenHua [2 ]
Tian, Cong [2 ]
机构
[1] Huaibei Coal Ind Teachers Coll, Sch Comp Sci & Technol, Huaibei 235000, Peoples R China
[2] Xidian Univ, Inst Comp Theory Technol, Xian 710071, Peoples R China
关键词
Projection Temporal Logic; UML Statecharts; Formal Semantics; Verification; Simulation;
D O I
10.1109/IITA.2009.309
中图分类号
TP18 [人工智能理论];
学科分类号
081104 ; 0812 ; 0835 ; 1405 ;
摘要
An approach for transforming UML statecharts into Projection Temporal Logic(PTL) formal models for system's simulation and verification is presented in this paper. UML Statechart is a graphic tool used to describe systems' behaviors, but it lacks formal semantics. PTL is a kind of temporal logic interpreted over discrete state sequences (intervals). With PTL, the formal semantics of UML Statecharts is defined. By transforming a UML statecharts into PTL model and describing properties with PTL, the system can be formally verified in the same logic frame and further simulated by Tempura an executable subset of PTL. A tool has been developed for automatically transforming UML statechart diagrams into PTL formal models which will facilitate system's simulation and verification.
引用
收藏
页码:381 / +
页数:2
相关论文
共 50 条
  • [1] A formal semantics of UML statecharts by model transition systems
    Varró, D
    [J]. GRAPH TRANSFORMATIONS, PROCEEDINGS, 2002, 2505 : 378 - 392
  • [2] A formal semantics of UML StateCharts by means of timed Petri Nets
    Hammal, Y
    [J]. FORMAL TECHNIQUES FOR NEWTOWRKED AND DISTRIBUTED SYSTEMS - FORTE 2005, 2005, 3731 : 38 - 52
  • [3] Semantics of UML statecharts in PVS
    Aredo, DB
    [J]. 7TH WORLD MULTICONFERENCE ON SYSTEMICS, CYBERNETICS AND INFORMATICS, VOL IX, PROCEEDINGS: COMPUTER SCIENCE AND ENGINEERING: II, 2003, : 77 - 82
  • [4] An approach to formalizing the semantics of UML statecharts
    Zhan, XD
    Miao, HK
    [J]. CONCEPTUAL MODELING - ER 2004, PROCEEDINGS, 2004, 3288 : 753 - 765
  • [5] UML Statecharts Compositional Semantics in LOTOS
    Mrowka, Rafal
    Szmuc, Tomasz
    [J]. PROCEEDINGS OF THE INTERNATIONAL SYMPOSIUM ON PARALLEL AND DISTRIBUTED COMPUTING, 2008, : 459 - 463
  • [6] Formalizing the semantics of UML statecharts with Z
    Zhan, XD
    Miao, HK
    Liu, L
    [J]. FOURTH INTERNATIONAL CONFERENCE ON COMPUTER AND INFORMATION TECHNOLOGY, PROCEEDINGS, 2004, : 1116 - 1121
  • [7] A formal testing framework for UML statecharts
    Zhan, Xuede
    [J]. SNPD 2007: Eighth ACIS International Conference on Software Engineering, Artificial Intelligence, Networking, and Parallel/Distributed Computing, Vol 3, Proceedings, 2007, : 882 - 887
  • [8] Formal modeling and analysis of UML statecharts
    Yao, Shuzhen
    Jin, Maozhong
    [J]. Beijing Hangkong Hangtian Daxue Xuebao/Journal of Beijing University of Aeronautics and Astronautics, 2007, 33 (04): : 472 - 476
  • [9] Mechanized semantics and refinement of UML-Statecharts
    Feng Sheng
    Liang Dou
    Zong-yuan Yang
    [J]. Frontiers of Information Technology & Electronic Engineering, 2017, 18 : 1773 - 1783
  • [10] A structured operational semantics for UML-statecharts
    Michael von der Beeck
    [J]. Software and Systems Modeling, 2002, 1 (2): : 130 - 141