Model checking UML statecharts

被引：9
|
作者：
Dong, W [1 ]
Wang, J [1 ]
Qi, X [1 ]
Qi, ZC [1 ]
机构：
[1] Natl Lab Parallel & Distributed Proc, Changsha, Peoples R China
来源：
APSEC 2001: EIGHTH ASIA-PACIFIC SOFTWARE ENGINEERING CONFERENCE, PROCEEDINGS | 2001年
关键词：
D O I：
10.1109/APSEC.2001.991503
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
Unified Modeling Language (UML) has been widely used in software development. Verifying if an UML model meets the required properties has become a key issue. Model checking is an important technology of automatic formal verification to ensure the correctness of design specifications. An approach of model checking UML statecharts is given in this paper At first, the brief syntax and semantics of UML statecharts are described. Then, the way of how UML statecharts is structurally expressed by extended hierarchical automaton and the labeled transition system are defined. The correctness of operational semantics of UML statecharts can be ensured through finding the maximal non-conflict transition set. For the system with infinite runs, the operational semantics can be mapped to a Buchi automaton and linear temporal logic properties of the system can be verified based on the automata theory of model checking. The paper also presents the method of verifying complex,system consist of multiple objects modeled by statecharts and collaboration diagram.
引用
收藏
页码：363 / 370
页数：8
相关论文
共 50 条
  • [31] A coalgebraic approach for the formalization of UML statecharts
    Du, DH
    Cao, HH
    He, KQ
    Peng, R
    [J]. Proceedings of the 11th Joint International Computer Conference, 2005, : 793 - 798
  • [32] 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
  • [33] Model Checking UML Activity Diagrams in FDR
    Xu, Dong
    Miao, Huaikou
    Philbert, Nduwimfura
    [J]. PROCEEDINGS OF THE 8TH IEEE/ACIS INTERNATIONAL CONFERENCE ON COMPUTER AND INFORMATION SCIENCE, 2009, : 1035 - 1040
  • [34] Symbolic model checking of UML activity diagrams
    Eshuis, R
    [J]. ACM TRANSACTIONS ON SOFTWARE ENGINEERING AND METHODOLOGY, 2006, 15 (01) : 1 - 38
  • [35] Applying Model Checking to Concurrent UML Models
    Gagnon, Patrice
    Mokhati, Farid
    Badri, Mourad
    [J]. JOURNAL OF OBJECT TECHNOLOGY, 2008, 7 (01): : 59 - 84
  • [36] Formalising UML state machines for model checking
    Lilius, J
    Paltor, IP
    [J]. UML'99 - THE UNIFIED MODELING LANGUAGE: BEYOND THE STANDARD, 1999, 1723 : 430 - 445
  • [37] A Model Checking Based Approach for Containment Checking of UML Sequence Diagrams
    Muram, Faiz Ul
    Tran, Huy
    Zdun, Uwe
    [J]. 2016 23RD ASIA-PACIFIC SOFTWARE ENGINEERING CONFERENCE (APSEC 2016), 2016, : 73 - 80
  • [38] UML Statecharts的层次组合验证
    董威
    王戟
    齐治昌
    [J]. 计算机工程与应用, 2005, (11) : 37 - 38
  • [39] 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
  • [40] Using UML Statecharts with Knowledge Logic Guards
    Drusinsky, Doron
    Shing, Man-Tak
    [J]. MODEL DRIVEN ENGINEERING LANGUAGES AND SYSTEMS, PROCEEDINGS, 2009, 5795 : 586 - 590
12345