%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 and Information Engineering
	%B World Academy of Science, Engineering and Technology
	%I Open Science Index 47, 2010
	%T Symbolic Model Checking of Interactions in Sequence Diagrams with Combined Fragments by SMV
	%U https://publications.waset.org/pdf/3874
	%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