A Formal Verification Tool for UML Behavioral Diagrams

被引：0

作者：

Rebelo dos Santos, Luciana Brasil ^{[1
]}

Eras, Eduardo Rohde ^{[1
]}

de Santiago Junior, Valdivino Alexandre ^{[1
]}

Vijaykumar, Nandamudi Lankalapalli ^{[1
]}

机构：

[1] Inst Nacl Pesquisas Espaciais, BR-12201 Sao Jose Dos Campos, SP, Brazil

来源：

COMPUTATIONAL SCIENCE AND ITS APPLICATIONS - ICCSA 2014, PT 1 | 2014年 / 8579卷

关键词：

D O I：

暂无

中图分类号：

TP [自动化技术、计算机技术];

学科分类号：

0812 ;

摘要：

Unified Modeling Language (UML) is considered a standard for modeling object-oriented software. It supports several different diagrams that can be used to model behavior and structure of the software. With respect to formal verification, particularly Model Checking, the existing approaches are usually restricted to a single UML diagram. This paper presents a tool to convert UML behavioral diagrams (sequence, activity, and state machine) into Transition Systems to support software Model Checking. A peculiar feature of our tool is that it is developed as part of a larger effort to allow Model Checking of software built in accordance with UML, including several UML behavioral diagrams. We demonstrate the effectiveness of our approach by applying it to a classic case study and also to a real case study (embedded software) in the space domain.

引用

页码：696 / 711

页数：16

共 23 条

[11]

eclipse.org, 2014, ECLIPSE

[12] Tool support for verifying UML activity diagrams [J].

Eshuis, R ;

Wieringa, R .

IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 2004, 30 (07) :437-447

[13]

Holzmann G. J., 2004, SPIN MODEL CHECKER P, V1003

[14]

Kessler F.B., 2011, NUSMV HOME PAGE

[15]

Lam Vitus S. W., 2007, Nordic Journal of Computing, V14, P43

[16]

Latella D., 1999, Formal Aspects of Computing, V11, P637, DOI 10.1007/s001659970003

[17] Implementing statecharts in PROMELA/SPIN [J].

Mikk, E ;

Lakhnech, Y ;

Siegel, M ;

Holzmann, GJ .

2ND IEEE WORKSHOP ON INDUSTRIAL STRENGTH FORMAL SPECIFICATION TECHNIQUES - PROCEEDINGS, 1999, :90-101

[18]

OMG T.O.M.G., 1997, OMG UN MOD LANG OMG

[19] Automatic generation of test specifications for coverage of system state transitions [J].

Sarma, M. ;

Mall, R. .

INFORMATION AND SOFTWARE TECHNOLOGY, 2009, 51 (02) :418-432

[20]

Schafer T., 2001, Electronic Notes in Theoretical Computer Science, V55, DOI 10.1016/S1571-0661(04)00262-2

← 1 2 3 →