Synthesis and Refinement Check of Sequence Diagrams

Hisashi MIYAZAKI  Tomoyuki YOKOGAWA  Sousuke AMASAKI  Kazuma ASADA  Yoichiro SATO  

IEICE TRANSACTIONS on Information and Systems   Vol.E95-D   No.9   pp.2193-2201
Publication Date: 2012/09/01
Online ISSN: 1745-1361
DOI: 10.1587/transinf.E95.D.2193
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)>>
Buy this Article

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.