Model Checking Consistency of UML Diagrams Using Alloy

Authors: Akie Nimiya, Tomoyuki Yokogawa, Hisashi Miyazaki, Sousuke Amasaki, Yoichiro Sato, Michiyoshi Hayase

Abstract:

In this paper, we proposed a method for detecting consistency violation between UML state machine diagrams and communication diagrams using Alloy. Using input language of Alloy, the proposed method expresses system behaviors described by state machine diagrams, message sequences described by communication diagrams, and a consistency property. As a result of application for an example system, we confirmed that consistency violation could be detected using Alloy correctly.

Keywords: Model checking, UML, state machine diagrams, communication diagram, alloy.

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

References:

[1] O. M. Group, Unified Modeling Language. Object Management Group, 2001, http://www.uml.org.
[2] K. McMillan, Symbolic Model Checking. Kluwer Academic, 1993.
[3] 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.
[4] Alloy, http://alloy.mit.edu/.
[5] D. Jackson, Software Abstractions: Logic, Language,and Analysis. The MIT Press, 2006.
[6] A. J. H. Simons and C. A. F. y Fern'andez, "Using alloy to model-check visual design notations," in ENC. IEEE Computer Society, 2005, pp. 121-128.
[7] A. Zito and J. Dingel, "Modeling UML2 package merge with alloy," in 1st Alloy Workshop (Alloy -06), ser. Lecture Notes in Computer Science, O. Nierstrasz, J. Whittle, D. Harel, and G. Reggio, Eds., vol. 4199. Springer, 2006, pp. 86-95.
[8] T. Sch¨afer, A. Knapp, and S. Merz, "Model checking UML state machines and collaborations," Electronic Notes in Theoretical Computer Science, vol. 55, no. 3, pp. 357-369, 2001.