King's College London

Model transformation verification has been hindered by the
complex language mechanisms and semantics of mainstream
transformation languages. In this paper we describe an abstract
formalism, TL, for the definition of bidirectional and
unidirectional transformations in a purely declarative manner.
In contrast to model transformation languages such as
ATL or QVT-R, there is no implicit or explicit sequencing
of rules in TL specifications. Reasoning about TL specifications
is therefore facilitated. We show that semantics preserving
translations can be defined from TL to subsets
of the mainstream transformation languages.