In this paper we propose a method to derive OCL invariants from declar-
ative 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 transfor-
mation) 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.