Constraint-based specification of model transformations

Model transformations are a central element of model-driven development (MDD) approaches. The correctness, modularity and flexibility of model transformations is critical to their effective use in practical software development. In this paper we describe an approach for the automated derivation of correct-by-construction transformation implementations from high-level specifications. We illustrate this approach on a range of model transformation case studies of different kinds (re-expression, refinement, quality improvement and abstraction transformations) and describe ways in which transformations can be composed and evolved using this approach.