Artur Boronat
email: aboronat@mcs.le.ac.uk

José Meseguer

Under consideration for publication in Formal Aspects of Computing An Algebraic Semantics for MOF

Keywords: MOF, model-driven development, membership equational logic, metamodeling semantics, reflection, formal analysis

In model-driven development, software artifacts are represented as models in order to improve productivity, quality, and cost effectiveness. In this area, the Meta-Object Facility (MOF) standard plays a crucial role as a generic framework within which a wide range of modeling languages can be defined. The MOF standard aims at offering a good basis for model-driven development, providing some of the building concepts that are needed: what is a model, what is a metamodel, what is reflection in the MOF framework, and so on. However, most of these concepts are not yet fully formally defined in the current MOF standard. In this paper we define a reflective, algebraic, executable framework for precise metamodeling based on membership equational logic (mel) that supports the MOF standard. Our framework provides a formal semantics of the following notions: metamodel, model, and conformance of a model to its metamodel. Furthermore, by using the Maude language, which directly supports mel specifications, this formal semantics is executable. This executable semantics has been integrated within the Eclipse Modeling Framework as a plugin tool called MOMENT2. In this way, formal analyses, such as semantic consistency checks, model checking of invariants and LTL model checking, become available within Eclipse to provide formal support for modeldriven development processes.

Introduction

Model-driven development is a software engineering field in which software artifacts are represented as models in order to improve productivity, quality, and cost-effectiveness. Models provide a more abstract description of a software artifact than the final code of the application. The Meta-Object Facility (MOF) standard [START_REF] Omg | Meta Object Facility (MOF) 2.0 Core Specification[END_REF] offers a generic framework in which the abstract syntax of different modeling languages can be defined. This is done by specifying within MOF different metamodels for different modeling languages. Models in a modeling language are then conforming instances of their corresponding metamodel. The MOF standard aims at offering a good basis for model-driven development, providing some of the building concepts that are needed: what is a model, what is a metamodel, what is reflection in the MOF framework, and so on. However, most of these concepts are not yet fully formally defined in the current MOF standard. This is, in part, due to the fact that metamodels can only be defined as data in the MOF framework.

In this paper, we define a reflective, algebraic, executable framework for precise metamodeling that supports the MOF standard, focusing on the subset Essential MOF (EMOF) that is commonly used for metamodeling and that has close implementations in mainstream metamodeling environments such as the Eclipse Modeling Framework (EMF) [START_REF]The Eclipse Modeling Framework[END_REF]. Our formal framework provides a formal semantics of the following notions: metamodel, model, and conformance of a model to its metamodel. We clearly distinguish the different roles that the notion of metamodel usually plays in the literature: as data, as type, and as theory. In addition, we introduce two new notions: (i) metamodel realization, referring to the mathematical representation of a metamodel; and (ii) model type, allowing models to be considered as first-class citizens. In particular, our executable algebraic semantics for MOF generates, in an automatic way, the algebraic semantics of any MOF metamodel by formalizing MOF metamodels as mel theories. Furthermore, such mel theories are executable by rewriting. This means that useful mel deduction capabilites become available as decision procedures to check properties about the models of a metamodel so formalized; and that all this can be achieved by executing the mel theory formalizing a metamodel in an algebraic language such as Maude [START_REF] Clavel | All About Maude -A High-Performance Logical Framework[END_REF]. In this way, the executable formal semantics of a metamodel can be used to automatically analyze the conformance of its model instances. Such model instances are characterized algebraically as terms modulo structural axioms of associativity, commutativity and identity, and have an equivalent topological characterization as graphs. This makes the formal semantics particularly useful, since models can be directly manipulated as graphs in their term-modulo-axioms formal representation. Furthermore, as we explain below, it makes possible a number of very useful model management and model analysis tasks.

Our framework provides not only an algebraic semantics, but also an executable environment called MO-MENT2 [START_REF][END_REF], that is plugged into the Eclipse Modeling Framework (EMF) [START_REF]The Eclipse Modeling Framework[END_REF] and that constitutes the kernel of an algebraic model management framework supporting model transformations and formal analysis techniques. In this work, we illustrate the basic principles on which MOMENT2 is based by showing how the executable formalization of MOF metamodels as mel theories provides automated, semantics-based support for very useful model-based tasks, such as the definition of domain specific languages, model transformations, model traceability and model management operators; and formal analysis techniques, such as reachability analysis and LTL model checking of model-based systems. EMF-based technology is used for developing modeling environments and model-based software, including automated support for textual and graphical syntax and programming facilities. Our approach smoothly complements the aforementioned technology, so that already existing fully-fledged EMF-based modeling languages can be formalized and analyzed in MOMENT2 in an automatic manner.

Philosophically, we can view this work as exploiting for the area of software modeling languages the kinds of benefits that the rewriting logic semantics project [START_REF] Meseguer | The rewriting logic semantics project[END_REF] has already demonstrated in the areas of programming languages (see [START_REF] Meseguer | Rewriting logic semantics: From language specifications to formal analysis tools[END_REF][START_REF] Meseguer | The rewriting logic semantics project[END_REF][START_REF] Serbanuta | A rewriting logic approach to operational semantics[END_REF] and references there), and of formal specification and verification languages (see, e.g., [START_REF] Clavel | Maude as a formal meta-tool[END_REF][START_REF] Stehr | Pure type systems in rewriting logic: Specifying typed higher-order languages in a first-order logical framework[END_REF][START_REF] Cervesato | Representing the MSR cryptoprotocol specification language in an extension of rewriting logic with dependent types[END_REF]). What is common to all these efforts is the use of a flexible logical framework (either rewriting logic [START_REF] Meseguer | Conditional rewriting logic as a unified model of concurrency[END_REF], or, as done in this paper, its mel equational sublogic [START_REF] Meseguer | Membership algebra as a logical framework for equational specification[END_REF]) to formalize the semantics of either a programming language, a formal specification language, or, as done in this work, a wide range of software modeling languages. By exploiting the fact that the framework's logic is executable and has a high-performance implementation, one obtains much more than just precise semantic definitions: one obtains useful (and quite efficient) semantics-based tools, such as programming language interpreters and model checkers, theorem provers of various kinds, and, in this paper, a model management tool like MOMENT2 that is metamodel-generic and can support a wide range of model management and model analysis tasks.

The paper is structured as follows: Section 2 briefly describes the underlying formal background; Section 3 identifies important concepts that are not formally defined in the MOF standard and are usually left unspecified in most of the MOF implementations; Section 4 presents the foundations of our algebraic framework, explaining how the algebraic semantics of MOF metamodels is defined; Section 5 illustrates several applications of our framework in different model-driven development scenarios; Section 6 discusses related work; and Section 7 summarizes the main contributions of this work and discusses future work.

Membership Equational Logic, Rewriting Logic, and Maude

The logical framework in which we give an algebraic semantics to MOF is membership equational logic (mel) [START_REF] Meseguer | Membership algebra as a logical framework for equational specification[END_REF]. A key feature of mel is its strong support for types (called sorts), subtypes, and partiality; and the closely-related feature that types can be very expressive. In mel, membership in a type is not just a syntactic matter, but may depend on the satisfaction of semantic conditions. This mel feature is crucially exploited in our semantics of MOF, where the set of models that conform to a given metamodel is precisely characterized by a type satisfying suitable semantic conditions. Another key feature of mel is that it has initial algebras [START_REF] Meseguer | Membership algebra as a logical framework for equational specification[END_REF]; therefore, our MOF semantics is an initial algebra semantics. Furthermore, under very reasonable assumptions mel theories are executable by rewriting.

The Syntax and Semantics of MEL

A mel signature is a triple (K, Σ, S) (just Σ in the following), with K a set of kinds, Σ = {Σ w,k } (w,k)∈K * ×K a many-kinded signature of function symbols, and S = {S k } k∈K a K-kinded family of disjoint sets of sorts. The kind of a sort s is denoted by [s]. Intuitively, membership in a sort is exactly definedness; whereas membership in just a kind without membership in any of the sorts of that kind means undefinedness or error. For example, let Numeric be a kind having sorts Nat, Int, and Rat. Then, in a suitable mel specification of the number hierarchy we may have expressions like 4 -7 of sort Int, and 2/7 of sort Rat. But the expression 2/0 has kind Numeric but has no sort and is therefore interpreted as an undefined or error expression.

A mel Σ-algebra A contains a set

A k for each kind k ∈ K, a function A f : A k1 × • • • × A kn → A k for each operator f ∈ Σ k1•••kn,k
and a subset A s ⊆ A k for each sort s ∈ S k , with the meaning that the elements in sorts are well-defined, while elements without a sort are errors. In particular, T Σ is the Σ-algebra of ground Σ-terms, and for X a set of K-kinded variables, T Σ (X), is the Σ-algebra of Σ-terms with variables in X. T Σ,k and T Σ (X) k denote, respectively, the set of ground Σ-terms of kind k and of Σ-terms of kind k over variables in X, where X = {x 1 : k 1 , . . . , x n : k n } is a set of kinded variables.

Given a mel signature Σ, atomic formulae have either the form t = t (Σ-equation) or t : s (Σmembership) with t, t ∈ T Σ (X) k and s ∈ S k ; and Σ-sentences are conditional formulae of the form (∀X) ϕ if i p i = q i ∧ j w j : s j , where ϕ is either a Σ-equation or a Σ-membership, and all the variables in ϕ, p i , q i , and w j are in X. The novel feature with respect to other equational logics is the support for conditional memberships of the form (∀X) t : s if i p i = q i ∧ j w j : s j . This makes membership in a sort not just a syntactic matter, but a semantic one, since the semantic conditions i p i = q i ∧ j w j : s j must be satisfied.

