doi: 10.4304/jsw.9.5.1229-1236
UML-Checker: An Approach for Verifying UML Behavioral Diagrams
- Computer Science Department, Pontifícia Universidade Católica de Minas Gerais Belo Horizonte, MG, Brazil
Abstract
UML is a visual modeling language used forspecifying, visualizing, constructing, and documentingsoftware artifacts. Despite having many features to modelsystems, conducting verifications and validations on UMLmodels is not an easy task. In this paper, the problem ofperforming verification of UML models is discussed througha translation of UML behavioral diagrams into formalmodels to be verified by a symbolic model checker. Anapproach and tool (UML checker) is presented in order toconduct verifications on UML diagrams. The main ideas are:(a) provide an approach to perform the translation ofactivity, state and use case diagrams to the formal inputlanguage of the NuSMV checker; (b) automate thetranslation of UML diagrams to a formal language; and (c)provide a set of predefined validations that are used tocheck the diagrams.
Keywords
- methods
- model checking
- UML behaviorald
How to Cite
Flávio Fernandes and Mark Song, "UML-Checker: An Approach for Verifying UML Behavioral Diagrams," Journal of Software, vol. 9, no. 5, pp. 1229-1236, 2014. https://doi.org/ 10.4304/jsw.9.5.1229-1236
Copyright & License
Copyright © 2014 by the authors. This is an open access article distributed under the Creative Commons Attribution License which permits unrestricted use, distribution, and reproduction in any medium, provided the original work is properly cited (CC BY 4.0).