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.
Digital Object Identifier (DOI): doi.org/10.5281/zenodo.1331113Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 1178
 O. M. Group, Unified Modeling Language. Object Management Group, 2001, http://www.uml.org.
 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.
 B. Litvak, S. S. Tyszberowicz, and A. Yehudai, "Behavioral consistency validation of UML diagrams," in SEFM. IEEE Computer Society, 2003, pp. 118-125.
 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.
 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.
 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.
 K. McMillan, Symbolic Model Checking. Kluwer Academic, 1993.