A mel theory is a pair (Σ, E) with Σ a mel signature and E a set of Σ-sentences. The paper [START_REF] Meseguer | Membership algebra as a logical framework for equational specification[END_REF] gives a detailed presentation of (Σ, E)-algebras, sound and complete deduction rules, and initial and free algebras. In particular, given a mel theory (Σ, E), its initial algebra is denoted T (Σ/E) . As usual for any Σ-algebra, given a sort s ∈ S, the set T (Σ/E),s is the set of terms of sort s in T (Σ/E) , which by construction is precisely the set of E-equivalence classes of ground terms t ∈ T Σ such that E t : s, where denotes the provability relation in mel (see [START_REF] Meseguer | Membership algebra as a logical framework for equational specification[END_REF]).

Order-sorted notation s 1 < s 2 can be used to abbreviate the conditional membership (∀x : k) x : s 2 if x : s 1 . Similarly, an operator declaration f : s 1 × • • • × s n → s corresponds to declaring f at the kind level and giving the membership axiom (∀x

1 : k 1 , . . . , x n : k n ) f (x 1 , . . . , x n ) : s if 1≤i≤n x i : s i . We write (∀x 1 : s 1 , . . . , x n : s n ) t = t in place of (∀x 1 : k 1 , . . . , x n : k n ) t = t if 1≤i≤n x i : s i .
We can use order-sorted notation as syntactic sugar to present a mel theory (Σ, E) in a more readable form as a tuple (S, <, Σ, E 0 ∪ A) where: (i) S is the set of sorts; (ii) < is the subsort inclusions, so that there is an implicit kind associated to each connected component in the poset of sorts (S, <); (iii) Σ is given as an order-sorted signature with possibly overloaded operator declarations f : s 1 × . . . × s n → s as described above; and (iv) the set E of (possibly conditional) equations and memberships is quantified with variables having specific sorts (instead than with variables having specific kinds) in the sugared fashion described above; furthermore, E is decomposed as a disjoint union E = E 0 ∪ A, where A is a collection of "structural" axioms such as associativity, commutativity, and identity. Any theory (S, <, Σ, E 0 ∪A) can then be desugared into a standard mel theory (Σ, E) in the way explained above.

Rewriting Logic

Rewriting logic [START_REF] Meseguer | Conditional rewriting logic as a unified model of concurrency[END_REF][START_REF] Bruni | Semantic foundations for generalized rewrite theories[END_REF] is a flexible logic to specify concurrent systems. Any such system is specified by a rewrite theory R = (Σ, E, R), where (Σ, E) is a MEL-theory, and R is a collection of rewrite rules of the form

t -→ t if C
where t, t ∈ T Σ (X) k for some kind k, and C is a condition or guard. For the purposes of this paper we assume that C is a conjunction of Σ-equations u 1 = v 1 ∧ . . . ∧ u n = v n (for a more general notion of condition see [START_REF] Bruni | Semantic foundations for generalized rewrite theories[END_REF]).

The intuition about R is that the states of the sytem that R specifies are formalized as elements of the initial algebra T (Σ,E) , whereas the local state transitions are applications of rules in R that satisfy their condition C. Such rewrite rules transform each state containing a fragment that is an instance of the rule's left-hand side t to a new state where that fragment is replaced by the corresponding instance of t . More complex concurrent transitions in such a system are then formalized as proofs in the theory R (see [START_REF] Meseguer | Conditional rewriting logic as a unified model of concurrency[END_REF][START_REF] Bruni | Semantic foundations for generalized rewrite theories[END_REF]).

Executable MEL Theories and Maude

The point of the decomposition E = E 0 ∪ A is that, under appropriate executability requirements explained in [START_REF] Bouhoula | Specification and proof in membership equational logic[END_REF][START_REF] Clavel | All About Maude -A High-Performance Logical Framework[END_REF], such as confluence, termination, and sort-decreasingness modulo A, a mel theory (S, <, Σ, E 0 ∪ A) becomes executable by rewriting with the equations and memberships E 0 modulo the structural axioms A. Furthermore, the initial algebra T (Σ/E) then becomes isomorphic to the canonical term algebra Can Σ/E0,A whose elements are A-equivalence classes of ground Σ-terms that cannot be further simplified by the equations and memberships in E 0 .

An important consequence of (S, <, Σ, E 0 ∪A) satisfying the confluence, termination and sort-decreasingness requirements is that both term equality and term membership become decidable by rewriting [START_REF] Bouhoula | Specification and proof in membership equational logic[END_REF]. Furthermore, mel theories satisfying these executability properties can be executed in high-performance languages such as Maude [START_REF] Clavel | All About Maude -A High-Performance Logical Framework[END_REF] that support execution of mel theories modulo any combination of associativity and/or commutatitvity and/or identity axioms.

The syntax of Maude follows very closely the mathematical syntax for mel and rewriting logic described above, including support for order-sorted notation. In the rest of the paper we will at times present fragments of mel and rewriting logic specifications in Maude syntax. Specifically, as explained in [START_REF] Clavel | All About Maude -A High-Performance Logical Framework[END_REF], mel theories are specified in Maude as functional modules, whereas rewrite theories are specified as system modules. Such syntax is essentially self-explanatory, but we give here a few explanations to help the reader. First of all, basic notions such as sorts, subsorts, operators, equations, rules and memberships are declared with respective keywords sort, subsort, op, eq (or ceq for conditional equations), rl (or crl for conditional rules) and mb (or cmb for conditional memberships). Second, associativity and/or commutativity and/or identity axioms are not declared explicitly as equations, but are instead declared as attributes of the binary operator enjoying them in the corresponding op declaration with the assoc, comm, and id: keywords. Third, the syntax of an operator need not be prefix syntax: it can also be user-definable "mixfix" syntax, where the argument places are indicated by underbars. For example, a user can define an if-then-else operator with syntax if then else fi.

MOF and its Semantic Issues

In this section, we give an informal description of the MOF standard by describing the MOF architecture and the main concepts in the MOF metamodel. We also discuss several semantic issues that are then addressed by the formal algebraic semantics presented in subsequent sections.

The MOF Modeling Framework

MOF is a semiformal approach to define modeling languages usually presented as a four-level hierarchy, with levels M0, M1, M2 and M3. Each entity M at level i represents a model1 . M consists of a collection of typed elements e, which can be simple data values or objects. Types T for the elements e that constitute a model M at level i are defined as collections of elements in a metamodel M at level i + 1. There are two different kinds of types T : data types and object types. We indicate that an element e is typed with a type M1 level. This level contains metarepresentations of models. A model is a collection of objects that describe the elements of some physical, abstract or hypothetical reality by using a well-defined language.

In addition, a model is suitable for computer-based interpretation, so that development tasks can be automated. For example, the model conf1 in Fig. 1 defines a configuration of client/server components describing how they are interconnected. We use object diagram notation for representing models, making their graph structure explicit. Each object corresponds to a component indicating whether it is a client or a server. M2 level. This level contains metarepresentations of metamodels, usually given as class diagrams. A metamodel is a model specifying the abstract syntax of a modeling language and defines the types that can be used for defining objects in a model by means of UML-like classes. As an example, we consider a metamodel for defining configurations of components as shown in Fig. 1 in UML notation. The types of a configuration are defined by the classes Component, Server and Client. The Component class is abstract so that it cannot be instantiated. This class is specialized into a Client and a Server classes.

The model conf1 at level 1 conforms to the component metamodel M at level 2. M3 level. An entity at level 3 is the metarepresentation of a meta-metamodel. A meta-metamodel specifies a modeling framework, which could also be called a modeling space. In MOF, there is only one such meta-metamodel, called the MOF meta-metamodel (usually also called the metamodel MOF). Within the MOF standard, we focus on the Essential MOF (EMOF) specification that describes the metametamodel, which appears simplified in Fig. 1. In the MOF modeling framework one can define many different metamodels. Such metamodels, when represented as data, must conform to the MOF metametamodel. That is, a metamodel, such as the component metamodel, is a model that conforms to the meta-metamodel MOF. Other metamodels that are likewise specified in MOF are the UML2 metamodel to define UML models, the OWL metamodel to define ontologies [START_REF] Lacy | Owl: Representing Information Using the Web Ontology Language[END_REF], the AADL metamodel to specify real-time distributed computer systems [SAE07], and so on. The fact that all these metamodels are specified within the single MOF framework greatly facilitates systematic model/metamodel interchange and integration. The MOF hierarchy is closed at its top level, because the MOF meta-metamodel itself is also defined as a model that conforms to itself. The class diagram notation is indeed used as a convenient concrete graphical syntax at levels 2 and 3 for hidding the verbose representation of a model, which could likewise be given as an object diagram. Fig. 2 in Section 4.3 shows the model that constitutes the component metamodel as an object diagram.

Discussion and Open Problems

At present, important MOF concepts such as those of metamodel, model and conformance relation do not have an explicit, syntactically characterizable status in their data versions. For example, we can syntactically characterize the correctness of the data elements of a metamodel M , but there is no explicit type that permits defining M as a well-characterized value, which we call a model type. In addition, in the MOF standard and in current MOF-like modeling environments, such as Eclipse Modeling Framework or MS DSL tools, a metamodel M does not have a precise mathematical status. Instead, at best, a metamodel M is realized as a program in a conventional language as, for example, the Java code that is generated for a metamodel M in EMF. This informal implementation corresponds to what we call a metamodel realization. In these modeling environments, the conformance relation between a model definition M and its corresponding metamodel M is checked by means of indirect techniques based on XML document validation or on toolspecific implementations in OO programming languages. Therefore, metamodels M and models M cannot be explicitly characterized as first-class entities in their data versions, and the semantics of the conformance relation remains formally unspecified. This is due to the lack of a suitable reflective formal framework in which software artifacts, and not just their metarepresentations, can acquire a formal semantics.

