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.
Digital Object Identifier (DOI): doi.org/10.5281/zenodo.1333026Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 1229
 O. M. Group, Unified Modeling Language. Object Management Group, 2001, http://www.uml.org.
 K. McMillan, Symbolic Model Checking. Kluwer Academic, 1993.
 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.
 Alloy, http://alloy.mit.edu/.
 D. Jackson, Software Abstractions: Logic, Language,and Analysis. The MIT Press, 2006.
 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.
 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.
 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.