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 条

[11] Model checking dynamic UML consistency
Zhao, Xiangpeng
Long, Quan
Qiu, Zongyan
[J]. Formal Methods and Software Engineering, Proceedings, 2006, 4260 : 440 - 459
[12] Using Executable UML to model Algorithmic Aspects of Visualization Systems
Braune, Annerose
Hennig, Stefan
[J]. 2009 7TH IEEE INTERNATIONAL CONFERENCE ON INDUSTRIAL INFORMATICS, VOLS 1 AND 2, 2009, : 301 - 306
[13] Model Checking UML Activity Diagrams in FDR
Xu, Dong
Miao, Huaikou
Philbert, Nduwimfura
[J]. PROCEEDINGS OF THE 8TH IEEE/ACIS INTERNATIONAL CONFERENCE ON COMPUTER AND INFORMATION SCIENCE, 2009, : 1035 - 1040
[14] Symbolic model checking of UML activity diagrams
Eshuis, R
[J]. ACM TRANSACTIONS ON SOFTWARE ENGINEERING AND METHODOLOGY, 2006, 15 (01) : 1 - 38
[15] Applying Model Checking to Concurrent UML Models
Gagnon, Patrice
Mokhati, Farid
Badri, Mourad
[J]. JOURNAL OF OBJECT TECHNOLOGY, 2008, 7 (01): : 59 - 84
[16] UML Executable: A Comparative Study of UML Compilers and Interpreters
Gotti, Sara
Mbarki, Samir
[J]. 2016 INTERNATIONAL CONFERENCE ON INFORMATION TECHNOLOGY FOR ORGANIZATIONS DEVELOPMENT (IT4OD), 2016,
[17] Formalising UML state machines for model checking
Lilius, J
Paltor, IP
[J]. UML'99 - THE UNIFIED MODELING LANGUAGE: BEYOND THE STANDARD, 1999, 1723 : 430 - 445
[18] Validating executable controller specifications through formal model checking
Scillieri, JJ
Butts, KR
Freudenberg, JS
[J]. PROCEEDINGS OF THE 2000 IEEE INTERNATIONAL SYMPOSIUM ON COMPUTER-AIDED CONTROL SYSTEM DESIGN, 2000, : 179 - 184
[19] A Model Checking Based Approach for Containment Checking of UML Sequence Diagrams
Muram, Faiz Ul
Tran, Huy
Zdun, Uwe
[J]. 2016 23RD ASIA-PACIFIC SOFTWARE ENGINEERING CONFERENCE (APSEC 2016), 2016, : 73 - 80
[20] From UML Component Diagram to an Executable Model Based on Petri Nets
Emadi, Sima
Shams, Fereidoon
[J]. INTERNATIONAL SYMPOSIUM OF INFORMATION TECHNOLOGY 2008, VOLS 1-4, PROCEEDINGS: COGNITIVE INFORMATICS: BRIDGING NATURAL AND ARTIFICIAL KNOWLEDGE, 2008, : 2780 - +

← 1 2 3 4 5 →