Verification and validation of declarative model-to-model transformations through invariants

In this paper we propose a method to derive OCL invariants from declarative model-to-model transformations in order to enable their verification and analysis. For this purpose we have defined a number of invariant-based verification properties which provide increasing degrees of confidence about transformation correctness, such as whether a rule (or the whole transformation) is satisfiable by some model, executable or total. We also provide some heuristics for generating meaningful scenarios that can be used to semi-automatically validate the transformations.As a proof of concept, the method is instantiated for two prominent model-to-model transformation languages: Triple Graph Grammars and QVT.