For Full-Text PDF, please login, if you are a member of IEICE,|
or go to Pay Per View on menu list, if you are a nonmember of IEICE.
Synthesis and Refinement Check of Sequence Diagrams
Hisashi MIYAZAKI Tomoyuki YOKOGAWA Sousuke AMASAKI Kazuma ASADA Yoichiro SATO
IEICE TRANSACTIONS on Information and Systems
Publication Date: 2012/09/01
Online ISSN: 1745-1361
Print ISSN: 0916-8532
Type of Manuscript: Special Section PAPER (Special Section on Software Reliability Engineering)
UML, sequence diagram, refinement, model checking, LTSA,
Full Text: PDF(530.5KB)>>
During a software development phase where a product is progressively elaborated, it is difficult to guarantee that the refined product retains its original behaviors. In this paper, we propose a method to detect refinement errors in UML sequence diagrams using LTSA (Labeled Transition System Analyzer). The method integrates multiple sequence diagrams using hMSC (high-level Message Sequence Charts) into a sequence diagram. Then, the method translates the diagram into FSP representation, which is the input language of LTSA. The method also supports some combined fragment operators in the UML 2.0 specification. We applied the method to some examples of refined sequence diagrams and checked the correctness of refinement. As a result, we confirmed the method can detect refinement errors in practical time.