Yuka Kawakami and Tomoyuki Yokogawa and Hisashi Miyazaki and Sousuke Amasaki and Yoichiro Sato and Michiyoshi Hayase
Symbolic Model Checking of Interactions in Sequence Diagrams with Combined Fragments by SMV
1692 - 1695
2010
4
11
International Journal of Computer and Information Engineering
https://publications.waset.org/pdf/3874
https://publications.waset.org/vol/47
World Academy of Science, Engineering and Technology
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.
Open Science Index 47, 2010