In this work, we formalize the notions of: (i) metamodel realization, (ii) model type, and (iii) conformance relation, by means of a reflective semantics that associates a mathematical metamodel realization to each metamodel M in MOF.

An Algebraic Semantics for MOF

The practical usefulness of a formal semantics for a language is that it provides a rigorous standard that can be used to judge the correctness of an implementation. For example, if a programming language lacks a formal semantics, compiler writers may interpret the informal semantics of the language in different ways, resulting in possibly inconsistent and diverging implementations. For MOF, given its genericity, the need for a formal semantics that can serve as a rigorous standard for any implementation is even more pressing, since many different modeling languages rely on the correctness of the MOF infrastructure. In this section, we propose an algebraic, mathematical semantics for MOF in membership equational logic (mel).

A High-Level View of the MOF Algebraic Semantics

A metamodel M describes a metamodel realization that contains a model type. What this metamodel describes is, of course, a set of models. We call this the extensional semantics of M , and denote this semantics by M . Recall that we use the notation M : M for the conformance relation. Using this notation, the extensional semantics can be informally defined as follows:

M = {M | M : M }.
We make the informal MOF semantics just described mathematically precise in terms of the initial algebra semantics of mel. As already mentioned in Section 2, a mel specification (Σ, E) has an associated initial algebra T (Σ,E) . We call T (Σ,E) the initial algebra semantics of (Σ, E), and write

(Σ, E) IAS = T (Σ,E) .
Let MOF denote the set of all MOF metamodels M , and let SpecMEL denote the set of all mel specifications. The reason why we define MOF as a set of metamodels M , instead than as a set of model types M is because, as already mentioned, the mathematical status of M is, as yet, undefined, and is precisely one of the questions to be settled by a mathematical semantics. Instead, well-formed metamodels M are data structures that can be syntactically characterized in a fully formal way. Therefore, the set MOF , thus understood, is a well-defined mathematical entity. Our algebraic semantics is then defined as a function A : MOF -→ SpecMEL that associates to each MOF metamodel M a corresponding mel specification A(M ). The function A is defined in detail in Sections 4.2-4.4. Our informal semantics M is thus made mathematically precise. Recall that any mel signature Σ has an associated set S of sorts. Therefore, in the initial algebra T (Σ,E) each sort s ∈ S has an associated set of elements T (Σ,E),s . The key point is that in any mel specification of the form A(M ), there is always a sort called Model , whose data elements in the initial algebra are precisely the data representations of those models that conform to M . That is, Model is the syntactical representation of the model type M associated to a metamodel M . Therefore, after A is defined, we can give a precise mathematical semantics to our informal MOF extensional semantics by the defining equation

M = T A(M),Model .
Note that our algebraic semantics gives a precise mathematical meaning to the entities lacking such a precise meaning in the informal semantics, namely, the notions of: (i) model type M , (ii) metamodel realization A(M ), and (iii) conformance relation M : M . Specifically, we associate to a metamodel M a precise mathematical object, namely, the mel theory A(M ), constituting its metamodel realization. The structural conformance relation between a model and its metamodel is then defined mathematically by the equivalence

M : M ⇔ M ∈ T A(M),Model .
We will summarize again our formal semantics of all the key MOF concepts in Section 4.4.1 after all details of the function A have been made precise in Sections 4.2-4.4.

Reflective Bootstrapping of the Algebraic Semantics

The algebraic semantics that we propose exploits the reflective features of both MOF and mel. This allows a modular, stepwise approach in the definition of the semantic function A. This has many advantages, both theoretically and in the practical realization of A in the MOMENT2 tool.

The key observation about reflection in MOF is that the MOF meta-meta-model at level 3 is also a meta-model at level 2, which can be treated just as any other metamodel. In particular this means that

MOF ∈ MOF .
It also means that our algebraic semantics function A : MOF -→ SpecMEL applies in particular to MOF, that is, that there is a mel theory A(MOF).

The mel theory A(MOF) is enormously useful to bootstrap our algebraic semantics because of the following remarkable property. Since for any metamodel M we have the identity M = T A(M),Model , in particular for the meta-metamodel MOF we have the identity

MOF = T A(MOF),Model .
This suggests the following bootstrapping strategy to define the semantic function A : MOF -→ SpecMEL.

1. First define the mel theory A(MOF). This automatically gives us the domain MOF of our desired semantic function A : MOF -→ SpecMEL as the algebraic data type MOF = T A(MOF),Model . 2. Once the domain MOF of A is thus algebraically represented, proceed to give a recursive definition of the semantic function A for any M ∈ MOF .

Step (1) is described in Section 4.3, and Step (2) in Section 4.4.

There is, however, a third very important step, namely, to also exploit reflection in the target logical framework mel. Reflection in mel means that there is a universal mel theory U ∈ SpecMEL that can simulate the deduction of all finitary mel theories, including its own deduction [START_REF] Clavel | Reflection in membership equational logic, many-sorted equational logic, Horn logic with equality, and rewriting logic[END_REF].

In particular, the universal theory U has a sort Module that meta-represents all finitary mel theories, including U itself. This means that there is an algebraic data type SpecMEL whose elements are metarepresentations of mel theories, so that given any finitary mel theory (Σ, E), we have (Σ, E) ∈ SpecMEL iff (Σ, E) ∈ SpecMEL, where (Σ, E) is the meta-representation of (Σ, E). Specifically, the algebraic data type SpecMEL has the following initial algebra semantics definition:

SpecMEL = T U ,Module .
All this means that we can take a third step in our bootstrapping process, namely, to realize our semantic function A as an equationally defined function A : MOF -→ SpecMEL mapping each metamodel M to the metarepresentation A(M ) of the mel theory A(M ).

At the theoretical level, this third bootstrapping step means that the entire algebraic semantics of MOF can be defined within the semantic framework of mel. At the practical level it also means that, because of the efficient support in Maude for key functionality of the universal mel theory U by means of Maude's META-LEVEL module, the function A can be efficiently implemented in Maude. In fact, this is exactly how the core functionality of the MOMENT2 tool has been developed, as explained in Section 4.4.

In Sections 4.3 and 4.4 we give a high level summary of the definition of the A semantic function, as achieved by the three reflective bootstrapping steps described above. A complete definition of A is available in [START_REF] Boronat | MOMENT: a formal framework for MOdel manageMENT[END_REF] 2 . In Section 4.5 we explain how A is used in the EMF by means of MOMENT2.

The MEL Theory A(MOF)

As already mentioned, we denote the metamodel that constitutes the meta-metamodel of the MOF framework by MOF. In particular, we focus on the subset EMOF of the MOF standard. An excerpt of the metamodel EMOF, extracted from the core specification of the standard MOF 2.0 [START_REF] Omg | Meta Object Facility (MOF) 2.0 Core Specification[END_REF] is shown in Fig. 1. MOF is itself a MOF metamodel, since MOF : MOF. In this section we take the first bootstrapping step described in Section 4.2, namely, to define the mel theory A(MOF). That is, we first define A for a single metamodel, namely MOF. The A(MOF) theory defines the MOF type as the set of metamodels M , which can be viewed as both graphs and terms. This theory has been manually defined in [START_REF] Boronat | MOMENT: a formal framework for MOdel manageMENT[END_REF] as a first step in the bootstrapping process needed to define the A function in general. The A(MOF) theory provides the algebraic representation for both object types and model types for defining metamodels M . The full specification of A(MOF) as a membership equational theory is given in Maude notation as a functional module [START_REF] Boronat | MOMENT: a formal framework for MOdel manageMENT[END_REF]. As already explained in Section 2.3, Maude functional modules are exactly mel theories with an initial algebra semantics. The Maude notation for sorts, subsorts, operations, equations and memberships is self-explanatory and typewriter variant of the mathematical notation [START_REF] Clavel | All About Maude -A High-Performance Logical Framework[END_REF]. In what follows we present some fragments of the theory fully specified in [START_REF] Boronat | MOMENT: a formal framework for MOdel manageMENT[END_REF], in Maude notation, with special emphasis on its sorts, subsorts and operations.

In the theory A(MOF), object types are used to describe a metamodel M : MOF as a collection of objects. Objects are defined by using the following sorts: Oid for object identifiers; Cid for class names; and PropertySet for multisets of comma-separated pairs of the form (property : name = value), which represent property values. Objects in a metamodel M are then syntactically characterized by means of an operator op <_:_|_> : Oid Cid PropertySet -> Object .

These sorts, subsorts and operators are defined, in Maude notation, as follows: In the A(MOF) theory, a metamodel M that conforms to the meta-metamodel MOF, that is, such that M : MOF, can be represented as a collection of objects by means of a term of sort Model. A term of sort Model is defined by means of the following constructors, in Maude notation: That is, we first form a collection of objects of sort ObjCol using the associative and commutative multiset union operator __3 and then we wrap the set of objects by using the <<_>> constructor to get the desired term of sort Model. Note that membership in the sort Model is not defined just by the constructor <<_>> (only membership in the kind [Model] is implied by the above operator declaration). Instead, membership of a term in the sort Model is achieved by conditional membership axioms that are given below after introducing the formal definition of the object types Class and Property. Each of these modeling primitives is specified in the A(MOF) theory by means of sorts, subsorts and operators, in Maude notation as follows.

