• Chỉ mục bởi
  • Năm xuất bản

Verifying implementation of UML sequence diagrams using Java PathFinder

Nguyen D.-P. University of Engineering and Technology, VNU, 144 Xuan Thuy, Hanoi, Viet Nam|
Radics N. | Truong A.-H. | Luu C.-T. Mitani Sangyo Co. Ltd., 1-5 Tamagawa-Cho, Kanazawa Ishikawa 920-8685, Japan|

Proceedings - 2nd International Conference on Knowledge and Systems Engineering, KSE 2010 Số , năm 2010 (Tập , trang 194-200)

DOI: 10.1109/KSE.2010.29

Tài liệu thuộc danh mục: Scopus

Conference Paper


Từ khóa: Execution paths; Java PathFinder; Java program; Sequence diagrams; Test case; UML sequence diagrams; Computer software; Specifications; Systems engineering; Java programming language
Tóm tắt tiếng anh
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 PathFinder (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. � 2010 IEEE.

Xem chi tiết