Model checking for an executable subset of UML

被引：5
|
作者：
Xie, F [1 ]
Levin, V [1 ]
Browne, JC [1 ]
机构：
[1] Univ Texas, Dept Comp Sci, Austin, TX 78712 USA
来源：
16TH ANNUAL INTERNATIONAL CONFERENCE ON AUTOMATED SOFTWARE ENGINEERING (ASE 2001), PROCEEDINGS | 2001年
关键词：
D O I：
10.1109/ASE.2001.989823
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
This paper presents an approach to model checking software system designs specified in xUML [3, 9], an executable subset of UML. This approach is enabled by the execution semantics of xUML and is based on automatic translation from xUML to SIR [2], the input language of the COSPAN [2] model checker Model transformations are applied to reduce the state space of the resulting SIR model that is to be verified by COSPAN. An xUML level logic for specifying properties to be checked is defined. Automated support is provided for translating properties specified in the logic to SIR representations and mapping error traces generated by COSPAN to xUML representations.
引用
收藏
页码：333 / 336
页数：4
相关论文
共 50 条
  • [1] Towards model checking executable UML specifications in mCRL2
    Hansen, Helle Hvid
    Ketema, Jeroen
    Luttik, Bas
    Mousavi, MohammadReza
    van de Pol, Jaco
    [J]. INNOVATIONS IN SYSTEMS AND SOFTWARE ENGINEERING, 2010, 6 (1-2) : 83 - 90
  • [2] Towards a Formal Account of a Foundational Subset for Executable UML Models
    Crane, Michelle L.
    Dingel, Juergen
    [J]. MODEL DRIVEN ENGINEERING LANGUAGES AND SYSTEMS, PROCEEDINGS, 2008, 5301 : 675 - 689
  • [3] Executable Counterexamples in Software Model Checking
    Gennari, Jeffrey
    Gurfinkel, Arie
    Kahsai, Temesghen
    Navas, Jorge A.
    Schwartz, Edward J.
    [J]. VERIFIED SOFTWARE: THEORIES, TOOLS, AND EXPERIMENTS, (VSTTE 2018), 2018, 11294 : 17 - 37
  • [4] 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
  • [5] Model checking UML statecharts
    Dong, W
    Wang, J
    Qi, X
    Qi, ZC
    [J]. APSEC 2001: EIGHTH ASIA-PACIFIC SOFTWARE ENGINEERING CONFERENCE, PROCEEDINGS, 2001, : 363 - 370
  • [6] UML for executable specification
    Douglass, BP
    [J]. EDN, 2001, 46 (18) : 83 - +
  • [7] Consistency Checking of UML Business Model
    Vasilecas, Olegas
    Dubauskaite, Ruta
    Rupnik, Rok
    [J]. TECHNOLOGICAL AND ECONOMIC DEVELOPMENT OF ECONOMY, 2011, 17 (01) : 133 - 150
  • [8] Model checking dynamic UML consistency
    Department of Informatics, School of Math., Peking University, Beijing, China
    不详
    [J]. Lect. Notes Comput. Sci., 2006, (440-459):
  • [9] Model checking for UML use cases
    Shinkawa, Yoshiyuki
    [J]. SOFTWARE ENGINEERING RESEARCH, MANAGEMENT AND APPLICATIONS, 2008, 150 : 233 - 246
  • [10] Model checking of UML 2.0 interactions
    Knapp, Alexander
    Wuttke, Jochen
    [J]. MODELS IN SOFTWARE ENGINEERING, 2007, 4364 : 42 - +
12345