An invariant-based method for the analysis of declarative model-to-model transformations

The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-540-87875-9_3Proceedings of 11th International Conference, MoDELS 2008, Toulouse, France, September 28 - October 3, 2008In this paper we propose a method to derive OCL invariants from declarative specifications of model-to-model transformations. In particular we consider two of the most prominent approaches for specifying 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 generation of valid pairs of source and target models.Work supported by the Spanish Ministry of Education and Science, projects MOSAIC (TSI2005-08225-C07-06), MODUWEB (TIN2006-09678) and TIN2005-06053, and an UOC-IN3 research gran