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 条

[1]

[Anonymous], P 19 INT C SOFTW ENG

[2]

[Anonymous], 2010, Software Engineering: a Practitioner's Approach

[3]

Baier C, 2008, PRINCIPLES OF MODEL CHECKING, P1

[4]

Baresi L., 2011, LNCS, V6957, P267

[5]

Behrmann G, 2004, LECT NOTES COMPUT SC, V3185, P200

[6] PRIMA-UML: a performance validation incremental methodology on early UML diagrams [J].

Cortellessa, V ;

Mirandola, R .

SCIENCE OF COMPUTER PROGRAMMING, 2002, 44 (01) :101-129

[7]

Debbabi M, 2010, VERIFICATION AND VALIDATION IN SYSTEMS ENGINEERING: ASSESSING UML/SYSML DESIGN MODELS, P1, DOI 10.1007/978-3-642-15228-3_1

[8] Symbolic Model Checking of Hierarchical UML State Machines [J].

Dubrovin, Jori ;

Junttila, Tommi .

2008 8TH INTERNATIONAL CONFERENCE ON APPLICATION OF CONCURRENCY TO SYSTEM DESIGN, PROCEEDINGS, 2008, :108-117

[9]

Dwyer M. B., 1999, Proceedings of the 1999 International Conference on Software Engineering (IEEE Cat. No.99CB37002), P411, DOI 10.1109/ICSE.1999.841031

[10]

eclipse.org, 2014, PAP

← 1 2 3 →