Class object type. Object types are the central concept of MOF to model entities of the problem domain in metamodels. An object type is defined in a metamodel M as a Class instance and a set of Property instances. The object type Class contains meta-properties like name, which indicates the name of the object type, ownedAttribute, which indicates the properties that belong to the Class instance, and superClass, which indicates that the object type is defined as a specialization of the object types that are referred to by means of this property. The Class object type is specified as a sort Class, such that Class < Cid, and a constant with the operator op Class : -> Class . Terms of sort Property in the theory A(M ) enable the definition of property values in objects that form part of a metamodel.

In the component metamodel, the Class instance that defines the object type Component in the metamodel M is defined as the term < 'class0 : Class | property : "name" = "Component", property : "isAbstract" = true, property : "ownedAttribute" = ... >

where 'class0 is an object identifier.

Property object type. A model can be viewed as a graph where the collection of nodes consists of the collection of attributed objects of the model and the edges are defined by means of directed links between objects, defined as object-typed property values. This graph structure is usually represented with object diagram notation as in Fig. 1. Indeed, a model is an enriched graph where edges can also be defined as structural containments so that hierarchies of nested objects can also be represented.

A Property instance in a metamodel M enables the definition of an attribute in an object or an association end between objects in a model definition M : M , one level down in the MOF framework. A Property instance defines the type of the property, where the type is represented as a DataType instance (basic data values and enumerations) or as a Class instance (object types). Properties that are typed with datatypes are attributes, and properties that are typed with object types are association ends or references. An association end defines a unidirectional association between two classes 4 . Bidirectional associations are defined by means of two opposite association ends. Composition associations can be defined by indicating that the association end that points to the composite class has its meta-property isComposite set to true. Other meta-properties, such as lower, upper, isOrdered and isUnique, constitute the multiplicity metadata of a specific property.

The constructors that permit defining objects of the Property object type are defined, in Maude notation, as follows5 : sort Prop . subsort Prop < TypedElement . op Prop : -> Prop .

The Property instance that defines the metaproperty name of the object type Component in the metamodel M of the example is represented by the term < 'prop : Prop | property : "name" = "name", property : "type" = 'String, property : "class" = 'class0 >.

where 'String is the identifier of the object that represents the built-in String type. We have taken into account the modeling primitives that constitute the metamodel Essential MOF, including simple data types and enumeration types. A detailed specification is provided in [START_REF] Boronat | MOMENT: a formal framework for MOdel manageMENT[END_REF]. The metamodel M of the example is defined as a term of sort Model in the A(MOF) theory in Fig. 2.

MOF model type. In the theory A(MOF), the sort ObjCol denotes collections of objects that are instances of the classes in the metamodel MOF and the sort Model denotes the set of collections of objects that are models that conform to a given metamodel by satisfying a number of constraints. In particular, we consider that an object collection is a model if: ( i) there are no duplicate identifiers for different objects, (ii) properties are only set once in an object tuple, (iii) there are no dangling references (that is, a model is a well-formed graph), (iv) an object can only have one container according to the composite association ends in the metamodel (that is, a model is a hierarchical graph), and (v) values in properties correspond to the type of the corresponding property definition in the metamodel. The sort Model is defined with the following memberships, which provide the semantics of the model type for the metamodel MOF: The predicates used in the condition of the second membership axiom are defined in the Appendix A as equationally defined boolean functions, where the predicates correspond to the above-mentioned constraints, in order of appearance.

The theory A(MOF) is the metamodel realization of MOF. The carrier of the sort Model, in the theory A(MOF), in the initial algebra T A(MOF) defines the MOF model type, i.e., the model type whose elements are metamodels:

MOF = T A(MOF),Model .
Note that, since MOF is the set of all metamodels M in MOF, this means that MOF ∈ MOF .

Reflective Algebraic Semantics of MOF Metamodels

Once the A(MOF) theory is provided, we define the value of the function A on any metamodel M , such that M ∈ MOF , as its corresponding mel theory A(M ). This corresponds to the second bootstrapping step described in Section 4.2. Given a metamodel M , the A(M ) theory defines the M semantics as the set of models M that consist of a collection of typed objects, which can be viewed as a graph where objects correspond to nodes, object attributes to node attributes and object-typed properties to edges. In addition, nodes can be nested by means of object-typed properties that are defined as isComposite. The metamodel M of a model M corresponds to the type graph of the graph M , where object types constitute node types enabling node inheritance by means of class inheritance relationships.

In the A(M ) theory, the algebraic notion of object type is generically given by means of the sort Object.

Terms of sort Object are defined by means of the constructor op <_:_|_> : Oid Cid PropertySet -> Object.

which is analogous to the constructor for objects that has been presented in the A(MOF) theory.

Models M : M are given as collections of objects, which are instances of a specific class with name C. A class in a metamodel is an instance of the class Class in MOF. Each class may contain a number of properties, defined as instances of the class Property in MOF, as explained in Section 4.3. The object type C that corresponds to a class C is the set of objects that can be defined as instances of the class C. Defining the algebraic semantics of an object type involves the definition of the object identifiers and the properties that may be involved in the definition of a specific object in a model M : M . Class inheritance and the corresponding object type specialization relationships must be also taken into account. Therefore, we need to define the carrier of the sorts Oid, Cid and PropertySet for a specific object type definition.

Consider, for example, the metamodel M in Fig. 1. In subsequent paragraphs, we use this example to obtain the theory that defines the Component, Server and Client object types.

Class Names. In the A(M ) theory, each Class definition with name C in M (except for abstract classes) is defined as a new sort also named C and declared to be a subsort of Cid, and C is also declared as a constant by giving an operator declaration op C : -> C . Abstract classes are defined as those that cannot be instantiated. For an abstract class C, only the sort C is declared as before. The name of an abstract class C is not specified as a constant. In this way, when C is an abstract class, objects in a model M , such that M : M , cannot have C as their type.

In the example of the component metamodel, the A function generates a sort for the abstract object type Component in Maude notation as follows:

sort Component .
The concrete object types Client and Server are formalized as sorts and constants as follows:

sorts Client Server . op Client : -> Client . op Server : -> Server .

The class name for a given object can be obtained by means of the operator class defined as follows:

op class : Object -> Cid . eq class(< O : C | PS >) = C .
Object Type Specialization Relation. A specialization is a taxonomic relationship between two object types and is represented as a class inheritance relationship between a subclass and a superclass, where multiple inheritance is allowed. This relationship specializes a general object type into a more specific one and is formalized in Maude as a subsort relationship. In the example, we algebraically define the inheritance relationships between the classes Client, Server and Component by means of the subsorts subsorts Client Server < Component .

The supersorts of the resulting subsort hierarchy are defined as subsorts of the sort Cid.

subsort Component < Cid .

Object Type Properties. A class is defined with a collection of Property instances describing its metaproperties. A Property instance is associated with a specific type t in the metamodel M , which is defined as an object t : Type. Depending on the type t of a property, we can distinguish two kinds of properties:

• Value-typed Properties or Attributes. Properties of this kind are typed with DataType instances, which can represent either a simple data type or an enumeration type. Value-typed properties define the attributes of nodes in a graph. • Object-typed Properties or Association Ends. Properties of this kind are typed with object types, enabling the definition of unidirectional labelled edges in a graph.

The type meta-property together with the multiplicity metadata define a set of specific constraints on the acceptable values for the property type. These constraints are taken into account in the algebraic type that is assigned to the property by means of OCL collection types, as indicated in Table 1. In this table, the Set{Oid} sort corresponds to sets of identifiers that may be empty by means of the constant empty-set, while the NeSet{Oid} sort corresponds to sets of identifiers that cannot be empty, i.e., it excludes the constant empty-set. In the example, the Component object type is specified in the theory A(M ) with the above sorts and subsorts and with the operators for defining properties.

Summary of the MOF Algebraic Semantics

The function A : M OF -→ SpecMEL specified in Sections 4.2-4.4 provides the basics for associating to each basic, informal concept about MOF metamodels a corresponding formal definition. This was already sketched out in Section 4.1, but is now made even more explicit for the following concepts: (i) metamodel realization, (ii) object type, (iii) model type, and (iv) conformance of a model to a metamodel. (i) The metamodel realization of M is the MEL-theory A(M ).

(ii) The object type of the class C is the set

C = {o | o ∈ T A(M),Object ∧ class(o) ∈ T A(M),C },
that is, the elements of the object type C are all the object instances of the class C and of all its subclasses in the inheritance relation specified in M . (iii) The model type of M is the set

M = T A(M),Model ,
that is, each model M of M is algebraically represented as an element M ∈ M , i.e., as an equivalence class of terms of sort Model modulo the equations and memberships of A(M ).

(iv) The metamodel conformance relation between a model M and its metamodel M , denoted M : M , is, by definition, the memberhip relation M ∈ M , that is, we have

M : M ⇔ M ∈ M .

Embedding MOF Reflection into MEL Logical Reflection.

We are now ready to discuss the third, final bootstrapping step, mentioned in Section 4.2. The logical reflective features of mel [CDE07, CMP07], particulary its universal theory U, make it possible to internalize the representation function mapping the specifications of some other formalism to mel as an equationally defined function within mel (see [START_REF] Clavel | Maude as a formal meta-tool[END_REF]). In particular this can be done for our representation function for MOF

A : MOF -→ SpecMEL.

