Formal verification techniques for model transformations specified by-demonstration
Abstract
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.