Symbolic Model Checking of Interactions in Sequence Diagrams with Combined Fragments by SMV

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.

• Yuka Kawakami
• Tomoyuki Yokogawa
• Hisashi Miyazaki
• Sousuke Amasaki
• Yoichiro Sato
• Michiyoshi Hayase

• UML
• model checking
• SMV
• sequence diagram.

[1] O. M. Group, Unified Modeling Language. Object Management Group,
2001, http://www.uml.org.
[2] S. Bernardi, S. Donatelli, and J. Merseguer, "From uml sequence diagrams
and statecharts to analysable petrinet models," in Workshop on Software
and Performance, 2002, pp. 35-45.
[3] B. Litvak, S. S. Tyszberowicz, and A. Yehudai, "Behavioral consistency
validation of UML diagrams," in SEFM. IEEE Computer Society, 2003,
pp. 118-125.
[4] T. Sch¨afer, A. Knapp, and S. Merz, "Model checking uml state machines
and collaborations," Electr. Notes Theor. Comput. Sci., vol. 55, no. 3,
2001.
[5] X. Zhao, Q. Long, and Z. Qiu, "Model checking dynamic UML consistency,"
in ICFEM, ser. Lecture Notes in Computer Science, Z. Liu and
J. He, Eds., vol. 4260. Springer, 2006, pp. 440-459.
[6] S. Harada, T. Yokogawa, H. Miyazaki, Y. Sato, and M. Hayase, "A tool
support for verifying consistency between UML diagrams by SMV," in
ITC-CSCC, 2009, pp. 897-900.
[7] K. McMillan, Symbolic Model Checking. Kluwer Academic, 1993.