Note that the domain of the function A, since it is the algebraic data type MOF = T A(MOF),Model defined by initial algebra semantics in Section 4.3, is already internalized within mel. However, the set of (finitary) mel specifications SpecMEL is a metalevel entity and therefore outside the object level of mel, that is, not directly definable as an algebraic data type in mel. As explained in detail in [START_REF] Clavel | Reflection in membership equational logic, many-sorted equational logic, Horn logic with equality, and rewriting logic[END_REF], this set is representable at the object level inside the universal theory U as the set of elements of sort Module in its initial algebra T U . That is, we have a faithful representation mapping

SpecMEL -→ SpecMEL : (Σ, E) → (Σ, E)
where, by definition, the set SpecMEL is the algebraic data type

SpecMEL = T U ,Module
corresponding to the elements of sort Module in the initial algebra of the universal theory U. Then, the reflective internalization of the MOF algebraic semantics A becomes an equationally defined function A : MOF -→ SpecMEL : M → A(M ) so that the term A(M ), for a specific metamodel M , metarepresents the mel theory A(M ).

But since the universal theory U faithfully simulates all the deductive capabilities of an object level theory (Σ, E) by means of its meta-representation (Σ, E) as data [START_REF] Clavel | Reflection in membership equational logic, many-sorted equational logic, Horn logic with equality, and rewriting logic[END_REF], this means that, given a metamodel M in MOF, anything we can do with its associated mel theory A(M ) we can likewise perform at the metalevel with its meta-representation as data A(M ). Furthermore, in an efficient implementation of the relevant deductive functionality of U such as the one provided in Maude's META-LEVEL module [CDE07], the difference in computation time between performing a deduction in A(M ) or performing the analogous deduction at the metalevel with A(M ) is negligible in practice.

In this way, the term A(M ), that for a specific metamodel M meta-represents the mel theory A(M ), can then be used in different model-driven development scenarios, as illustrated in Section 5. The function A is completely defined in [START_REF] Boronat | MOMENT: a formal framework for MOdel manageMENT[END_REF] and is implemented as A in MOMENT2. That the function A is equationally definable follows from the general principle that A is a computable function and that all computable functions can be equationally defined by a finite set of confluent and terminating equations [START_REF] Bergstra | Characterization of computable data types by means of a finite equational specification method[END_REF]. In practical terms, this is just a matter of representing all the recursive definitions given for in A earlier in Section 4.4 as corresponding equational definitions at the metalevel.

MOMENT2 and the Eclipse Modeling Framework

MOMENT2 is a suite of tools, built on top of the Eclipse Modeling Framework (EMF), that provides support for formal model-driven development. The mathematical foundations of this tool suite directly rely on the algebraic semantics A of MOF metamodels, presented in this work, which can be neatly exploited in the EMF, a widely used MOF-like metamodeling framework, by means of OMG standards, such as MOF, OCL and QVT. In this way, the formal analysis techniques that are presented in Section 5 can be applied to modeldriven development practices in industrial environments, such as Rational Software Architect [START_REF]Rational Software Architect for WebSphere Software[END_REF] or OSATE AADL [SAE07]. In particular, MOMENT2 provides support for verifying metamodel conformance with OCL constraint satisfaction [START_REF] Boronat | Algebraic Semantics of OCL-constrained Metamodel Specifications[END_REF], QVT-like model transformations and their verification based on Maude's reachability analysis and Maude's LTL model checker, as explained in [START_REF] Boronat | Rewriting Logic Semantics and Verification of Model Transformations[END_REF].

The integration of MOMENT2 into the EMF is based on a metamodel-independent, automatic bridge6 between EMF and Maude. For each metamodel M , the key components of this bridge are: (i) a model representation function rep : M -→ M EMF , which represents each M -conformant model M ∈ M in the algebraic semantics as an EMF model instance7 rep(M ) ∈ M EMF , where M EMF denotes the set of M -conformant models in their EMF representation; and (ii) its inverse function rep -1 : M EMF -→ M , which converts each EMF model instance to its corresponding algebraic representation rep -1 (M EMF ) ∈ M . Note that only the set M has been given a formal representation. Therefore, the set M EMF and the functions rep and rep -1 are respectively realized by the EMF system and Java code in the MOMENT2 implementation. However, the bridge provided by the (rep, rep -1 ) pair is quite robust, because the conformance relation is checked for M EMF ∈ M EMF by EMF, and for M ∈ M by Maude. Up to renaming of object identifiers, the functions rep and rep -1 are inverse of each other. Specifically, for each M EMF ∈ M EMF we have rep -1 (rep(M EMF )) = M EMF and for each M ∈ M , rep(rep -1 (M )) differs from M only in a renaming of its object identifiers, due to the internal management of object identifiers as URIs in EMF.

Fig. 3 shows a summary of the formalization of the metamodel M of the example and a configuration of components as a model M in the formal framework, i.e., as a term of sort Model. In this way, MOMENT2 enables the prototyping and experimentation of formal model-driven development techniques and the formal analysis of model-based languages and models in Maude, as shown in Section 5.

M2 M1

Fig. 3. EMF-Maude mappings in MOMENT2.

A Metamodeling Framework with n Layers.

Although the number of metamodeling layers that are usually taken into account is up to four, the MOF 2.0 core specification allows the use of n layers [START_REF] Omg | Meta Object Facility (MOF) 2.0 Core Specification[END_REF]. Our algebraic semantics for layers M3-M28 can be naturally extended to support n layers for arbitrary n ≥ 2. Furthermore, it is not necessary to require that the corresponding semantic framework is mel, which typically supports a more static semantics. To support dynamic semantics of models in an n-layer MOF framework, we may use rewriting logic and exploit the logic containment mel ⊆ rl, which induces a containment of specifications SpecMEL ⊆ SpecRL. Our present semantics, which is a semantics A = A 1 , can be extended as follows. The first step of the extension chooses a model Q 1 ∈ MOF and defines a new formal semantics for layer 2 as a function

A 2 : Q 1 -→ SpecRL.
We again define the semantics of a model Q 2 ∈ Q 1 using initial model semantics by using a sort Model in

A 2 (Q 2 ) and defining Q 2 = T A(Q2),Model where if A 2 (Q 2 ) is the rewrite theory (Σ, E∪A, R), then T A2(Q2),Model
is, by definition, the carrier of sort Model in the initial algebra T (Σ,E∪A) .

Following inductively this way, if we have already provided a semantics up to level n using models

Q 0 ∈ MOF (where Q 0 = MOF), Q 1 ∈ Q 0 , Q 2 ∈ Q 1 , . . . , Q n-1 ∈ Q n-2 , then we can add layer n + 1 0 Q 0 Q 0 A0 / / A 0 (Q 0 ) 1 Q 0 Q 1 A1 / / A 1 (Q 1 ) . . . . . . n + 1 Q n Q n+1 An+1 / / A n+1 (Q n+1 )
Fig. 4. N-layer metamodeling framework for MOF.

in the same way by choosing a model Q n ∈ Q n-1 and by defining a function

A n+1 : Q n -→ SpecRL
again, defining for each Q n+1 ∈ Q n its semantics by the identity

Q n+1 = T An+1(Qn+1),Model .
This process of iterated extension is schematically depicted in Figure 4, where A 0 coincides with A obtaining the MOF theory A 0 (Q 0 ) = A(MOF), explained in Section 4.3. Note that the first extension step A 2 to our semantics A 1 has already been considered, in a more general way, in the paper [START_REF] Boronat | What is a Multi-Modeling Language?[END_REF], where for each Q 1 ∈ MOF an institution [GoB92] I Q1 is chosen and then an

I Q1 -based semantics is given as a mapping A 2 : Q 1 -→ Spec I Q 1 .
The above extension scheme is the case where I Q1 = rl. Furthermore, our scheme, by using initial model semantics at all layers can be extended to an arbitrary number of levels, whereas it is not clear how the more general institutional semantics of [START_REF] Boronat | What is a Multi-Modeling Language?[END_REF] could be further extended to layer 3 for an arbitrary institution.

An interesting example of a useful extension of our semantics A 1 to a rewriting logic semantics A 2 is provided by the semantics (presented in [START_REF] Ölveczky | Formal Semantics and Analysis of Behavioral AADL Models in Real-Time Maude[END_REF]) of (a fragment of) AADL models in rewriting logic as a mapping A 2 : AADL -→ SpecRL, where an AADL model Q 2 , including behavior information defined with AADL's behavioral annex, has an associated rewrite theory A 2 (Q 2 ) that can be used in conjuction with the Real-Time Maude tool [START_REF] Ölveczky | Semantics and pragmatics of Real-Time Maude[END_REF] to both simulate and formally analyze real-time properties of the AADL model Q 2 .

Applications in Model-Driven Development Scenarios

In this Section we present some model-driven scenarios in which the algebraic semantics A of MOF metamodels plays an important role. We illustrate the application of A by using Maude and its support for formal reasoning in the running example of model-based software architecture reconfigurations. These techniques are internally used in MOMENT2, so that they can be applied in EMF-based environments through OMG standards and without explicit contact with the underlying mel and Maude.

Section 5.1 presents some scenarios where A provides the formal foundations for techniques and practices widely used in the model-driven community: metamodel conformance, semantics of MOF domain-specific languages, model transformations and model management. Section 5.2 focuses on the formal implications and advantages of our approach where formal analysis is made available within modeling environments: static analysis based on structural constraint satisfaction, and dynamic analysis based on reachability analysis and LTL model checking.

Model-Driven Development Scenarios

