Towards a Rewriting Logic Semantics for ATL

As the complexity of model transformation (MT) grows, the need to count on formal semantics of MT languages also increases. Firstly, formal semantics provide precise specifications of the expected behavior of transformations, which are crucial for both MT users (to be able to understand them and to use them properly) and MT tool builders (to develop correct MT engines, optimizers, etc.). Secondly, we need to be able to reason about the MTs to prove their correctness. This is specially important in case of large and complex MTs (with, e.g., hundreds or thousands of rules) for which manual debugging is no longer possible. In this paper we present a formal semantics to the ATL model transformation language using rewriting logic and Maude, which allows addressing these issues. This formalization provides additional benefits, such as enabling the simulation of the specifications or giving access to the Maude toolkit to reason about them.