An Invariant-Based Method for the Analysis of Declarative Model-to-Model Transformations

Abstract. In this paper we propose a method to derive OCL invari-ants from declarative specifications of model-to-model transformations. In particular we consider two of the most prominent approaches for speci-fying such transformations: Triple Graph Grammars and QVT. Once the specification is expressed in the form of invariants, the transformation developer can use such description to verify properties of the original transformation (e.g. whether it defines a total, surjective or injective function), and to validate the transformation by the automatic genera-tion of valid pairs of source and target models.