Model-driven development techniques can be formalized in our approach as follows. A MOF-based domain-specific language (DSL) provides modeling primitives that can be used to define concepts in a given domain. For example, real-time embedded systems can be specified with AADL [SAE07], web service workflows can be defined with BPEL [START_REF]Web Services Business Process Execution Language Version 2.0[END_REF], or ontologies can be defined with OWL [START_REF] Lacy | Owl: Representing Information Using the Web Ontology Language[END_REF]. The abstract syntax of these languages is provided as MOF metamodels, their concrete syntax can be either textual or graphical, and their dynamic semantics can be defined either with approaches for defining the semantics of programming languages, with frameworks that provide library support for manipulating models, such as Kermeta [Tri08], or with graph transformation systems [Roz97, EMK99, EEP06]. The last one constitutes an interesting candidate for defining model-based DSLs due to the graph-based nature of models and to the formalization of the approach.

A MOF metamodel M is used to define concepts in a particular domain, such as components in our running example, where software architectures are configurations of components that may be connected to each other through the connectsTo association end. In this section, we enrich the algebraic semantics A(M ) with a rewrite rule to define a dynamic semantics for component configurations. In particular, we add a dynamic connection load balancing strategy, so that a server component should not have more than two connections at a time, i.e., when a component has more than two connections, the spare connections are forwarded to other components with less than two incoming connections. We depict the reconfiguration as a graph transformation rule in Fig. 5, where a rule is defined with a left-hand side (LHS) pattern and a right-hand side (RHS) pattern. Each pattern consists of nodes that represent Component objects in a model (graph) M and edges representing connectsTo references between them. A reconfiguration can be applied whenever the LHS pattern of the rule can be matched against a specific configuration M of components, and then the edges are manipulated as follows: an edge in the LHS and not in the RHS is removed from the configuration, an edge not in the LHS but in the RHS is added, the rest of edges remain unmodified. Marked edges indicate that the edges must not exist in order to apply the rule; this notion is known as a negative application condition in the graph transformation community.

The graph-theoretic nature of models is axiomatized in our algebraic semantics as a set of objects modulo the associativity, commutativity, and identity axioms of set union. The semantics of a reconfiguration can then be naturally expressed as a rewrite theory [START_REF] Meseguer | Conditional rewriting logic as a unified model of concurrency[END_REF] extending the algebraic semantics A(M ) of our metamodel specification with rewrite rules that are applied modulo the equational axioms. In this way, the above graph-transformation rule can be summarized at a high level as follows: where the expression P := M matches the pattern P to the model variable M, O1, O2, O3, O4, O5 : Oid, C1, C2, C3, C4, C5 : Component, PS1, PS2, PS3, PS4, PS5 : PropertySet, OC : ObjCol, M : Model, the LHS of the graph transformation rule in Fig. 5 corresponds to the pattern in the P := M expression, its RHS corresponds to the RHS of the rewrite (after the => symbol), and the nac(O5,M) condition corresponds to the negative application condition that enables the application of the rule:

op nac : Oid Model -> Bool . eq [counterexampleNAC] : nac(O1, << < O1 : C1 | PS1 > < O2 : C2 | property : "connectsTo" = O1, PS2 > < O3 : C3 | property : "connectsTo" = O1, PS3 > OC >> ) = false . eq [satisfiedNAC] : nac(O1, M) = true [owise] .
The formalization of model transformations in rewriting logic and their verification in Maude presented in [START_REF] Boronat | Rewriting Logic Semantics and Verification of Model Transformations[END_REF] is also available in the MOMENT2 framework, extending the formalization of the MOF framework that is presented in this paper, relying on it, and providing a user-friendly EMF-based programming environment generated with openArchitectureWare9 . The most recent version of MOMENT2 provides a QVT-like syntax to define transformation rules that are then automatically translated into rewrite rules and executed by Maude. In [START_REF] Boronat | Rewriting Logic Semantics and Verification of Model Transformations[END_REF], the authors present a more detailed treatment of the graph transformation notions that are explained in this section for formal verification purposes.

Model transformations and operators for model management.

Due to the executability of MEL specifications in Maude, the realization of MOF metamodels as MEL theories enhances the formalization and prototyping of model-driven development processes, such as:

• Model transformations [START_REF] Sendall | Model transformation: The heart and soul of model-driven software development[END_REF], where translations of models between different modeling languages can be performed. • Model-driven roundtrip engineering [START_REF] Bork | Towards roundtrip engineering -a template-based reverse engineering approach[END_REF][START_REF] Paesschen | Selfsync: a dynamic round-trip engineering environment[END_REF], where a model that constitutes the abstract syntax tree of a program can be translated into a model that specifies the software at a higher level of abstraction.

Code may be generated again from recovered models in an automated way. An important issue is to keep both the abstract description and the code synchronized to deal with changes in a consistent way. • Model traceability [START_REF] Aizenbud-Reshef | Model traceability[END_REF], where traceability is important to keep track of the changes applied to software artifacts in a software development process for maintenance and evolution purposes. • Model management [START_REF] Bernstein | Applying Model Management to Classical Meta Data Problems[END_REF], where models can be manipulated by means of generic operators that rely on mappings between models. These operators permit, for example, merging models, generating mappings between models, and computing differences between models; they can be used to solve complex scenarios such as the roundtrip problem.

We illustrate the application of MOMENT2 to trace component reconfigurations, which can be applied to adapt a configuration to a given criteria, as the load balance strategy discussed above. We consider a traceability metamodel T to define mappings between components as models T , such that T : T . An equationally defined operator is presented to generate such models. The metamodel T in Fig. 6 permits defining mappings between components that may belong to different configurations as TMapping instances. A TModel instance constitutes the container for all the mappings between two models. Given configurations conf1 and conf2, a trace model can be defined between them in order to map the elements that represent the same component in both configurations. Such mappings can be used to keep track of the changes that have been applied to the initial configuration or to identify structurally-equivalent elements in a model management scenario as presented in [START_REF] Boronat | Automatic Support for Traceability in a Generic Model Management Framework[END_REF]BCR06].

A model transformation, defined as an equationally defined function, can be used to automatically generate a trace model between two configurations. The following match operator takes two component configurations (the models conf1 and conf2 in Fig. 1) as inputs and generates a trace model with mappings between the components of both configurations. The match operator uses an auxiliar operator $match that, in addition, takes a traceability model that is initialized with a TModel instance, and a natural number that is used to create object identifiers. The $match operator adds a new link whenever two components with the same name are found. More complex structural criteria can be used to match objects by simply traversing the objects that constitute the model by means of matching modulo associativity and commutativity axioms. where Model{Trac} is the sort of the model type T in the theory A(T ), init-trac is a constant that represents a trace model with a single TModel instance, the getNewOid function obtains a new object identifier from a natural number, and the including operator adds an element to a set, as in OCL. The trace model betweeen the configurations conf1 and conf2 can be generated by means of the command red match(conf1, conf2). The output model is illustrated in Fig. 7.

Formal Analysis Scenarios

In this subsection, we present some applications of the algebraic semantics A for MOF metamodels to formal reasoning of model-driven development practices. In particular, static and dynamic analysis of model-based domain-specific languages (DSLs).

Static analysis.

Once a metamodel M is realized as a theory A(M ), more axioms can be added to A(M ) in order to enrich the semantics of the metamodel M or to add semantics to the corresponding DSL. These axioms may correspond to OCL constraints as shown in [START_REF] Boronat | Algebraic Semantics of OCL-constrained Metamodel Specifications[END_REF] and can be used to verify that a specific model satisfies certain semantic properties.

For example, we can define a boolean predicate over a model that specifies that client components do not receive connections from other components in a specific configuration. This predicate is given as an equationally defined function that negates the satisfaction of the predicate when the property is not satisfied and that asserts its satisfaction in any other case: where O1, O2: Oid, C1 : Component, PS1, PS2: PropertySet, and OC : ObjCol, and where the last equation uses Maude's owise feature, so that it is applied if and only if the other equations for checkClientServer fail. As explained in [START_REF] Clavel | All About Maude -A High-Performance Logical Framework[END_REF], owise equations are semantically equivalent to ordinary but more verbose conditional equations. The models conf1 and conf2 in Fig. 1 can then be verified as follows:

red checkClientServer(conf1) . result Bool: true red checkClientServer(conf2) . result Bool: false where conf2 does not satisfy the constraint.

Formal verification of behavioral specifications.

The rewriting logic semantics of DSLs, defined by means of A and additional rewrite rules, can also be used for formal dynamic analysis. Given a specific initial configuration M of components, we can use Maude's search command to model check whether or not all possible reconfigurations of an initial configuration preserve the constraint checkClientServer, introduced above.

The metamodel realization A(M ), corresponding to Fig. 1, and the rewriting rule free-reconfiguration presented above define a state transition system, where states represent configurations M and M of components and transitions M -→ M are given by one application of the reconfiguration rule. However, a reconfiguration of this kind could conceivably produce configurations M of components that do not satisfy the constraint checkClientServer.

In Maude, the search command allows one to exhaustively explore (following a breadth-first strategy)

the reachable state space defined by a state transition system as the one above, checking if an invariant is violated. We can use the search command to find out if the reconfiguration free-reconfiguration produces such an illegal configuration as follows10 :

search [1] free-reconfiguration(conf1) =>+ free-reconfiguration(<< < O1 : C1 | property : "connectsTo" = O2, PS1 > < O2 : Client | PS2 > OC >>) .

where conf1 is a constant that represents the initial configuration M in Fig. 1. This command finds a counterexample, conf2 in Fig. 1, where a client component is connected to another client component. An alternative reconfiguration rule can be defined to avoid this problem as shown below, by indicating that the node O5 in the graph patterns of the rule in Fig. 5 is of type Server. No counterexamples are found when running again the search command with the new reconfiguration rule.

