A Rewriting Logic Semantics for ATL

Journal of Object Technology Published by AITO — Association Internationale pour les Technologies Objets, c JOT 2011 Online at http://www.jot.fm. A Rewriting Logic Semantics for ATL Javier TroyaaAntonio Vallecilloa a. GISUM/Atenea Research Group. Universidad de M´alaga, Spain. Abstract As the complexity of model transformation (MT) grows, the need to rely on formal semantics of MT languages becomes a critical issue. Formal semantics provide precise specifications of the expected behavior of transformations, allowing users to understand them and to use them properly, and MT tool builders to develop correct MT engines, compilers, etc. In addition, formal semantics allow modelers to reason about the MTs and to prove their correctness, something 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 give a formal semantics of the ATL 3.0 model transformation language using rewriting logic and Maude, which allows addressing these issues. Such formalization provides additional benefits, such as enabling the simulation of the specifications or giving access to the Maude toolkit to reason about them. Keywords ATL; Maude; Model Transformation; semantics. 1 Introduction Model transformations (MT) are at the heart of Model-Driven Engineering, and provide the essential mechanisms for manipulating and transforming models. As the complexity of model transformations grows, the need to rely on formal semantics of MT languages also increases. Formal semantics provide precise specifications of the expected behavior of the transformations, which are crucial for users to be able to understand and use model transformations properly, and for tool builders to develop correct model transformation engines, compilers, optimizers, debuggers, etc. Furthermore, MT programmers need to know the expected behavior of the rules and transformations they write, in order to reason about them and 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. For instance, in the case of rule-based model transformation languages, proving that the specifications are confluent and terminating is required. Also, looking for non-triggered rules may help detecting potential design problems in large MT systems. ATL [JABK08] is one of the most popular and widely used model transformation languages. As usual in the community, the ATL language has been described in an intuitive and informal manner, by means of definitions of its main features in natural Javier Troya, Antonio Vallecillo. A Rewriting Logic Semantics for ATL. In Journal of Object Technology, vol. 10, 2011, pages 5:1–29. doi:10.5381/jot.2011.10.1.a5 2·Javier Troya, Antonio Vallecillo Figure 1 – ATL model transformation schema. language. However, this lack of rigorous description can easily lead to imprecisions and misunderstandings that might hinder the proper usage and analysis of the language, and the development of correct and interoperable tools. The other reference implementation of ATL is available as metamodels for the language and its virtual machine, and as a compiler from the language to the virtual machine and an interpreter for the virtual machine. The problem of this kind of implementation is that it is not abstract enough to provide meaningful semantics, and in an implementationindependent manner. In this paper we investigate the use of rewriting logic [Mes92], and its implementation in Maude [CDE+07], for giving semantics to ATL. The use of Maude as a target semantic domain brings very interesting benefits, because it enables the simulation of the ATL specifications and the formal analysis of the ATL programs. In this sense, we provide a more abstract encoding than the ATL current implementation, together with an alternative specification of the transformations that can be simulated and analyzed for correctness. This paper is an extension of the one presented in the ICMT’10 conference [TV10a]. Here we deal with all new features of ATL version 3.0, and in particular we formalize the ATL refining mode — in addition to the ATL default execution semantics. Furthermore, we discuss some improvements in the Maude representation of the ATL rules to obtain better performance when simulating the ATL specifications. New ATL examples are also shown in this paper. The structure of the document is as follows. After this introduction, sections 2 and 3 provide an introduction to ATL and Maude, respectively. Then, section 4 presents how ATL language constructs can be encoded in Maude, and section 5 describes the current tool support. Finally, section 6 compares our work with other related proposals, and section 7 draws some conclusions and outlines some future research activities. 2 Transformations with ATL ATL is a hybrid model transformation language containing a mixture of declarative and imperative constructs. ATL transformations are unidirectional, operating on read-only source models and producing write-only target models (Fig. 1). During the execution of a transformation, source models may be navigated but changes are not allowed. Target models cannot be navigated. ATL modules define the transformations. A module contains a mandatory header Journal of Object Technology, vol. 10, 2011 A Rewriting Logic Semantics for ATL ·3 (a) Source metamodel. (b) Target metamodel. Figure 2 – Metamodels used in the example transformation. section, an import section, and a number of helpers and transformation rules. The header section provides the name of the transformation module and declares the source and target models (which are typed by their metamodels). Helpers and transformation rules are the constructs used to specify the transformation functionality. Declarative ATL rules are called matched rules and lazy rules. Lazy rules are like matched rules, but are only applied when called by another rule. They both specify relations between source patterns and target patterns. The source pattern of a rule specifies a set of source types and an optional guard given as a Boolean expression in OCL. A source pattern is evaluated to a set of matches in source models. The target pattern is composed of a set of elements. Each of these elements specifies a target type from the target metamodel and a set of bindings. A binding refers to a feature of the type (i.e., an attribute, a reference or an association end) and specifies an expression whose value is used to initialize the feature. Lazy rules can be called several times using a collect construct. Unique lazy rules are a special kind of lazy rules that always return the same target element for a given source element. The target element is retrieved by navigating the internal traceability links, as in normal rules. Non-unique lazy rules do not navigate the traceability links but create new target elements in each execution. In some cases, complex transformation algorithms may be required, and it may be difficult to specify them in a declarative way. For this reason ATL provides two imperative constructs: called rules and action blocks. A called rule is a rule called by others like a procedure. An action block is a sequence of imperative statements and can be used instead of or in combination with a target pattern in matched or called rules. The imperative statements in ATL are the usual constructs for attribute assignment and control flow: conditions and loops. ATL also provides the resolveTemp operation for dealing with complex transformations. This operation allows to refer to any of the target model elements generated from a given source model element: resolveTemp(srcObj,targetPatternName). The first argument is the source model element, and the second is a string with the name of the target pattern element. This operation can be called from the target pattern and imperative sections of any matched or called rule. ATL has two execution modes, the normal (default) execution mode and the refinJournal of Object Technology, vol. 10, 2011 4·Javier Troya, Antonio Vallecillo ing one. In the former, the ATL developer has to specify, either by matched or called rules, the way to generate each of the expected target model elements. This execution mode suits to most ATL transformations where source and target metamodels are different. Using the refining mode, ATL developers can define transformations that modify the source model to obtain the target model, since both models conform to the same metamodel. This mode is further explained in section 2.1. In order to illustrate our proposal for the ATL default execution mode we will use the example of JavaSource2Table model transformation [Ecl10], whose code is shown below. It has two matched rules, two lazy rules and two helpers. The complete description of this example and its encoding in Maude can be found in the technical report [TBV10]. Although the ATL rules are mostly self-explanatory, readers not fluent in ATL can also consult [JABK08, TV10b] for more details and examples. module JavaSource2Table; create OUT :Table from IN :JavaSource; helper def:allMethodDefs :Sequence(JavaSource!MethodDefinition) = JavaSource!MethodDefinition.allInstances() −>sortedBy(e|e.class.name +’_’ +e.name) −>asSequence() ; helper context JavaSource!MethodDefinition def :computeContent(col :JavaSource!MethodDefinition) : String = self.invocations −>select(i|i.method.name =col.name and i.method.class.name =col.class.name)−>size(); rule Main { from s:JavaSource!JavaSource to t:Table!Table ( rows <−Sequence{first_row,thisModule.allMethodDefs−> collect(e|thisModule.resolveTemp(e,’row’)) } ), first_row :Table!Row (cells <− Sequence{first_col,thisModule.allMethodDefs −>collect (e|thisModule.getContentFirstRow(e))}), first_col :Table!Cell (content <−’’) } rule MethodDefinition { from m:JavaSource!MethodDefinition to row :Table!Row (cells <−Sequence{title_cel,thisModule.allMethodDefs −> collect (e|thisModule.getComputeContent(m,e))}), title_cel :Table!Cell (content <−m.class.name +’.’ +m.name } lazy rule getContentFirstRow { from m:JavaSource!MethodDefinition to c:Table!Cell (content <−m.class.name +’.’ +m.name) } lazy rule getComputeContent{ from m1 :JavaSource!MethodDefinition, m2 :JavaSource!MethodDefinition to c:Table!Cell (content <−m1.computeContent(m2).toString() ) } The input model we have used in our transformations examples contains a JavaSource with two ClassDeclarations. It is shown in Fig. 3. Its corresponding target model when the JavaSource2Table transformation is applied over it is the Table model Journal of Object Technology, vol. 10, 2011 A Rewriting Logic Semantics for ATL ·5 Figure 3 –JavaSource input model. Figure 4 –Table target model. shown in Fig. 4. A visual explanation of how the transformation works is shown in Fig. 5. 2.1 ATL Refining Mode ATL also defines another execution mode, in case the transformation modifies the source model. This is the ATL refining mode, in which the transformation defines the elements that should be changed and how. The rest of the elements in the model are implicitly copied by the ATL engine without modifications. In the 2004 version of ATL, the copying was performed implicitly only for contained elements of copied elements, and it was mandatory to specify all bindings. The effort of copying some elements of a transformation, while modifying others, was reduced in the next version of the ATL language in 2006, which introduced some changes to the refining mode. In this new version every element stays unchanged if it is not explicitly matched by any of the transformation rules. However, the 2006 version did not provide support for the deletion of elements. The new ATL 2010 compiler implements a full in-place strategy, where elements can be deleted by the rules, and also reverse bindings for the first output pattern element are supported. Transformations in this mode are performed in two steps. In the first step, the transformation engine executes the rules which, as a result, produce a set of changes that is temporarily stored. In the second step, this set of changes is applied directly on the source model. Deletion is possible using the “drop” keyword in the to pattern. Let us illustrate this execution mode using the well-known example of the Public2Private transformation, which makes all public attributes of a UML model private. Getters and setters are also created appropriately, as shown below. module Public2Private; create OUT :UML refining IN :UML; helper context String def :toU1Case :String = self.substring(1,1).toUpper() + self.substring(2,self.size()); rule Property { from publicAttribute : Journal of Object Technology, vol. 10, 2011 6·Javier Troya, Antonio Vallecillo Figure 5 – Visual explanation of the transformation. UML!Property (publicAttribute.visibility = #public) to privateAttribute : UML!Property (visibility <−#private), getter :UML!Operation (name <−’get’+publicAttribute.name.toU1Case, class <−publicAttribute.refImmediateComposite(), type <−publicAttribute.type), setter :UML!Operation (name <−’set’+publicAttribute.name.toU1Case, class <−publicAttribute.refImmediateComposite(), ownedParameter <−setterParam), setterParam :UML!Parameter (name <−publicAttribute.name, type <−publicAttribute.type)} Detailed information about this transformation can be found in [Ecl10]. The reference metamodel is a simplification of the UML metamodel with only the relevant information for this example, and is shown in Fig. 6. 3 Rewriting Logic and Maude Maude [CDE+07] is a high-level language and a high-performance interpreter in the OBJ algebraic specification family that supports membership equational logic [BJM00] and rewriting logic [Mes92] specification and programming of systems. Thus, Maude integrates an equational style of functional programming with rewriting logic computation. We informally describe in this section those Maude’s features necessary for understanding the paper; the interested reader is referred to [CDE+07] for more details. Rewriting logic is a logic of change that can naturally deal with state and with highly nondeterministic concurrent computations. A system is axiomatized in rewritJournal of Object Technology, vol. 10, 2011 A Rewriting Logic Semantics for ATL ·7 Figure 6 – Metamodel used in the Public2Private transformation. ing logic by a rewrite theory R= (Σ,E,R), where (Σ,E) is an equational theory describing its set of states as the algebraic data type TΣ/Eassociated to the initial algebra (Σ,E), and Ris a collection of rewrite rules. Maude’s underlying equational logic is membership equational logic [BJM00], a Horn logic whose atomic sentences are equalities t=t0and membership assertions of the form t:S, stating that a term thas sort S. Such a logic extends order-sorted equational logic, and supports sorts, subsort relations, subsort overloading of operators, and definition of partial functions with equationally defined domains. Rewrite rules, which are written crl [l] : t=>t0if Cond, with lthe rule label, t and t0terms, and Cond a condition, describe the local, concurrent transitions that are possible in the system, i.e., when a part of the system state fits the pattern t, then it can be replaced by the corresponding instantiation of t0. The guard Cond acts as a blocking precondition, in the sense that a conditional rule can be fired only if its condition holds. A condition is written EqCond1/\ ... /\ EqCondnwhere each of the EqCondi is either an ordinary equation t=t0, a matching equation t := t0, a sort constraint t:s, or a term tof sort Bool, abbreviating the equation t= true. In the execution of a matching equation t:= t0, the variables of the term t, which may not appear in the left hand side of the corresponding conditional equation, become instantiated by matching the term tagainst the canonical form of the bounded subject term t0. 4 Encoding ATL in Maude To give a formal semantics to ATL using rewriting logic, we provide a representation of the ATL constructs and of their behavior in Maude. We start by defining how the models and metamodels handled by ATL can be encoded in Maude, and then we provide the semantics of matched rules, lazy rules, unique lazy rules, helpers, imperative sections, the resolveTemp function and the refining execution mode. One of the benefits of such an encoding is that it is systematic and can be automated, something we are currently implementing using ATL transformations (between the ATL and Maude metamodels). Journal of Object Technology, vol. 10, 2011 8·Javier Troya, Antonio Vallecillo Figure 7 – Elements of a relation R(M,N). 4.1 Characterizing Model Transformations In our view, a model transformation is just an algorithmic specification (let it be declarative or operational) associated to a relation R⊆MMS×MMTdefined between two metamodels which allows to obtain a target model MTconforming to MMT from a source model MSthat conforms to metamodel MMS[Ste07]. In the most general case, a model transformation can be defined between multiple source and target metamodels. In this case MMSand MMTrepresent sets of metamodels. The idea supporting our proposal considers that model transformations combine two different aspects: structure and behavior. The former aspect defines the structural relation Rthat should hold between source and target models, whilst the latter describes how the specific source model elements are transformed into target model elements. This separation allows differentiating between the relation that the model transformation ensures from the algorithm it actually uses to compute the target model. Thus, to represent the structural aspects of a transformation we will use three models: the source model MS, the target model MTthat the transformation builds, and the relation R(MS,MT) between the two. R(MS,MT) is also called the trace model, that specifies how the elements of MSand MTare consistently related by R. Please note that each element riof R(MS,MT) = {r1, ..., rk} ⊆ P(MS)×P(MT) relates a set of elements of MSwith a set of elements of MT(see Fig. 7). The behavioral aspects of an ATL transformation (i.e., how the transformation progressively builds the target model elements from the source model, and the traces between them) is defined using the different kinds of rules (matched, lazy, unique lazy); their possible combinations and direct invocation from other rules, and the final imperative algorithms that can be invoked after each rule. 4.2 Encoding Models and Metamodels in Maude We will follow the representation of models and metamodels introduced in [RVD09], which is inspired by the Maude representation of object-oriented systems. We represent models in Maude as structures of sort @Model of the form mm{obj1obj2... objN}, where mm is the name of the metamodel and objiare the objects of the model. An object is a record-like structure <o:c|a1:v1, ..., an:vn>(of sort @Object), where ois the object identifier (of sort Oid), cis the class the object belongs to (of sort Journal of Object Technology, vol. 10, 2011 A Rewriting Logic Semantics for ATL ·9 @Class), and ai:viare attribute-value pairs (of sort @StructuralFeatureInstance). Given the appropriate definitions for all classes, attributes and references in its corresponding metamodel (as we shall see below), the following Maude term describes the input model shown in section 2. @javasourcemm@ { <’s:JavaSource@javasourcemm | classes@JavaSource@javasourcemm :Sequence[ ’c1 ; ’c2 ]> <’c1 :ClassDeclaration@javasourcemm | name@NamedElement@javasourcemm :"FirstClass" # methods@ClassDeclaration@javasourcemm :Sequence[ ’m1 ; ’m2 ]> <’m1 :MethodDefinition@javasourcemm | name@NamedElement@javasourcemm :"fc_m1" # invocations@MethodDefinition@javasourcemm :null # class@MethodDefinition@javasourcemm : ’c1 > <’m2 :MethodDefinition@javasourcemm | name@NamedElement@javasourcemm :"fc_m2" # invocations@MethodDefinition@javasourcemm :Sequence [ ’i1 ; ’i1 ] # class@MethodDefinition@javasourcemm : ’c1 > <’i1 :MethodInvocation@javasourcemm | method@MethodInvocation@javasourcemm : ’m1 > <’c2 :ClassDeclaration@javasourcemm | name@NamedElement@javasourcemm :"SecondClass" # methods@ClassDeclaration@javasourcemm :Sequence [ ’m3 ; ’m4 ]> <’m3 :MethodDefinition@javasourcemm | name@NamedElement@javasourcemm :"sc_m1" # invocations@MethodDefinition@javasourcemm : ’i2 # class@MethodDefinition@javasourcemm : ’c2 > <’i2 :MethodInvocation@javasourcemm | method@MethodInvocation@javasourcemm : ’m1 > <’m4 :MethodDefinition@javasourcemm | name@NamedElement@javasourcemm :"sc_m2" # invocations@MethodDefinition@javasourcemm : ’i3 # class@MethodDefinition@javasourcemm : ’c2 > <’i3 :MethodInvocation@javasourcemm | method@MethodInvocation@javasourcemm : ’m3 > } Note that quoted identifiers are used as object identifiers; references are encoded as object attributes by means of object identifiers; and OCL collections (Set,OrderedSet, Sequence, and Bag) are supported by means of mOdCL [RD08]. Metamodels are encoded using a sort for every metamodel element: sort @Class for classes, sort @Attribute for attributes, sort @Reference for references, etc. Thus, a metamodel is represented by declaring a constant of the corresponding sort for each metamodel element. Thus, each class is represented by a constant of a sort named after the class. This sort, which will be declared as subsort of sort @Class, is defined to support class inheritance through Maude’s order-sorted type structure. Other properties of metamodel elements, such as whether a class is abstract or not, the opposite of a reference (to represent bidirectional associations), or attributes and reference types, are expressed by means of Maude equations. Classes, attributes and references are qualified with their containers’ names, so that classes with the same name belonging to different packages, as well as attributes and references of different classes, are distinguished. See [RVD09] for further details. Journal of Object Technology, vol. 10, 2011 16 ·Javier Troya, Antonio Vallecillo cell2 :Table!Cell(content <−’SecondCell’), cell3 :Table!Cell(content <−’ThirdCell’) do{ cell1.content <−cell1.content +’_assignment’; if (row.cells −>size() = 3) { cell2.content <−’Condition_satisfied’; }else { cell2.content <−’Condition_not_satisfied’; } for (i in row.cells){ i.content <−i.content +’_assign_for’; if (i.content =’ThirdCell_assign_for’){ i.content <−i.content +’_if_for_satisfied’; }else { i.content <−i.content +’_if_for_not_satisfied’; } i.content <−i.content +’_after_if_for’; } thisModule.NewTable(’NewTable’); } } The corresponding encoding in Maude is as follows: crl[Main] : Sequence[...] => Sequence[... (@Tablemm@ {do ( <T@ :Table@tablemm |rows@Table@tablemm :R@ > <R@ :Row@tablemm |cells@Row@tablemm :Sequence [C1@ ;C2@ ;C3@ ]> <C1@ :Cell@tablemm |content@Cell@tablemm :"FirstCell" > <C2@ :Cell@tablemm |content@Cell@tablemm :"SecondCell" > <C3@ :Cell@tablemm |content@Cell@tablemm :"ThirdCell" >, Assign(C1@,content@Cell@tablemm, << C1@ .content@Cell@tablemm ;TABLEMODEL@ >> +"_assignment") ˆ If(<< Sequence[C1@ ;C2@ ;C3@]−>size() ; JAVASOURCEMODEL@ >> == 3, Assign(C2@,content@Cell@tablemm,"Condition_satisfied"), Assign(C2@,content@Cell@tablemm,"Condition_not_satisfied")) ˆ --- endIf For(<< R@ .cells@Row@tablemm ;TABLEMODEL2@ >>, AssignAttFor(content@Cell@tablemm,content@Cell@tablemm,TABLEMODEL2@, "_assign_for") ˆ IfFor("==",content@Cell@tablemm,"ThirdCell_assign_for",TABLEMODEL3@, AssignAttFor(content@Cell@tablemm,content@Cell@tablemm,TABLEMODEL3@, "_if_for_satisfied"), AssignAttFor(content@Cell@tablemm,content@Cell@tablemm,TABLEMODEL3@, "_if_for_not_satisfied") ) ˆ --- endIfFor AssignAttFor(content@Cell@tablemm,content@Cell@tablemm,TABLEMODEL4@, "_after_if_for") ) ˆ --- endFor NewTable(VALUE@CNT@ + 6, "NewTable")) OBJSETTT@ } ) ]if... The first argument of function do is the set of objects created in the declarative part of the rule. Consequently, we enforce the declarative part of the rule to be Journal of Object Technology, vol. 10, 2011 A Rewriting Logic Semantics for ATL ·17 Figure 8 – Trace class. executed before the imperative part. This is the way in which ATL works. The second argument is a sequence of instructions. It contains, in this case, four instructions. The first instruction executed is an Assign. Then, an If block with two assignments inside is executed. After this, a For instruction, containing three instructions (two assignments and a if block), is executed. Finally, the instruction that represents the called rule, NewTable, is executed. 4.3.6 ResolveTemp The resolveTemp function looks for the trace that contains the source element passed as first argument, and returns the identifier of the element from the sequence of elements created from the source element. Its representation in Maude is as follows: op resolveTemp :Oid Nat @Model @Model −>Oid . eq resolveTemp(O@ ,N@ ,@TraceMm@{<TR@ :Trace@TraceMm |srcEl@TraceMm : Sequence[O@] # trgEl@TraceMm :SEQ #SFS >OBJSET},SOURCEMODEL@ ) = if (<< SEQ −>size ( ) <N@ ;SOURCEMODEL@ >>)then null else << SEQ −>at(N@) ; SOURCEMODEL@ >> fi. It has four arguments: the identifier of the source model element from which the searched target model element is produced; the position of the target object identifier in the sequence trgEl@TraceMm; and the trace and class models, respectively. It returns the identifier of the element to be retrieved. The major difference with the ATL function is that here we receive as second argument the position that the searched target model element has among the ones created by the corresponding rule. In ATL, instead, the argument received is the name of the variable that was given to the target model element when it was created. This deviation from ATL is merely due to technical reasons: we do not use variable names in this function because we do not store variable names in traces. A trace contains a sequence with the identifiers of the target elements that were created from the source elements. As it is a sequence, it is ordered and, consequently, every element identifier has a position within the sequence. Therefore, the difference of passing as argument the position of the element identifier in the sequence instead of the variable name is not significant since it is easy to retrieve the position of the element among those created by the ATL rule. 4.4 ATL refining mode in Maude As explained in section 2.1, the ATL refining execution mode transforms the elements identified by the source patterns according to the behaviour defined in the rules. Those model elements that are not explicitly affected by the rules (either directly or indirectly) remain unchanged. Journal of Object Technology, vol. 10, 2011 18 ·Javier Troya, Antonio Vallecillo The semantics of this ATL execution mode can be specified in Maude in a similar way to the one used to specify the normal execution mode. However, the traces will be treated in a slightly different manner, because we do not need to specify and maintain traces between elements that have not been modified by the transformation. In fact, traces in this execution mode can be considered as model differences between the elements of both models: the old and new versions of the model being transformed. Thus, we have defined each trace as an instance of the class shown in Fig. 8, which follows the approach used in [RV08]. Traces of type modified represent the transformation of an object from the source model into another object in the target model where at least one of its attributes (or references) have been modified. Traces whose type is added, in turn, represent the addition of a new object (or more than one) in the target model. In the 2010 implementation of the refining mode, ATL allows to remove objects. To represent this new feature we have traces of type deleted, whose source elements (srcEl) are the deleted objects, and the set of target elements (trgEl) is empty. A Maude rule that represents an ATL rule where objects are deleted simply contains these objects in its left hand side, but not in its right hand side, and it creates a trace of type deleted as mentioned above. In the encoding of a transformation in refining mode in Maude, the Init rule is also different, since now the source model is copied into the target one. Thus, in case of the Public2Private example introduced in section 2.1, this rule is as follows: rl [Init] : Sequence[(@UMLSimpMm@ {OBJSET@ })] => Sequence[(@UMLSimpMm@ {OBJSET@ }) ; (@TraceMm@ {<’CNT :Counter@CounterMm |value@Counter@CounterMm : 1 >}) ; (@UMLSimpMm@ {OBJSET@ })] . After the application of this rule, both the source and target models contain the same elements. Then, the target model is modified as the ATL matched rules are executed, “navigating” the source model. Models navigability and in-place transformations The ATL documentation [Gro06] states that, both in normal and in refining execution modes, source models are read-only and target models are write-only. This means that only source models can be navigated and, therefore, the state of the target model does not affect the behavior of the transformation. This is an important detail that significantly affects the way in which ATL works in refining mode. In fact, it is a common mistake to confuse the behavior of the ATL refining mode with the typical behavior of the in-place transformations used by most rewriting systems, including graph grammars or even Maude rules. In these rewriting systems, a set of rules modifies the state of a configuration of objects (i.e., a model) one by one. Thus, after the application of each rule the state of the system is changed, and subsequent rules will be applied on the system on this new state. In this way, the target model after the application of one rule becomes the source model in the next step. In other words, the transformation navigates the target model, which is continuously updated by every executed rule. However, this is not the way in which the ATL refining mode works. In ATL the rules always read (i.e., navigate) the state of the source model, which remains unchanged during all the transformation execution. This is the approach we have followed in our representation in Maude, too. Journal of Object Technology, vol. 10, 2011 A Rewriting Logic Semantics for ATL ·19 Figure 9 – In-place behavior: navigability on the target model. In order to illustrate this difference, let us go back to the Public2Private transformation and imagine that we add another matched rule that changes all private Properties, capitalizing the first letter of their names. Let us call this rule Private2Capital. If ATL worked in a pure in-place manner (i.e., navigating the target model), the transformation would change the names of all properties: all of them will end up being private and with the first letter of their names in capitals (see the example shown in Fig. 9). However, the ATL refining mode navigates the source model. This means that, at the end of the execution of the Public2Private transformation, only those properties that were originally private in the source model will have their names capitalized, while the original public properties in the model will be transformed into private properties but their names will not be changed (see Fig. 10). 5 Simulation and Formal Analysis Once the ATL model transformation specifications are encoded in Maude, what we get is a rewriting logic specification for it. Maude offers tool support for interesting possibilities such as model simulation, reachability analysis and model checking [CDE+07]. Journal of Object Technology, vol. 10, 2011 20 ·Javier Troya, Antonio Vallecillo Figure 10 – ATL refining mode: navigability always on the source model. 5.1 Simulating the transformations Because the rewriting logic specifications produced are executable, this specification can be used as a prototype of the transformation, which allows us to simulate it. Maude offers different possibilities for performing the simulation, including step-bystep execution, several execution strategies, etc. In particular, Maude provides two different rewrite commands, namely rewrite and frewrite, which implement two different execution strategies, a top-down rule-fair strategy, and a depth-first position-fair strategy, respectively [CDE+07]. The result of the process is the final configuration of objects reached after the rewriting steps, which is nothing but a model. For example, the JavaSource2Table ATL model transformation described in section 2, when executed in default mode over the JavaSource source model shown in Fig. 3, results in a sequence of three models: the source, the trace and the target model. The encoding in Maude of this last one, which conforms to the Table metamodel and is displayed in Fig. 4, is shown below. @JavaSourceMm@ { <’s:JavaSource@javasourcemm | classes@JavaSource@javasourcemm :Sequence[ ’c1 ; ’c2 ]> <’c1 :ClassDeclaration@javasourcemm | name@NamedElement@javasourcemm :"FirstClass" # Journal of Object Technology, vol. 10, 2011 A Rewriting Logic Semantics for ATL ·21 methods@ClassDeclaration@javasourcemm :Sequence[ ’m1 ; ’m2 ]> <’m1 :MethodDefinition@javasourcemm | name@NamedElement@javasourcemm :"fc_m1" # invocations@MethodDefinition@javasourcemm :null # class@MethodDefinition@javasourcemm : ’c1 > <’m2 :MethodDefinition@javasourcemm | name@NamedElement@javasourcemm :"fc_m2" # invocations@MethodDefinition@javasourcemm :Sequence [ ’i1 ; ’i1 ] # class@MethodDefinition@javasourcemm : ’c1 > <’i1 :MethodInvocation@javasourcemm | method@MethodInvocation@javasourcemm : ’m1 > <’c2 :ClassDeclaration@javasourcemm | name@NamedElement@javasourcemm :"SecondClass" # methods@ClassDeclaration@javasourcemm :Sequence [ ’m3 ; ’m4 ]> <’m3 :MethodDefinition@javasourcemm | name@NamedElement@javasourcemm :"sc_m1" # invocations@MethodDefinition@javasourcemm : ’i2 # class@MethodDefinition@javasourcemm : ’c2 > <’i2 :MethodInvocation@javasourcemm | method@MethodInvocation@javasourcemm : ’m1 > <’m4 :MethodDefinition@javasourcemm | name@NamedElement@javasourcemm :"sc_m2" # invocations@MethodDefinition@javasourcemm : ’i3 # class@MethodDefinition@javasourcemm : ’c2 > <’i3 :MethodInvocation@javasourcemm | method@MethodInvocation@javasourcemm : ’m3 >} Although the Maude specifications can be used for running the ATL transformations, and not only for simulating it, the performance of the Maude specifications is not comparable with ATL (see Section 5.4). However, our proposal does not try to compete with ATL in this respect. It is not the goal of this work to use Maude for implementing model transformations, but for providing semantics to ATL. The fact that Maude specifications are executable gives us an implementation of the transformation, but such an implementation is not intended to be used as an alternative to ATL in practice—just for verification purposes. 5.2 Reachability analysis Executing the system using the rewrite and frewrite commands means exploring just one possible behavior of the system. However, a rewrite system does not need to be Church-Rosser and terminating,2and there might be many different execution paths. Although these commands are enough in many practical situations where an execution path is sufficient for testing executability, the user might be interested in exploring all possible execution paths from the starting model, a subset of these, or a specific one. Maude search command allows us to explore (following a breadthfirst strategy up to a specified bound) the reachable state space in different ways, looking for certain states of special interest. Other possibilities would include searching for any state 2For membership equational logic specifications, being Church-Rosser and terminating means not only confluence (a unique normal form will be reached) but also a sort decreasingness property, namely that the normal form will have the least possible sort among those of all other equivalent terms. Journal of Object Technology, vol. 10, 2011 22 ·Javier Troya, Antonio Vallecillo (given by a model) in the execution tree, let it be final or not. For example, we could be interested in knowing the partial order in which two ATL matched rules are executed, checking that one always occurs before the other. This can be proved by searching for states that contain the second one in the trace model, but not the first. 5.3 Checking other properties After the simulation is completed, it is also possible to analyze the trace model looking for instance for rules that have not been executed, or for obtaining the traces (and source model elements) related to a particular target model element (or viceversa). Although this could also be done in any transformation language that makes the trace model explicit, the advantages of using our encoding in Maude is that these operations become easy to specify because of Maude’s facilities for manipulating sets using order-sorted unification modulo associativity and commutativity: op getSourceElements :@Model Oid −>Sequence . eq getSourceElements(@TraceMm@{<TR@ :Trace@TraceMm |srcEl@TraceMm : SEQ #trgEl@TraceMm :Sequence[O@ ;LO] # SFS >OBJSET},O@) = SEQ . eq getSourceElements(@TraceMm@{<TR@ :Trace@TraceMm |srcEl@TraceMm : SEQ #trgEl@TraceMm :Sequence[T@ ;LO] # SFS >OBJSET},O@) =getSourceElements(@TraceMm@{<TR@ :Trace@TraceMm |srcEl@TraceMm : SEQ #trgEl@TraceMm :Sequence[LO] # SFS >OBJSET},O@) . eq getSourceElements(@TraceMm@{OBJSET},O@) = Sequence[mt−ord] [owise] . We can also use a similar operation to traverse the trace model and check that every source element has been transformed by at most one ATL match rule. In fact, in ATL only one matched rule can be applied on a given model element (this ensures some kind of confluence of the ATL rules, too). In general there are two ways of dealing with such constraints, depending on whether we want the Maude rules to enforce them during their execution or not. In the first case these constraints will be added to the Maude rules. In the second case the mapping to Maude will not consider them, so these situations will occur if they happen in the ATL code. But we will be able to check them once the transformation is done by exploring the trace model, as mentioned above. For example, to check that no more than one ATL rule is applied over a single source element we have defined the singleApplicability operation: op singleApplicability :OCL−Exp String @Model Int −>@Object . eq singleApplicability(SR@,NAME,@TraceMm@ {<TR@ :Trace@TraceMm | srcEl@TraceMm :Sequence[SR@ ;LO] # rlName@TraceMm :NAME’ # SFS >OBJSET}, VALUE@CNT@) = if NAME =/= NAME’then <newId(VALUE@CNT@) : TraceSA@TraceMm |rl1Name@TraceMm :NAME # rl2Name@TraceMm :NAME’ # srcEl@TraceMm :SR@ #errMsg@TraceMm :"Rules " + NAME +" and " +NAME’ + " are applied over the same source element: " + SR@ > else singleApplicability(SR@,NAME,@TraceMm@ {<TR@ :Trace@TraceMm | srcEl@TraceMm :Sequence[LO] # rlName@TraceMm :NAME’ # SFS >OBJSET}, VALUE@CNT@) fi. eq singleApplicability(SR@,NAME,TRACEMODEL@,VALUE@CNT@) = none [owise] . This operation receives as arguments a source model element, a string with the name of the rule from which the function is called, the trace model and the counter Journal of Object Technology, vol. 10, 2011 A Rewriting Logic Semantics for ATL ·23 to create new identifiers. The function looks for a trace created by a different rule (we check that the names of the rules are different: NAME =/= NAME’) where the element received as argument is present in the srcEl@TraceMm part. The problem, as usual, is what to do when a problem is encountered during the execution of the rule. In this case our encoding generates a special kind of trace (TraceSA@TraceMm), which captures every error found. Such traces store the problematic rule names (those whose left hand side parts contain the same source model element), the source model element and an error message. As an example of how this function is called, we add a call to it in the MethodDefinition matched rule that we presented above. We can see the call in the next listing: crl[MethodDefinition] : Sequence[ (@JavaSourcemm@ {<M@ :MethodDefinition@javasourcemm |SFS >OBJSET@ }) ; (@TraceMm@ {<CNT@ :Counter@CounterMm |value@Counter@CounterMm :VALUE@CNT@> OBJSETT@ }) ; (@Tablemm@ {OBJSETTT@ }) ] =>Sequence[ (@JavaSourcemm@ {<M@ :MethodDefinition@javasourcemm |SFS >OBJSET@ }) ; (@TraceMm@ { <CNT@ :Counter@CounterMm |value@Counter@CounterMm :VALUE@CNT@ + 4 > ... singleApplicability(M@,"MethodDefinition",@TraceMm@{OBJSETT@},VALUE@CNT@) OBJSETT@}) ; (@Tablemm@ {... }) ] if JAVASOURCEMODEL@ := ... /\TR@ := newId(VALUE@CNT@ + 1) /\R@ := newId(VALUE@CNT@ + 2) /\TC@ := newId(VALUE@CNT@ + 3) /\ /\not alreadyExecuted(Sequence[M@],"MethodDefinition",@TraceMm@ {OBJSETT@ }). 5.4 Questions of efficiency Another improvement over the proposal presented in [TV10a] is the use of a more compact encoding of the Maude representation of the ATL rules. Maude is a very expressive language, which allows many different ways to represent the same concepts or the same behaviors. Each encoding, although functionally and semantically equivalent, may be different regarding other non-functional aspects such as performance, readability or understandability, among others. In the previous sections we have shown the encoding that was also used in [TV10a]. This encoding is rather natural (to the Maude users) and convenient for representing the behavior of ATL constructs and rules. However, when it comes to simulating and analyzing the specifications, it may be significantly improved in several ways. The aim of the modifications is to remove as many guards as possible from the Maude rules, so that the rewrite process does not need to evaluate conditions for triggering them. Thus, we have avoided the use of auxiliary variables that were declared as guards with the “:=” operator by replacing them with their corresponding expressions in the places where these auxiliary variables were used. We have also got rid of the AlreadyExecuted function, which had to navigate the trace model in each rule invocation, by introducing an auxiliary model in the Maude rules that contains the elements from the input model that have not yet been transformed by ATL rules. Journal of Object Technology, vol. 10, 2011 24 ·Javier Troya, Antonio Vallecillo Original Optimized encoding encoding ATL 125 Classes, 500 Attributes 15” 4” 0.3” 250 Classes, 1000 Attributes 1’37” 15” 0.5” 375 Classes, 1500 Attributes 5’53” 40” 0.8” 500 Classes, 2000 Attributes 16’09” 1’37” 1.1” 750 Classes, 3000 Attributes 58’28” 4’02” 2” 1250 Classes, 5000 Attributes 3h16’49” 16’37” 3” 2000 Classes, 8000 Attributes 17h57’15” 1h04’19” 5” Table 1 – Comparative performance figures. This new model initially coincides with the input model of the transformation and, when a rule is executed on a set of elements, these elements are removed from the model. We have removed the evaluation of some OCL expressions in the conditions of the Maude rules by checking them in the input model. We have also tried to avoid the use of OCL expressions in the right hand side of Maude rules when initializing objects attributes in the target model by specifying variables for the values of the objects’ attributes in the input model. Please refer to [TBV10] for a complete description of the performed modifications. This alternative encoding provides significant improvements in efficiency and performance, as shown in Table 1 for the ATL Class2Relational transformation [TV10a]. Still, it is not comparable to the performance of the equivalent ATL transformation (shown in the last column). The problem is that the new Maude encoding is much more verbose and less easy to read and understand. However, this new encoding can be automatically obtained from the previous one, hence allowing an automatic transformation from one to the other. This is why we have detailed here the original encoding, because it is functionally equivalent and much easier to read and understand. 6 Related Work The definition of a formal semantics for ATL has received attention by different groups, using different approaches. For example, in [dRJK+06] the authors propose an extension of AMMA, the ATLAS Model Management Architecture, to specify the dynamic semantics of a wide range of Domain Specific Languages by means of Abstract State Machines (ASMs), and present a case study where the semantics of part of ATL (namely, matched rules) are formalized. Although ASMs are very expressive, the declarative nature of ATL does not help providing formal semantics to the complete ATL language in this formalism, hindering the complete formalization of the language—something that we were pursuing with our approach. Other works [BS06, ABK07] have proposed the use of Alloy to formalize and analyze graph transformation systems, and in particular ATL. These analysis include checking the reachability of given configurations of the host graph through a finite sequence of steps (invocations of rules), and verifying whether given sequences of rules can be applied on an initial graph. These analysis are also possible with our approach, and we also obtain significant gains in expressiveness and completeness. The problem Journal of Object Technology, vol. 10, 2011 A Rewriting Logic Semantics for ATL ·25 is that Alloy expressiveness and analysis capabilities are quite limited [ABK07]: it has a simple type system with only integers; models in Alloy are static, and thus the approach presented in [ABK07] can only be used to reason about static properties of the transformations (for example it is not possible to reason whether applying a rule r1before a rule r2in a model will have the same effect as applying r2before r1); only ATL declarative rules are considered, etc. In our approach we can deal with all the ATL language constructs without having to abstract away essential parts such as the imperative section, basic types, etc. More kinds of analysis are also possible with our approach. Other works provide formal semantics to model transformation languages using types. For intance, Poernomo [Poe08] uses Constructive Type Theory (CTT) for formalizing model transformation and proving their correctness with respect to a given preand post-condition specification. This approach relies on a simple encoding of MetaClasses as mixed inductive/co-inductive structured types which the current proof assistant does not handle well due to structural guard constraints for co-inductive definitions [PM10]. Alternative approaches encode models as graph covering trees and additional links [GS10, GSMP11] or as a classical mathematical graphs relying on nodes and relations between nodes [TCCG07]. These approaches can be considered as complementary to ours, each one focusing on different aspects. There are also the early works in the graph grammar community with a logic-based definition and formalization of graph transformation systems. For example, Courcelle [Cou97] proposes a combination of graph grammars with second order monadic logic to study graph properties and their transformations. Sch¨urr [SWZ99] has also studied the formal specification of the semantics of the graph transformation language PROGRES by translating it into some sort of non-monotonic logics. A different line of work proposed in [BHM09] defines a QVT-like model transformation language reusing the main concepts of graph transformation systems. They formalize their model transformations as theories in rewriting logic, and in this way Maude’s reachability analysis and model checking features can be used to verify them. Only the reduced part of QVT relations that can be expressed with this language is covered. Our work is different: we formalize a complete existing transformation language by providing its representation in Maude, without proposing yet another MT language. In this paper we have dealt with all new features of ATL version 3.0, and in particular we have formalized the ATL refining mode. Many works have been dedicated to the semantics of the default execution mode, but no one seems to be focused on the refining mode despite the importance this execution mode is gaining. For example, Tisi et al. propose in [TCJ10] the use of this execution mode to implement Higher-Order Transformations (HOTs). They are model transformations that analyze, produce or manipulate other model transformations [TJF+09]. Writing HOTs is generally considered a time-consuming and error-prone task, and often results in verbose code. Refining mode is used in [TCJ10] to facilitate the definition of HOTs in ATL, and they recommend the developers to consider in-place refining mode for every transformation modification and (de)composition. Finally, Maude has been proposed as a formal notation and environment for specifying and effectively analyzing models and metamodels [RVD09, BM08]. Simulation, reachability and model-checking analysis are possible using the tools and techniques provided by Maude [RVD09]. We build on these works, making use of one of these formalizations to represent the models and metamodels that ATL handles. Journal of Object Technology, vol. 10, 2011