WASET
	@article{(Open Science Index):https://publications.waset.org/pdf/3874,
	  title     = {Symbolic Model Checking of Interactions in Sequence Diagrams with Combined Fragments by SMV},
	  author    = {Yuka Kawakami and  Tomoyuki Yokogawa and  Hisashi Miyazaki and Sousuke Amasaki and  Yoichiro Sato and  Michiyoshi Hayase},
	  country	= {},
	  institution	= {},
	  abstract     = {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.
},
	    journal   = {International Journal of Computer and Information Engineering},
	  volume    = {4},
	  number    = {11},
	  year      = {2010},
	  pages     = {1692 - 1695},
	  ee        = {https://publications.waset.org/pdf/3874},
	  url   	= {https://publications.waset.org/vol/47},
	  bibsource = {https://publications.waset.org/},
	  issn  	= {eISSN: 1307-6892},
	  publisher = {World Academy of Science, Engineering and Technology},
	  index 	= {Open Science Index 47, 2010},
	}