My main interests in this area are the

1. Integration of graph transformation techniques in current mainstream UML/OCL modeling approaches.
2. Verification and validation of model transformations

So far we have presented two different methods (depending on the kind of model transformations employed: imperative or declarative):

1. Transformation of imperative graph transformation rules to OCL operation contracts (roughly, the precondition corresponds to the LHS of the rule, while the postcondition applies changes according to the RHS). The analysis of the OCL pre and postconditions allows to determine several correctness properties of the transformation as its applicability and weak and strong executability, among others. Results have been presented at the ICMT'08 Conf. (see this paper ) and published in this paper to appear in the Software and Systems Modeling Journal.
2. Transformation of declarative graph transformation rules (i.e. Triple graph grammars) and QVT relations to OCL invariants that restrict the possible relations between the source and target models. The analysis of the generated OCL invariants helps to determine several correctness properties of the rules and identify possible relevant validation scenarios. Results presented at the MODELS'08 Conf. (see this paper ) and published in this paper to appear in the Journal of Systems and Software.