Linear temporal logic model checking.

Maude also provides a model checker where properties can be given as linear temporal logic (LTL) formulae [START_REF] Clavel | All About Maude -A High-Performance Logical Framework[END_REF]. Taking into account the safe-reconfiguration rule that has been added to the theory A(M ), we can also model check liveness properties, such as the fact that the server s1 will always have a balanced load L eventually. This property can be formulated in LTL as ♦ balanced ("s1 ", L), where balanced("s1", L) is a state predicate that is satisfied when the server component with name "s1" has L or less connections. Following the guidelines provided in [START_REF] Clavel | All About Maude -A High-Performance Logical Framework[END_REF], we defined a subtheory inclusion to use Maude's model checker, defined in the theory MODEL-CHECKER, into the theory A(M ) that is extended with the rule safe-reconfiguration. The sort Model is defined as subsort of the sort State, used by the model checker to represent system states. The predicate symbol balanced is then defined as a parametric predicate _|=_ between system states and state predicates can be equationally defined for the case in which the state predicate is satisfied: where countBalance is an equationally defined function that counts the number of connections to a given component with identifier O1 in the model M: The model predicate balanced("s1",2) can be used in a LTL formula to model check that the server "s1" will end up with 2 or less connections as follows:

red modelCheck(safe-reconfiguration(conf1), [] <> balanced("s1", 2)) .

Related Work

The meaning of the metamodel notion has been widely discussed in the literature, see for example [START_REF] Ludewig | Models in software engineering -an introduction[END_REF][START_REF] Seidewitz | What models mean. Software[END_REF][START_REF] Kühne | Matters of (meta-) modeling[END_REF][START_REF] Rensink | Subjects, models, languages, transformations[END_REF]. There is a consensus that a metamodel can play several roles: as data, as type or as theory. In this paper, we have formally expressed each of these roles by means of the notions of metamodel M , model type M , and metamodel realization A(M ), respectively.

The current MOF standard does not provide any guidelines to implement a reflective mechanism that obtains the semantics of a metamodel. An informal attempt to realize MOF metamodels as Java programs is provided in the Java Metadata Interface (JMI) specification [START_REF]The Java Metadata Interface (JMI) Specification[END_REF], which is defined for a previous version of the MOF standard. A mapping of this kind has been successfully implemented in modeling environments such as the Eclipse Modeling Framework. By contrast, our A function gives us an executable formal specification of the algebraic semantics of any EMOF metamodel M .

Although EMOF metamodels can be viewed as simplified UML class diagrams, formal approaches for metamodeling need a reflective mechanism, such as A in our approach, to provide the semantics of modeling languages. This mechanism is not needed in UML, where the modeling language is fixed. We focus on several approaches for metamodeling that rely on different formalisms. The Meta-Modeling Language is a meta-circular language based on the MML calculus [START_REF] Clark | The Metamodelling Language Calculus: Foundation Semantics for UML[END_REF], which provides an operational semantics for both UML modeling constructs and OCL operators. Modeling languages can be precisely defined in MML by explicitly specifying its abstract syntax, its semantic domain and a mapping between the concepts involved in both [START_REF] Clark | Engineering modelling languages: A precise meta-modelling approach[END_REF]. This mapping can be viewed as the application of the function A to a specific metamodel M .

Alloy [START_REF] Jackson | Software Abstractions: Logic, Language, and Analysis[END_REF] is a declarative language based on first-order relational logic in which systems with constraints can be modeled. The Alloy analyzer [START_REF]Alloy Analyzer Homepage[END_REF] provides an automated mechanism for constraint satisfaction with two main functionalities: simulation for producing valid instances of an Alloy specification and assertion for verifying constraints. [START_REF] Anastasakis | UML2Alloy: A Challenging Model Transformation[END_REF] provides an encoding of EMOF metamodels with OCL constraints into Alloy so that the Alloy analyzer [START_REF]Alloy Analyzer Homepage[END_REF] is used to generate models that conform to a metamodel (automated test case generation) and to verify that OCL constraints can be satisfied. Counterexamples and logical inconsistencies are found when the constraints are not satisfied. In [START_REF] Anastasakis | Analysis of Model Transformations via Alloy[END_REF], the Alloy analyzer is used to verify relational model transformations in order to ensure that a model transformation cannot produce invalid models. However, Alloy has a simple type system where only integers can be used in attribute values.

In [START_REF] Poernomo | The meta-object facility typed[END_REF], constructive type theory is used for defining a typed metamodeling framework, where models, which are defined as terms, can also be represented as types by means of a reflection mechanism such as A.

In this framework, the conformance relation is implicitly provided by construction: only valid models can be defined as terms, and their definition constitutes a formal proof of the fact that the model belongs to the corresponding type by means of the Curry-Howard isomorphism. The Diagram Predicate Framework, which combines notions from category theory and first-order logic extending the theory of generalized sketches [START_REF] Makkai | Generalized sketches as a framework for completeness theorems[END_REF], has been used to formalize MOF metamodels and their OCL constraints diagrammatically [START_REF] Adrian Rutle | A Diagrammatic Formalisation of MOF-Based Modelling Languages[END_REF]. In this work, the authors illustrate how their approach can be used to formalize software artifacts in several layers of the MOF framework, where the conformance of a model to its metamodel is encoded as a graph morphism.

In the graph transformations field [Roz97, EMK99, EEP06], metamodels are defined as type graphs with node inheritance, and models are defined as attributed typed graphs. The main difference between type graphs and metamodels rely on the use of composition associations in EMOF metamodels, which can be used for defining hierarchies of composite objects in models. A notion of graph with containments is introduced in [START_REF] Biermann | Precise Semantics of EMF Model Transformations by Graph Transformation[END_REF], where the authors show how graph transformations can be used as a formal backend for model transformations. In this way, the theory on graph transformations and related tools can be used to perform formal analysis of model transformations. In particular, the authors show how to analyse termination and confluence of model transformations that are encoded as graph transformations in the algebraic graph transformation environment AGG [Agg09].

There are a number of metamodeling approaches based on Maude. Maude already provides support for object-oriented programming [START_REF] Meseguer | A logical theory of concurrent objects and its realization in the Maude language[END_REF], where objects, the isInstanceOf relation and the class specialization relation are supported. The dynamics of object-oriented systems can be provided by means of term rewriting. The static semantics of the UML metamodel (version 1.3) has been previously formalized as an algebraic specification in mel [START_REF] Fernández | Seamless Formalizing the UML Semantics through Metamodels[END_REF]. In this approach, the authors already took the MOF approach into account, although the MOF standard was in its early stages. In [START_REF] Fernández | Can intuition become rigorous? Foundations for UML model verification tools[END_REF][START_REF] Fernández Alemán | A formalization proposal of the UML four-layered architecture[END_REF], the authors provide a formal fourlayered framework where: (i) some parts of the MOF meta-metamodel are formalized in a mel theory at M3 level (called MOF layer); (ii) the UML class diagram and the object diagram metamodels are provided as mel theories, called syntactic specification and semantic specification respectively, at M2 level (called UML metamodel layer); (iii) UML class diagrams are defined as terms in the syntactic specification theory at M1 level (called domain model layer); and (iv) object diagrams are defined as terms in the semantic specification theory at M0-level (named user objects layer). A novel feature in this approach relies on the reuse of the reflective facilities of mel to provide support for the evolution of UML-based software artifacts [START_REF] Toval | Formally modeling uml and its evolution: a holistic approach[END_REF]. The authors focused on the verification of static properties by using Maude as an implementation of mel and the language to define the constraints.

Another approach [START_REF] Romero | Formal and Tool Support for Model Driven Engineering with Maude[END_REF] based on Maude uses the KM3 language [START_REF] Jouault | Km3: A dsl for metamodel specification[END_REF] for indirectly defining EMOF metamodels. In this work, the authors present how KM3 specifications of metamodels can be represented as object modules [START_REF] Clavel | All About Maude -A High-Performance Logical Framework[END_REF] in Full-Maude and how models can be defined as Maude collections of objects. However, no automated support is provided for representing models as terms since KM3 only permits defining the textual concrete syntax of metamodels. That is, mappings like rep -1 and rep are not defined for models that conform to metamodels that are extracted from KM3 specifications. In this way, the user has to define the models in Maude notation directly. The authors provide a mechanism to represent KM3 specifications of metamodels as collections of objects at a syntactic level so that Maude is used to statically analyse KM3 specifications: to check when two metamodels describe model subtypes, to infer metamodels from models and to compute metrics. However, model types are not algebraically characterized. Since KM3 metamodels can be represented in EMF automatically, KM3 metamodels can also be formalized through MOMENT2.

Our algebraic semantics A for EMOF metamodels M in mel formally defines the notions of metamodel realization A(M ), model type M and model conformance M : M . This means that A enables reasoning with model types at an algebraic level and not just at a syntactical level. Due to the graph nature of models, the algebraic semantics A for MOF can also be used as an algebraic environment for graph transformations, where Maude's analysis capabilities, such as reachability analysis and LTL model checking, can be reused. The complete algebraic formalization of EMOF metamodels together with OCL can be found in [START_REF] Boronat | Algebraic Semantics of OCL-constrained Metamodel Specifications[END_REF][START_REF] Boronat | MOMENT: a formal framework for MOdel manageMENT[END_REF],

where composition associations are also taken into account in the formalization. The algebraic semantics A is implemented in MOMENT2 where EMF is used as implementation of the EMOF standard. Furthermore, the generic mappings rep and rep -1 allow representing EMF models as terms in MOMENT2 in a transparent way to the user. This is an essential feature in MOMENT2, where the goal is to apply Maude for formal model management tasks by using OMG standards, such as MOF, OCL and QVT.

