Specifying the correctness properties of model transformations

The correctness of a model transformation is central to the success of a model-driven software development process. A transformation can be said to have executed correctly if it resulted in the desired output model, but this requires a specification of what constitutes a desirably correct output. If we have this specification, and a framework to verify that it holds on a specific execution of the transformation, then that execution instance may be "certified correct". In this paper, we explore a technique to specify such a correctness, using a language framework that can easily be incorporated into a variety of domains. We will also see how these correctness criteria can be verified on instance models.