Formalising UML state machines for model checking

被引：0
|
作者：
Lilius, J [1 ]
Paltor, IP [1 ]
机构：
[1] Turku Ctr Comp Sci, FIN-20520 Turku, Finland
来源：
UML'99 - THE UNIFIED MODELING LANGUAGE: BEYOND THE STANDARD | 1999年 / 1723卷
关键词：
D O I：
暂无
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
The paper discusses a complete formalisation of UML state machine semantics. This formalisation is given in terms of an operational semantics and it can be used as the basis for code-generation, simulation and verification tools for UML Statecharts diagrams. The formalisation is done in two steps. First, the structure of a UML state machine is translated into a term rewriting system. In the second step, the operational semantics of state machines is defined. In addition, some problematic situations that may arise are discussed. Our formalisation is able to deal with all the features of UML state machines and it has been implemented in the vUML tool, a tool for model-checking UML models.
引用
收藏
页码：430 / 445
页数：16
相关论文
共 50 条
  • [1] A New Approach to Model Checking of UML State Machines
    Niewiadomski, Artur
    Penczek, Wojciech
    Szreter, Maciej
    [J]. FUNDAMENTA INFORMATICAE, 2009, 93 (1-3) : 289 - 303
  • [2] Symbolic Model Checking of Hierarchical UML State Machines
    Dubrovin, Jori
    Junttila, Tommi
    [J]. 2008 8TH INTERNATIONAL CONFERENCE ON APPLICATION OF CONCURRENCY TO SYSTEM DESIGN, PROCEEDINGS, 2008, : 108 - 117
  • [3] Detecting policy conflicts by model checking UML state machines
    Ter Beek, Maurice H.
    Gnesi, Stefania
    Montangero, Carlo
    Semini, Laura
    [J]. FEATURE INTERACTIONS IN SOFTWARE AND COMMUNICATION SYSTEMS X, 2009, : 59 - +
  • [4] A rule-based Approach to Model Checking of UML State Machines
    Grobelna, Iwona
    Grobelny, Michal
    Stefanowicz, Lukasz
    [J]. PROCEEDINGS OF THE INTERNATIONAL CONFERENCE OF COMPUTATIONAL METHODS IN SCIENCES AND ENGINEERING 2016 (ICCMSE-2016), 2016, 1790
  • [5] Formalising concurrent UML state machines using coloured Petri nets
    Andre, Etienne
    Benmoussa, Mohamed Mahdi
    Choppy, Christine
    [J]. FORMAL ASPECTS OF COMPUTING, 2016, 28 (05) : 805 - 845
  • [6] Translation of UML 2 Activity Diagrams into Finite State Machines for Model Checking
    Raschke, Alexander
    [J]. 2009 35TH EUROMICRO CONFERENCE ON SOFTWARE ENGINEERING AND ADVANCED APPLICATIONS, PROCEEDINGS, 2009, : 149 - 154
  • [7] Towards Checking Parametric Reachability for UML State Machines
    Niewiadomski, Artur
    Penczek, Wojciech
    Szreter, Maciej
    [J]. PERSPECTIVES OF SYSTEMS INFORMATICS, 2010, 5947 : 319 - +
  • [8] Checking consistency in UML diagrams: Classes and state machines
    Rasch, H
    Wehrheim, H
    [J]. FORMAL METHODS FOR OPEN OBJECT-BASED DISTRIBUTED SYSTEMS, PROCEEDINGS, 2003, 2884 : 229 - 243
  • [9] Model checking of hierarchical state machines
    Alur, R
    Yannakakis, M
    [J]. ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 2001, 23 (03): : 273 - 303
  • [10] Lazy model checking for recursive state machines
    Dubslaff, Clemens
    Wienhoeft, Patrick
    Fehnker, Ansgar
    [J]. SOFTWARE AND SYSTEMS MODELING, 2024, 23 (02): : 369 - 401
12345