Using graph transformation and maude to simulate and verify UML models

UML is a standard language for object-oriented paradigm with an open notation and several concepts to be widely used in software modeling. However, the poorness of modeling languages to deal with simulation and verification has actuated researchers to use formal representations. Maude is the specification language of rewriting logic that allows simulation and verification of properties with its LTL model-checker. So, the transformation of UML models to Maude specification seems to be a good approach that deals with the limits of UML. The contribution of this paper is twofold. Firstly, we improved our graph grammar presented in a previous work by replacing it with two complementary graph grammars to generate more easily Maude specifications. Secondary, we performed the verification of some properties of the obtained formal Maude models using Maude LTL Model-checker. An illustrative example is presented.