Conclusions and Future Work

In this work we have proposed an algebraic semantics for the MOF metamodeling framework, formalizing notions not yet clear in the MOF standard. In our approach, we give an explicit formal representation for each of the different notions that may be involved in a metamodeling framework: metamodel realization A(M ), model type M , and metamodel conformance M : M . Our work provides an algebraic executable formalization of the MOF standard that can be reused in standard-compliant frameworks.

This algebraic framework opens a wide spectrum of interesting applications for model-driven development. In particular, we have shown how it can be used for automatically checking metamodel conformance, defining domain-specific languages and specifying model transformations and model management operators. In addition, Maude's formal verification facilities can be used for static and dynamic analysis of domainspecific languages, such as checking constraints over models, reachability analysis and LTL model checking.

The algebraic semantics for MOF provides the foundational notions for a model management tool suite, MOMENT2 [START_REF][END_REF], that supports both OCL [START_REF] Boronat | Algebraic Semantics of OCL-constrained Metamodel Specifications[END_REF] and QVT-like model transformations [START_REF] Boronat | Rewriting Logic Semantics and Verification of Model Transformations[END_REF]. MOMENT2 uses MOF, OCL and a QVT-like model transformation language as interface, so that the techniques that have been illustrated in this work are internally used in a transparent way to the user. For the development of this framework, we have relied on the experience gained in previous prototypes that gave algebraic executable specifications for OCL [START_REF] Boronat | An Algebraic Specification of Generic OCL Queries Within the Eclipse Modeling Framework[END_REF], QVT [BCR06] and model management operators [START_REF] Boronat | Automatic Support for Traceability in a Generic Model Management Framework[END_REF]BCR06]. In addition, grammar-based software artifacts can also be related to models by specifying context-free grammars as mel signatures. This last feature makes our framework also suitable for forward and reverse model-driven engineering.

In future work, we plan to apply the algebraic MOF framework together with the aforementioned tool for model transformations and Maude-based formal reasoning techniques in model-driven development scenarios, where software systems that are developed contain critical properties that have to be verified. In particular, we are considering the formal analysis of real-time embedded systems in the avionics domain, by using model-based languages like the Architecture Analysis and Design Language (AADL) [SAE07].

---ii) op propertyValidType : Cid Property -> Bool . eq propertyValidType( C, property : PN ) = true . eq propertyValidType( C, property : PN = V:Collection+{String} ) = IsStringProperty(metaProp(C, PN)) . ---more equations deal with other built-in types ---iii) op propertyValidCardinality : Cid Property -> Bool . eq propertyValidCardinality( C, class : ClassName ) = true .

---no value eq propertyValidCardinality( C, property : PN ) = (metaProp(C, PN) . getInt( "lowerBound" ) == 0) .

---only 1 value eq propertyValidCardinality( C, property : PN = V:MetaOid) = ((metaProp(C, PN) . getInt( "lowerBound" )) <= 1) and-then ((metaProp(C, PN) . getInt( "upperBound" )) == 1) .

---more than one value eq propertyValidCardinality( C, property : PN = V:Collection{Oid}) = ((metaProp(C, PN) . getInt( "lowerBound" )) <= (V:Collection{Oid} -> size)) and ( ((metaProp(C, PN) . getInt( "upperBound" )) == -1 ) or ((metaProp(C, PN) . getInt( "upperBound" )) >= (V:Collection{Oid} -> size)) ) .

Fig. 1 .

 1 Fig. 1. The MOF framework.

  sorts ObjCol Model . subsort Model < ObjCol . op none : -> ObjCol . op __ : ObjCol ObjCol -> ObjCol [assoc comm id: none] . op <<_>> : ObjCol -> [Model] .

  mb << none >> : Model . cmb << OC >> : Model if ( OC =/= none ) and uniqueOid( OC ) and noDuplicateProperties( OC ) and noDanglingEdges( OC ) and singleContainer( OC ) and validProperties( OC ) .

Fig. 2 .

 2 Fig. 2. Metamodel M viewed as a graph and as a term.

Fig. 5 .

 5 Fig. 5. Reconfiguration rule.

  op free-reconfiguration : Model -> Model . crl free-reconfiguration(M) => free-reconfiguration(<< < O1 : C1 | PS1 > < O2 : C2 | property : "connectsTo" = O1, PS2 > < O3 : C3 | property : "connectsTo" = O1, PS3 > < O4 : C4 | property : "connectsTo" = O5, PS4 > < O5 : C5 | PS5 > OC >>) if << < O1 : C1 | PS1 > < O2 : C2 | property : "connectsTo" = O1, PS2 > < O3 : C3 | property : "connectsTo" = O1, PS3 > < O4 : C4 | property : "connectsTo" = O1, PS4 > < O5 : C5 | PS5 > OC >> := M ∧ nac(O5, M) .

Fig. 6 .

 6 Fig. 6. Traceability metamodel T and its algebraic realization A(T ).

  op match : Model Model -> ModelTrac . eq match(M1,M2) = $match(M1,M2,init-trac,0) . op $match : Model Model ModelTrac Nat -> ModelTrac . eq $match( << < O1 : C1 | property : "name" = Name, PS1 > OC1 >>, << < O2 : C2 | property : "name" = Name, PS2 > OC2 >>, << < O3 : TModel | property : "links" = Set, PS3 > OC3 >>, N ) = $match( << OC1 >>, << OC2 >>, << < O3 : TModel | property : "links" = Set -> including( getNewOid(N) ), PS3 > < getNewOid(N) : TMapping | domain : O1, range : O2 > OC3 >>, N + 1 ) . eq $match(M1,M2,TM, N) = TM [owise] .

Fig. 7 .

 7 Fig. 7. Trace model and its term representation.

  op checkClientServer : Model Bool . eq checkClientServer( << < O1 : C1 | property : "connectsTo" = O2, PS1 > < O2 : Client | PS2 > OC >> ) = false . eq checkClientServer( M:Model ) = true [owise] .

  op safe-reconfiguration : Model -> Model . crl safe-reconfiguration(M) => safe-reconfiguration(<< < O1 : C1 | PS1 > < O2 : C2 | property : "connectsTo" = O1, PS2 > < O3 : C3 | property : "connectsTo" = O1, PS3 > < O4 : C4 | property : "connectsTo" = O5, PS4 > < O5 : Server | PS5 > OC >>) if << < O1 : C1 | PS1 > < O2 : C2 | property : "connectsTo" = O1, PS2 > < O3 : C3 | property : "connectsTo" = O1, PS3 > < O4 : C4 | property : "connectsTo" = O1, PS4 > < O5 : Server | PS5 > OC >> := M / nac(O5, M) .

  subsort Model < State . op balanced : String Nat -> Prop . eq free-reconfiguration( << < O1 : Server | property : "name" = Name, PS1 > OC >> ) |= balanced(Name, L) = (countBalance(O1, << < O1 : Server | property : "name" = Name, PS1 > OC >>) <= L) .

  op countBalance : Oid Model -> Nat . eq countBalance( O1, << < O2 : C2 | property : "connectsTo" = O1, PS2 > OC >> ) = 1 + countBalance(O1, << OC >>) . eq countBalance( O1, M ) = 0 [owise] .

Table 1 .

 1 OCL types for encoding multiplicity constraints in properties. Given a MOF-conformant metamodel M : MOF, and given an object class named C in M :

	Type	Lower Bound Upper Bound isOrdered isUnique
	∅, Oid	0	1	-	-
	Set{Oid}	0	*	false	true
	OrderedSetOid}	0	*	true	true
	Bag{Oid}	0	*	false	false
	Sequence{Oid}	0	*	true	false
	Oid	1	1	-	-
	NeSet{Oid}	1	*	false	true
	NeOrderedSetOid}	1	*	true	true
	NeBag{Oid}	1	*	false	false
	NeSequence{Oid}	1	*	true	false
	Definition 1.

In the MOF framework, the concept of a model M is conceptually specialized depending on the specific metalevel, in which a model is located: model at level M1, metamodel at level M2 and meta-metamodel at level M3; as shown below.

In the dissertation, the A function is denoted by reflect MOF .

This binary operator symbol has empty syntax (juxtaposition).

Association ends are defined, in the MOF standard[START_REF] Omg | Meta Object Facility (MOF) 2.0 Core Specification[END_REF], as properties that are owned by the class from which they can be navigated. This notion was called Reference in previous versions of the MOF standard and it is called EReference in the EMF.

We represent the name of the Property class as Prop to avoid name collisions with the aforementioned sort Property.

This bridge uses the API of the Maude Development Tools[START_REF]Maude Development Tools[END_REF] for integrating Maude into Eclipse.

In EMF terminology, a metamodel at M2 is an EMF model and a model at M1 is an EMF model instance.

Recall from Section 3 that layer 0 is the meta-metamodel layer M3 of MOF, layer 1 is the layer M2 of metamodels M ∈ MOF , and layer 2 is the layer M1 of models M ∈ M .

An updated version with the new XText framework is ongoing work.

We have removed the types of the variables in the RHS of the command (after the =>+ symbol) for the sake of simplicity.

Acknowledgments.

We thank the anonymous referees for their comments and suggestions that have helped us to improve the exposition. This work has been partially supported by the project META TIN2006-15175-C05-01, by the ONR Grant N00014-02-1-0715, by NSF Grant IIS-07-20482, and by the project SENSORIA, IST-2005-016004.