Verifying Implementation of UML Sequence Diagrams Using Java PathFinder

Author

Nguyen, Dinh-Phuc ; Luu, Chung-Tuyen ; Truong, Anh-Hoang ; Radics, Norbert

Author_Institution

Univ. of Eng. & Technol., Hanoi, Vietnam

fYear

2010

fDate

7-9 Oct. 2010

Firstpage

194

Lastpage

200

Abstract

The introduction of combined fragments to UML 2.x sequence diagrams makes it much harder for programmers to check manually the correctness of an implementation, especially when the fragments are nested. We develop an extension for Symbolic Java Path Finder (SPF) to verify if a Java program correctly implements its sequence diagram specification. Our main contribution is an algorithm to follow SPF exploration both when it advances and when it backtracks to find execution paths that are not specified in the specifications. We also generate the test cases that make the implementation go wrong for reproducing and debugging the bugs.

Keywords

Java; Unified Modeling Language; checkpointing; computer debugging; formal specification; formal verification; Java program; UML sequence diagrams; combined fragments; debugging; specifications; symbolic Java PathFinder; unified modeling language; Computer bugs; Java; Protocols; Search problems; Semantics; Unified modeling language; Virtual machining; Java PathFinder; UML sequence diagram; verification;

fLanguage

English

Publisher

ieee

Conference_Titel

Knowledge and Systems Engineering (KSE), 2010 Second International Conference on

Conference_Location

Hanoi

Print_ISBN

978-1-4244-8334-1

Type

conf

DOI

10.1109/KSE.2010.29

Filename

5632065