MCDL: A Language for Specifying Graph Conditions with Attribute Constraints

The offline analysis of graph rewriting-based model transformations, when only the definition of the transformation and the specification of the modeling languages are taken into account, have gained focus recently. In this case, the analysis must be performed only once, and the results are independent from the concrete input models. For the formal analysis, we need to formally define the properties that should be verified. This paper presents the outline of an automated offline verification framework. We propose a formal language to express the model properties that must be verified. On a case study of refactoring social network models, we demonstrate that our language is descriptive enough to specify the property classes that should be validated on the output models of the model transformations.