In this paper we describe techniques for the specification and verification of model transformations using a combination of UML and formal methods. The use of UML 2 notations to specify model transfor- mations facilitates the integration of model transformations with other software development processes. Extracts from three large case studies of the specification of model transformations are given, to demonstrate the practical application of the approach.