F-Alloy: An Alloy Based Model Transformation Language

Model transformations are one of the core artifacts of a model-driven engineering approach. The relational logic language Alloy has been used in the past to verify properties of model transformations.
In this paper we introduce the concept of functional Alloy modules. In essence a functional Alloy module can be viewed as an Alloy module representing a model transformation.
We describe a sublanguage of Alloy called F-Alloy that allows the specification of functional Alloy modules. Modules in F-Alloy are analysable using the powerful automatic analysis features of Alloy but can also be interpreted efficiently without the use of backtracking.