Formal verification techniques for model transformations specified by-demonstration

Model transformations play an essential role in many aspects of model-driven development. By-demonstration approaches provide a user-friendly tool for specifying reusable model transformations. Here, a modeler performs the model transformation only once by hand and an executable transformation is automatically derived. Such a transformation is characterized by the set of pre- and postconditions that are required to be satisfied prior and after the execution of the transformation. However, the automatically derived conditions are usually too restrictive or incomplete and need to be refined manually to obtain the intended model transformation. As model transformations may be specified improperly despite the use of by-demonstration development approaches, we propose to employ formal verification techniques to detect inconsistent and erroneous transformations. In particular, we conjecture that methods drawn from software model checking and theorem proving might be employed to verify certain correctness properties of model transformations.