Checking Transformation Model Properties with a UML and OCL Model Validator.

This paper studies model transformations in the form of transformation models connecting source and target metamodels. We propose to analyze transformation models with a UML and OCL tool on the basis of an implementation of relational logic on top of Kodkod. Within this approach it is feasible to prove transformation model consistency, i.e., to automatically construct a valid metamodel model instance. Certain properties implied by the transformation model, e.g. whether a particular property is preserved by the transformation, can be inspected as well. As an example, the paper uses the well-known transformation between ER schemata and relational database schemata.