Open Science Research Excellence
%0 Journal Article
%A Yuka Kawakami and  Tomoyuki Yokogawa and  Hisashi Miyazaki and Sousuke Amasaki and  Yoichiro Sato and  Michiyoshi Hayase
%D 2010 
%J  International Journal of Computer, Electrical, Automation, Control and Information Engineering
%B World Academy of Science, Engineering and Technology
%I International Science Index 47, 2010
%T Symbolic Model Checking of Interactions in Sequence Diagrams with Combined Fragments by SMV
%V 47
%X In this paper, we proposed a method for detecting consistency violation between state machine diagrams and a sequence diagram defined in UML 2.0 using SMV. We extended a method expressing these diagrams defined in UML 1.0 with boolean formulas so that it can express a sequence diagram with combined fragments introduced in UML 2.0. This extension made it possible to represent three types of combined fragment: alternative, option and parallel. As a result of experiment, we confirmed that the proposed method could detect consistency violation correctly with SMV.

%P 1692 - 1695