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
相关论文
共 12 条
  • [1] [Anonymous], 2006, P MODEV 2, P94
  • [2] UML Automatic Verification Tool with Formal Methods
    Beato, Ma Encarnacion
    Barrio-Solorzano, Manuel
    Cuesta, Carlos E.
    de la Fuente, Pablo
    [J]. ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2005, 127 (04) : 3 - 16
  • [3] BHADURI P, 2004, CS0407038 ARXIV COMP
  • [4] Compton Kevin, 2000, CSETR42300 U MICH
  • [5] CRANE ML, 2005, 2005501 QUEENS U
  • [6] DIETHERS K, 2002, P UML 02 WORKSHOP TU, P35
  • [7] DUBROVIN J, 2007, B23 HUT TCS
  • [8] KNAPP A, 2002, LECT NOTES COMPUTER, V2469, P395
  • [9] Lilius J., 1999, 14th IEEE International Conference on Automated Software Engineering, P255, DOI 10.1109/ASE.1999.802301
  • [10] NIEWIADOMSKI A, 2009, 7 INT ERSH MEM C PER, P229
12