Consistency of model transformation contracts

Model-driven development is a generative software development process with increasing relevance both in industry and academia. Model transformations are the generative components in a model-driven development process. As such, their analysis is an important task. We have been developing a technique to specify, validate and implement model transformations. Our technique is based on the concept of transformation contracts, a specification that relates two modeling languages and declares properties that must be fulfilled in such a relation. Since a transformation contract is a model, the verification and validation of a transformation contract use the same techniques that are used to verify and validate any given model. This paper describes our technique, discusses consistency of model transformations and reports on its application to a non-trivial model transformation from access control models to Java security.