Towards Checking Parametric Reachability for UML State Machines

被引：0
|
作者：
Niewiadomski, Artur [1 ]
Penczek, Wojciech [1 ,2 ]
Szreter, Maciej [2 ]
机构：
[1] Univ Podlasie, ICS, Siedlce, Poland
[2] Polish Acad Sci, ICS, Warsaw, Poland
来源：
PERSPECTIVES OF SYSTEMS INFORMATICS | 2010年 / 5947卷
关键词：
D O I：
暂无
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
The paper presents a new approach to model checking of systems specified in UML. All the executions of an UML system (unfolded to a. given depth) are encoded directly into a boolean propositional formula, satisfiability of which is checked using a SAT-solver. Contrary to other UML verification tools we do not use any of the existing model checkers as we do not translate UML specifications into an intermediate formalism. Moreover, we introduce some parametric extensions to the method. The method has been implemented as the (prototype) tool BMC4UML and several experimental results are presented.
引用
收藏
页码：319 / +
页数：2
相关论文
共 50 条
  • [1] Formalising UML state machines for model checking
    Lilius, J
    Paltor, IP
    UML'99 - THE UNIFIED MODELING LANGUAGE: BEYOND THE STANDARD, 1999, 1723 : 430 - 445
  • [2] A New Approach to Model Checking of UML State Machines
    Niewiadomski, Artur
    Penczek, Wojciech
    Szreter, Maciej
    FUNDAMENTA INFORMATICAE, 2009, 93 (1-3) : 289 - 303
  • [3] Symbolic Model Checking of Hierarchical UML State Machines
    Dubrovin, Jori
    Junttila, Tommi
    2008 8TH INTERNATIONAL CONFERENCE ON APPLICATION OF CONCURRENCY TO SYSTEM DESIGN, PROCEEDINGS, 2008, : 108 - 117
  • [4] Checking consistency in UML diagrams: Classes and state machines
    Rasch, H
    Wehrheim, H
    FORMAL METHODS FOR OPEN OBJECT-BASED DISTRIBUTED SYSTEMS, PROCEEDINGS, 2003, 2884 : 229 - 243
  • [5] Detecting policy conflicts by model checking UML state machines
    Ter Beek, Maurice H.
    Gnesi, Stefania
    Montangero, Carlo
    Semini, Laura
    FEATURE INTERACTIONS IN SOFTWARE AND COMMUNICATION SYSTEMS X, 2009, : 59 - +
  • [6] A rule-based Approach to Model Checking of UML State Machines
    Grobelna, Iwona
    Grobelny, Michal
    Stefanowicz, Lukasz
    PROCEEDINGS OF THE INTERNATIONAL CONFERENCE OF COMPUTATIONAL METHODS IN SCIENCES AND ENGINEERING 2016 (ICCMSE-2016), 2016, 1790
  • [7] Translation of UML 2 Activity Diagrams into Finite State Machines for Model Checking
    Raschke, Alexander
    2009 35TH EUROMICRO CONFERENCE ON SOFTWARE ENGINEERING AND ADVANCED APPLICATIONS, PROCEEDINGS, 2009, : 149 - 154
  • [8] Comparing the state-based and behavioural approaches to checking consistency between associations and state machines in UML
    Yeung, WL
    INTELLIGENT AND ADAPTIVE SYSTEMS AND SOFTWARE ENGINEERING, 2004, : 233 - 238
  • [9] Slicing of UML State Machines
    Lano, Kevin
    AIC '09: PROCEEDINGS OF THE 9TH WSEAS INTERNATIONAL CONFERENCE ON APPLIED INFORMATICS AND COMMUNICATIONS: RECENT ADVANCES IN APPLIED INFORMAT AND COMMUNICATIONS, 2009, : 63 - +
  • [10] Enhancing UML state machines with aspects
    Zhang, Gefei
    Hoelzl, Matthias
    Knapp, Alexander
    MODEL DRIVEN ENGINEERING LANGUAGES AND SYSTEMS, PROCEEDINGS, 2007, 4735 : 529 - +
12345