Model transformations are key elements of model driven engineering. Current challenges for transformation languages include improving usability (i.e., succinct means to express the transformation intent) and devising powerful analysis methods.
In our recent paper (non-paywall version): Backwards reasoning for model transformations: Method and applications by Clariso, Cabot, Guerra and de Lara, part of the special issue to commemorate the 35th anniversary of Journal of Systems and Software (authors of the top ten most cited papers among those published in JSS each year between 2009 and 2013 were invited to submit their top-quality papers, 17 out of 42 were accepted) we show how backwards reasoning helps in both respects. The reasoning is based on a method that, given an OCL expression and a transformation rule, calculates a constraint that is satisfiable before the rule application if and only if the original OCL expression is satisfiable afterwards.
That is, given a constraint C that a model M must satisfy after the application of a rule r, the method generates the weakest constraint C′r such that if the model satisfies it before applying r, then the resulting model is guaranteed to satisfy C
With this method we can improve the usability of the rule execution process by automatically deriving suitable application conditions for a rule (or rule sequence) to guarantee that applying that rule does not break any integrity constraint (e.g. meta-model constraints). When combined with model finders, this method facilitates the validation, verification, testing and diagnosis of transformations, and we show several applications for both in-place and exogenous transformations, like checking weak and strong executability of a rule, rule applicability, white-box testing of rule sequences, deadlock analysis, rule independence among several others.
The computation of this “weakest precondition” is based on a set of syntax-driven replacement patterns that consider the list of modification actions performed by a rule to rewrite the constraint so that it can be equivalently verified before the execution of those actions takes place.