@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}, }