Experimentation with a Big-Step Semantics for ATL Model Transformations

Formal semantics is a convenient tool to equip a model transformation language with precise meaning for its model transformations. Hence, clarifying their usage in complex scenarios and helping in the development of robust model transformation engines. In this paper, we focus on the formal specification of a model transformation engine for the declarative part of ATL. We present an implementation-agnostic, big-step, structural operational semantics for ATL transformation rules and a rule scheduler, which form the specification of an interpreter for ATL. Hence, avoiding a complex compilation phase. The resulting semantics for rules enjoys a compositional nature and we illustrate its advantages by reusing an interpreter for OCL. The semantics discussed has been validated with the implementation of an interpreter in Maude, enabling the execution of model transformations and their formal analysis using Maude’s toolkit. We also present an evaluation of the interpreter’s performance and scalability.