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

Authors: Yuka Kawakami, Tomoyuki Yokogawa, Hisashi Miyazaki, Sousuke Amasaki, Yoichiro Sato, Michiyoshi Hayase

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.

Keywords: UML, model checking, SMV, sequence diagram.

Digital Object Identifier (DOI): doi.org/10.5281/zenodo.1331113

References:

[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.