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 条
  • [1] Slicing hierarchical automata for model checking UML statecharts
    Wang, J
    Dong, W
    Qi, ZC
    [J]. FORMAL METHODS AND SOFTWARE ENGINEERING, PROCEEDINGS, 2002, 2495 : 435 - 446
  • [2] Rewrite rules and operational semantics for model checking UML statecharts
    Kwon, G
    [J]. UML 2000 - THE UNIFIED MODELING LANGUAGE, PROCEEDINGS: ADVANCING THE STANDARD, 2000, 1939 : 528 - 540
  • [3] Model checking for timed statecharts
    Qian, JY
    Xu, BW
    [J]. FORMAL TECHNIQUES FOR NETWORKED AND DISTRIBUTED SYSTEMS - FORTE 2005, 2005, 3731 : 261 - 274
  • [4] LTL model checking for statecharts
    Qian, Junyan
    Xu, Baowen
    [J]. Journal of Computational Information Systems, 2007, 3 (06): : 2241 - 2248
  • [5] Optimizing symbolic model checking for statecharts
    Chan, W
    Anderson, RJ
    Beame, P
    Jones, DH
    Notkin, D
    Warner, WE
    [J]. IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 2001, 27 (02) : 170 - 190
  • [6] On testing UML statecharts
    Massink, Mieke
    Latella, Diego
    Gnesi, Stefania
    [J]. JOURNAL OF LOGIC AND ALGEBRAIC PROGRAMMING, 2006, 69 (1-2): : 1 - 74
  • [7] A formal semantics of UML statecharts by model transition systems
    Varró, D
    [J]. GRAPH TRANSFORMATIONS, PROCEEDINGS, 2002, 2505 : 378 - 392
  • [8] Extending the UML Statecharts Notation to Model Security Aspects
    El-Attar, Mohamed
    Luqman, Hamza
    Karpati, Peter
    Sindre, Guttorm
    Opdahl, Andreas L.
    [J]. IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 2015, 41 (07) : 661 - 690
  • [9] Extending UML for Model Checking
    Shu, Xinfeng
    Wang, Mengnan
    Wang, Xiaobing
    [J]. STRUCTURED OBJECT-ORIENTED FORMAL LANGUAGE AND METHOD, SOFL+MSVL 2017, 2018, 10795 : 88 - 107
  • [10] 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
12345