Model Checking Consistency of UML Diagrams Using Alloy

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.

• Akie Nimiya
• Tomoyuki Yokogawa
• Hisashi Miyazaki
• Sousuke Amasaki
• Yoichiro Sato
• Michiyoshi Hayase

• Model checking
• UML
• state machine diagrams
• communication diagram
• alloy.

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