Low-code software development promises rapid delivery of software cloud applications by employing domain-specific languages (DSLs), requiring minimal traditional coding. Model-driven engineering (MDE) provides tools, modelling notations and practices suited for engineering such DSLs, both from a syntactic and semantic perspective. However, low-code software development is heavily reliant on software reuse. It is imperative to provide safe mechanisms that guarantee valid semantic reuse of structural components and their behaviour, most often in a stepwise manner. This article presents a semantic reuse technique based on model subtyping over metamodels to manage correct model-driven engineering of DSLs. Model subtyping is generalized to structural semantics by considering OCL constraints. Moreover, model subtyping is generalized to behavioural semantics by considering specifications of model transformation operations, which may encode operational or translational semantics. Model subtyping facilitates structural and behavioural refinement. It has been implemented atop a bounded model checker, realizing a semi-decidable procedure for verifying that DSL elements are safely reused. The algorithm finds semantic witnesses of inconsistencies when refinement principles are not satisfied, fostering a correct stepwise engineering of DSLs. Moreover, the algorithm produces an extension metamodel that permits the as-is reuse of implementations of model transformation operation specifications. Finally, the versatility of the model subtyping technique is illustrated with common use cases extracted from the research literature.
Notes
Communicated by Romina Eramo, Benoit Combemale and Juan de Lara.
Publisher's Note
Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.
1 Introduction
Software reuse [1] is a recommended software engineering strategy that builds new systems on top of existing software artefacts. Such strategy is driven by a need to cope with increasingly complex software while lowering software development costs, shortening delivery times, and improving software quality. Low-code and no-code software development epitomizes current approaches to reuse-based software engineering [2], where software systems are designed using domain-specific languages (DSLs) so that they can readily be deployed on the cloud as a service, with little or no traditional coding required. Correct engineering of low-code platforms is critical to ensure the quality of the generated software applications.
The design principles and practices involved in low-code software development overlap greatly with those in model-driven engineering (MDE) [3]. The structural semantics of domain-specific modelling languages is represented in terms of metamodel specifications, involving a metamodel and possibly additional constraints [4], and their behavioural semantics is represented by model transformation operations, like model interpreters and model compilers. As low-code development platforms become sophisticated, such metamodel specifications and model transformations grow complex and reuse techniques become vital for engineering them correctly. Specially when those reuse techniques come equipped with automated verification support.
Advertisement
A very general form of reuse emerges when we want to learn whether we can extrapolate model transformation operations from one metamodel specification to another one or when we want to engineer a model transformation based on an existing one. On the one hand, (i) when a model transformation is to be applied to a different metamodel specification, whose metamodel and constraints need not be related a priori, involves learning whether the original and new metamodel specifications are compatible, capturing the notion of subtype polymorphism in model transformation operations. On the other hand, reusing model transformations to engineer new ones involves analysing how they are related. In particular, we can find two additional common use cases: (ii) when a model transformation can be safely reused across DSLs; and (iii) when the specification of a model transformation is refined stepwise, reusing and extending the original set of requirements. In all of these cases, appropriate automated verification mechanisms should be provided to ensure the safe reuse of model transformation operations. Specifically, we are interested in ensuring two types of safety properties (nothing bad can happen): invariants, which need to hold for all states (or execution configurations) of the interpreter, and behavioural requirements, which need to hold for all transformation steps.
Depending on how typing is considered [5], we can distinguish semantics where typing (the instanceOf relation) is ontological, explicitly definable in the metamodelling language, or linguistic, implicitly defined by the metamodelling language. In addition, we consider that the semantics of object subtyping corresponds to (static) subclassing—generalization—in the first approach; and subsumption in the second approach. Hence, we distinguish approaches where models are represented as graphs, where typing is ontological; or as terms, where typing is linguistic. On the one hand, graph transformation theory and well-known (meta)modelling environments, such as the Eclipse Modelling Framework (EMF) and the USE environment [6, 7], rely on the first representation, exploiting a set-theoretic representation to implement tools, e.g. for checking model typing and for analysing (OCL) constraints. On the other hand, type-theoretic approaches, such as [8, 9], rely on the second representation for exploiting inductive reasoning and higher-order functions.
Our aim in this work is to revisit the research question of whether type subsumption—i.e. the relation capturing that any inhabitant of a given subtype is also an inhabitant of a given supertype—is a valid mechanism for facilitating reuse of model transformation operations in MDE in order to analyse its advantages and limitations. We approach this topic by tackling the three different reuse problems above in modelling language engineering, which we then solve by using structural and behavioural model subtyping. The following results have been developed to solve these reuse problems:
(1)
Extension of OO types, with multiple inheritance semantics [10], to model types with referential constraints, reusing a type-theoretic framework, with linguistic typing and a convenient semantics for subtyping. Our model types formalize the common features of EMF metamodels, including classes with attributes, cross-references and containments, multiple inheritance, data types and enumeration types, multiplicity, ordering, uniqueness and bidirectionality constraints for cross-references and containments.
(2)
Attachment of the USE semantics of OCL constraints [11], with ontological typing, to extended OO types in order to reuse tool support for mechanizing the satisfaction of OCL constraints in our model types.
(3)
Definition of a subtyping relation \(\le :\) between metamodel specifications that couples extended OO subtyping, between the types in both metamodels, with the compatibility of their OCL constraints. This subtyping relation can be regarded as a structural refinement relation between metamodel specifications. The computation of the subtyping relation for two given metamodel specifications relies on the construction of an extension metamodel that reflects (linguistic) model subtyping using (ontological) subtyping, enabling reasoning about the compatibility of OCL constraints from both metamodel specifications. The extension metamodel also serves as the basis for reusing model transformation operations as-is, i.e. without introducing changes to the operation behaviour.
(4)
A semi-decidable procedure that solves the proposed problem by using structural model subtyping and its implementation in a tool, facilitating flexibility in MDE by supporting dynamic, partial and multiple typing.
The subtyping relation has been generalized in Sect. 5.5 to behavioural specifications of model transformations, both syntactically and semantically, enabling (i) safe application of operations, (ii) substitutability of operations that satisfy the same set of requirements, and (iii) refinement of model transformation specifications.
(6)
A semi-decidable procedure in Sect. 5.5 implements the satisfiability of the subtyping relation, automatically verifying (i) application of model transformation operations, (ii) their substitutability, and (iii) stepwise refinement of transformation specifications.
(7)
Re-typing and type coercion mechanisms are explained in more detail using the EMF-Syncer [13] in Sect. 6.4.
(8)
A number of use cases in Sect. 7 illustrate the different possibilities of the subtyping relation, including structural and behavioural refinement, and multiple typing.
The structure of the rest of the article is as follows. In Sect. 2, we introduce an example and discuss approaches for model typing, focusing on accepted notions of model subtyping for EMF metamodels and graph transformation theory. In Sect. 3, the main approaches to model subtyping are introduced. In Sect. 4, syntactic representations for model types and structural model subtyping are introduced. In Sect. 5, we map a semantics of metamodels specifications to our model types and extend the subtyping relation to metamodel specifications and operation specifications. In Sect. 6, we present how the tool provides support for the theory developed. In Sect. 7, the subtyping relation is illustrated with additional use cases. In Sect. 8, we compare our approach to related work, finalizing the work with concluding remarks.
2 Running example
A low-code development platform usually builds atop a surface modelling language, with which a modeller designs a system in a particular domain. The language’s abstract syntax is given as a metamodel, which may be enriched with constraints, specifying structural properties that need to be satisfied by its models. This metamodel specification [4], formed by a metamodel and its OCL constraints, characterizes the structural semantics of the DSL. Traditionally, the behavioural semantics of a DSL is either operational or translational. Operational semantics can be specified declaratively using in-place model transformations in a model interpreter, while translational semantics can be implemented using out-place model transformations in a model compiler.
Advertisement
In the following subsections, we develop a running example in which an abstract specification of a graph-based DSL for evaluating functions is reused, and refined, for engineering a simulator for state machines.
2.1 Reuse of structural requirements
The metamodel specifications \((\mathcal {M}_g,\Omega _g)\) and \((\mathcal {M}_{sm},\Omega _{sm})\), shown in Fig. 1, define modelling languages for abstract graphs and deterministic state machines, respectively. The model types described by both metamodels are structurally similar in that they both describe graphical forms. On the one hand, \((\mathcal {M}_g,\Omega _g)\) characterizes the graph of a function defined over nodes, with the OCL constraint \(\Omega _g\). On the other hand, \((\mathcal {M}_{sm},\Omega _{sm})\) characterizes state machines where transitions can be triggered by an event (indicated in the
attribute of the transition) or are triggerless, e.g. they are completion transitions. These metamodels also include notions for engineering the execution context of a model interpreter, namely the notions of
to mark nodes as already mapped in \(\mathcal {M}_g\), and
to indicate which states have been observed in \(\mathcal {M}_{sm}\).
By showing that the abstract graph DSL is a subtype of the state machine DSL,
the requirement that abstract graphs define maps can be reused in the context of state machines, where the requirement imposes determinism on the representable state machines. Furthermore, the subtyping operator also checks whether any additional constraints in the metamodel specification \((\mathcal {M}_{sm},\Omega _{sm})\) are compatible with the constraints \(\Omega _g\), ensuring that \((\mathcal {M}_{sm},\Omega _{sm})\) is a valid structural refinement of \((\mathcal {M}_{g},\Omega _{g})\).
Our notion of subtyping can compare metamodels that are not related a priori by exploiting structural similarities. However, it is most effective when applied to metamodels with known similarities, say as a consequence of evolution, because those similarities are automatically inferred, easing the language engineer’s reuse task.
2.2 Reuse of model transformation operations
To consider the behavioural semantics of DSLs, we are introducing an ATL transformation that defines a basic interpreter for evaluating functions defined according to the metamodel specification \((\mathcal {M}_g,\Omega _g)\). The ATL transformation applies a function graph to a node, as shown in Listing 1. The interface of the interpreter is given in terms of the metamodel specification \((\mathcal {M}_g,\Omega _g)\). By extending this interface with the metamodel specification \((\mathcal {M}_{sm},\Omega _{sm})\) via the subtyping operator, the interpreter can be safely reused for state machines.
×
Figure 2 shows one simulation step carried out with the ATL transformation applied to an initial state machine, with an observation of the initial state. The simulation step adds a marking on the successor state with a new timestamp. The marking is an instance of the class
as the ATL transformation has no awareness of the classifiers in the subtype model. Type coercion is used in the last step to down cast the resulting state machine to an instance of the subtype model, by retyping object
to the class
.
Fig. 2
Simulation trace and type coercion
×
2.3 Stepwise refinement
In the previous reuse use case, the interpreter is defined using the metamodel specification \((\mathcal {M}_g,\Omega _g)\) as its interface. Thereby, the interpreter is reused for \((\mathcal {M}_{sm},\Omega _{sm})\) as a blackbox. As explained by Liskov and Wing [14], the subtyping operation only guarantees that the entire space of side effects of the interpreter function within \((\mathcal {M}_{sm},\Omega _{sm})\) is also present within \((\mathcal {M}_{g},\Omega _{g})\). That is, that no type errors occur. However, this type of reuse shows very little knowledge about the actual behaviour of the operation. In this section, the specification of the interpreter is refined, for an extension of the metamodel specification \((\mathcal {M}_{sm},\Omega _{sm})\), with additional constraints that describe the actual behaviour of the simulator of state machines.
Figure 3 shows a refined metamodel specification \((\mathcal {M}_{sm'},\Omega _{sm'})\) (top) that includes temporal information via the association
. In its metamodel, the classifier
corresponds to the snapshot notion, which contains a marker for the state currently being observed. In addition, each state machine may have one predecessor, representing the previous snapshot in the execution. The invariant (top, right) specifies the behavioural semantics of the interpretation model transformation in Listing 11. Figure 3 shows the semantics of the model interpreter (bottom), consisting of two transformations, given an initial state machine snapshot. Hence, by comparing metamodel specifications that contain behavioural semantics, the subtyping operation is also able to reason about behavioural properties of DSLs, both to reuse behavioural semantics and to ensure valid behavioural refinements. This example has been chosen to illustrate how the operation specification subtyping relation can be used to check refinement of model transformation operations. However, the operation specification subtyping relation is more general, as it does not require an initial snapshot to determine whether subtyping is satisfied.
Fig. 3
Operation specifications: subtype (top left) and supertype (top right); traces starting at a given state machine (bottom)
×
3 Background on model subtyping
In the recent literature on model transformation, there is an emerging interest in formalizing mechanisms for reuse of model transformations [15‐17]. Approaches to reuse transformation logic involve mechanisms to facilitate its application in different contexts (through typing) or by extending the logic itself (through transformation rule extension). We will focus on the first one, while laying the foundations for the second one, to study when it is safe to reuse a model transformation operation.
Regarding typing, working with models in MDE processes can be done at two levels of abstraction: a white-box approach (called intra-resource in [18]) where model internals are exposed so that side effects can be analysed as model transformations act upon models; and a more coarse (blackbox) approach (called inter-resource in [18]) where models are treated as first-order citizens in model transformation scenarios [3]. Depending on the desired level of rigour, the former may be regarded as a building block to enable a sound basis for the latter, i.e. by building model management systems based on safe model transformations. Refining this classification around the notion of intra-resource typing, we find approaches that build on a notion of model type, typically considering model subtyping or metamodel adaptation, out of which we are interested in subtyping only.
Model subtyping can be dealt with as a subsumption relation or as model type matching, by generalizing the homologous notions in OO programming languages [19]. Steel et al. [20] proposed a type system with type groups in order to formalize the type of a metamodel. Substitutability in this type system is facilitated by a model type matching relation, which generalizes the matching relation on type groups presented in [21] to model types, where a model type M’ matches a model type M, denoted \(\texttt {M'}<\# \; \texttt {M}\), iff for each class C in M, there is a class C in M’ such that the signature of its operations is preserved2. The type system proposed relies on class names to match object types, which implies that the model type for state machines of Fig. 1 would not be considered a subtype of the model type for graphs without an explicit adaptation.
In [20], the authors argue that a name-independent structural type system is not able to capture classes with no contents that are solely used for adding structure to a concept taxonomy, e.g. by denoting final states in a state machine. From a design point of view, the use of empty classes may be helpful for modelling new concepts at an early stage in the development process. However, this may be considered a design smell for implementation purposes, as it violates the single-responsibility principle. In addition, there are alternative modelling techniques that permit skipping that case without losing expressive power. For example, one may consider clustering a hierarchy of empty children classes into the superclass by adding a segregative attribute (e.g. a Boolean attribute
) or by designating different types of classes by using references (e.g. by using a reference
from the class
to the class
).
Guy et al. improved this notion of subtyping as isomorphic model subtyping in [17] and introduced non-isomorphic model subtyping for enabling model adaptation utilizing renaming maps. Guy et al. [17] also discuss the notion of partial and total subtyping in order to facilitate the reuse of model transformations in practical scenarios. Partial model subtyping aims to enable the safe reuse of a model transformation even if only the part of the model type used in the model transformation is present. In this context, Sen et al. [22, 23] conceptualized this situation as the notion of effective model type of a transformation: the minimal subset of the elements of the input metamodel that is used in the transformation.
Model transformations based on graph transformation theory rely on the theory of typed attributed graphs with type node inheritance [24, 25]. Type checking in this theory is achieved by constructing a graph morphism between a graph (the model) and the type graph (the metamodel) that preserves the graph’s structure. Model subtyping is supported in graph transformations employing the notion of abstract production rule where nodes in a graph pattern in the rule may correspond to abstract nodes (similar to an abstract superclass). From a theoretical point of view, given a graph and an abstract production rule that can be applied to it, it has been shown that a unique concrete production rule can be constructed so that the effects of the transformation on the graph are equivalent to the application of abstract production rule directly on the graph. Hence, the usual theory for typed attributed graph transformation can be applied for graph grammars with abstract production rules, with a notion of object subtyping. Using this theory, the type graphs representing the metamodels in Fig. 1 denote different types of graphs that are not related unless adaptation mechanisms are used explicitly.
4 Model types and subtyping
One of the contributions of this work consists in giving an interpretation to metamodels (and object-oriented models), where refinement extension is achieved by (static) subclassing, with model types where refinement is achieved by subtyping (subsumption). To distinguish both kinds of type representations, we are going to use \(\mathcal {M}^{\rightarrow }_{}\) to denote metamodels and \(\mathcal {M}^{<}_{}\) to denote model type expressions. This distinction is necessary in order to consider OCL constraints in model types, as discussed in the following section.
In this section, we first introduce model type expressions \(\mathcal {M}^{<}_{}\) for representing model types \(\mathopen {\llbracket }{\mathcal {M}^{<}_{}}\mathclose {\rrbracket }\) and, subsequently, define them. Then, we define a notion of model subtyping based on subsumption. In Sect. 5, we show how a metamodel \(\mathcal {M}^{\rightarrow }_{}\) is related to its model type expression \(\mathcal {M}^{<}_{}.\)
4.1 Model type expressions
Models in software engineering have a dual interpretation, namely as “a related collection of instances of metaobjects, representing (describing or prescribing) an information system, or parts thereof, such as a software product or as semantics”, or as “a semantically closed abstraction of a system or a complete description of a system from a particular perspective” [26]. That is, as syntax or as semantics [27]. Since metamodels are also models, we differentiate a metamodel from a model type by saying that a metamodel denotes a unique model type [28, 29].
Our model types are used as classifiers of objects, and their operations are applied to models, even if they act on the internals of the model representation. For example, a model transformation may consist of a sequence of updates of property values or alter the structure of the model.
In [10], record types are used to model classes of objects, and thus object types, and union types define tagged values. That is, whereas an record type (name: String) denotes objects with a property name, a union type [red : [], blue: [], green: []] defines the type of those values that contain a single literal, defining an enumeration type. In the following, we extend the syntax for types presented in [10], by including referential types and by including notation both for the types themselves and for their name. The reason for this is to enable the definition of recursive structures through referential types.
Definition 1
(Extended syntax for types) Given the countable sets \(\mathcal {B} = \{ Oid , Bool , String , Int , Float \}\) of base type names b, \(\mathcal {E}\) of enumeration type names \(\epsilon \), \(\mathcal {C}\) of class names \( c \), \(\mathcal {P}\) of property names p, the set \(\tau \) of types over \(\mathcal {B},\)\(\mathcal {E},\)\(\mathcal {C}\) and \(\mathcal {P},\) is defined as follows
where \(n\in \mathbf {N}\) and \(m\in \mathbf {N}\cup \{*\}\).
\([]\) denotes the bottom type as the least informative type, \(\texttt {Void}\) denotes its name, \(()\) denotes the most general type, \(\texttt {Any}\) denotes its name, and \(\tau \rightarrow \tau \) denotes the type of a function. Optional sentential forms are denoted with grouping parentheses and a question mark.
We will use the Boolean predicates \( isRef (\rho )\), \( isCmt (\rho ),\)\( isOrdered (\rho )\) and \( isUnique (\rho )\) to check whether a property type expression is a cross-reference type expression or a containment reference type, whether it is ordered and whether it is unique, respectively. In addition, the projections \( c (\rho ),\)\( lower (\rho ),\)\( upper (\rho ),\) and \( op (\rho )\) obtain the class name, the lower bound, the upper bound and the opposite property name (when present), respectively.
\(p_1 : \alpha _1,\ldots ,p_n : \alpha _n\) corresponds to a set of structural features, where attributes are defined as properties of the form \( p : b\) or \( p : \epsilon ,\) cross-references pointing to a class \( c \) are defined as properties of the form
$$\begin{aligned} p : ref \, ( unique )? \, ( ordered )? \, c [n..m](\# p )? \end{aligned}$$
and containments pointing to a class \( c \) are defined as properties of the form \( p : ( unique )? \, ( ordered )? \, c [n..m](\# p )?.\)
Definition 2
(Model Type Expression)
Given finite sets \(\mathcal {B}\) of base type names b, \(\mathcal {C}\) of class names \( c \), \(\mathcal {E}\) of enumeration names \(\epsilon \) and \(\mathcal {P}\) of property names \( p \), a model type expression \(\mathcal {M}^{<}_{}\) is defined as a tuple \(( type , roots )\) where: \( type \) is an injective function mapping each class name \( c \) to a corresponding object type \(\varsigma \) of the form \((p_1 : \alpha _1,\dots ,p_n : \alpha _n),\) specifying the structure of the objects of class \( c ,\) each enumeration type name \(\epsilon \), denoting an enumeration of literals \( l _1,\dots , l _n,\) to a union type of the form \([ l _1 : [], \ldots , l _n : []]\), \(\texttt {Any}\) to \(()\), and \(\texttt {Void}\) to \([];\)\( roots \subseteq \mathcal {C}\) are the names that designate the root metaclasses in the metamodel inducing the union type \([ \bigcup _{c\in roots } (c : unique \; c [0..*])]\), which we denote by \(\mu (\mathcal {M}^{<}_{})\).
In our approach, a model may consist of heterogeneous root objects. When considering models in a purely graph-theoretic sense, one needs to consider all classes as roots. The model type expression corresponding to the state machine metamodel of Figure1 has the root class name
and
is defined as follows:
×
4.2 Semantics of model type expressions
We borrow the semantic domain from [10], where \({\textbf {V}}\) is the universal value domain of all computable values. We consider that \({\textbf {V}}\) contains the set of typed object identifiers \(\mathcal {O}\) and refer to object identifiers of objects that are instances of a particular class c as \(\mathcal {O}_c\).
We refine the semantics for type expressions as model type expressions in order to consider referential types and the different types of constraints definable in a metamodel. The semantics of a referential type expression \(\rho \) of the form
$$\begin{aligned} p : ( ref )? \, ( unique )? \, ( ordered )? \, ( c \, | \,\texttt {Any})[n..m](\# p ')? \end{aligned}$$
is given by the expression \(\mathopen {\llbracket }{\rho }\mathclose {\rrbracket }_{r}\) where r is an optional parameter referring to the record containing the field \( p .\) The expression \(\mathopen {\llbracket }{\rho }\mathclose {\rrbracket }_{r}\) is defined as follows:
If \(\rho \) denotes a referential type (with prefix \( ref \)) of c that is ordered, then the type is \(\mathopen {\llbracket }{List(\mathcal {O}_c)}\mathclose {\rrbracket }\), where \(List(\mathcal {O}_c)\) can be regarded as the space of injective functions \(\mathbf {N} \rightarrow \mathcal {O}_c\) (where \(\mathbf {N} \subseteq {\textbf {V}}\) is the set of natural numbers and the index determines the ordering). If it is not ordered, then the type is \(\mathopen {\llbracket }{Bag(\mathcal {O}_c)}\mathclose {\rrbracket }\), where \(Bag(\mathcal {O}_c)\) can be regarded as the space of non-injective functions \(\mathbf {N} \rightarrow \mathcal {O}_c,\) where the index is only used to distinguish different occurrences of the same value.
Otherwise, \(\rho \) denotes a containment type (an object type) of class c and if it is ordered, then the type is \(\mathopen {\llbracket }{List( type (c))}\mathclose {\rrbracket }\), where \(List( type (c))\) can be regarded as the space of injective functions \(\mathbf {N} \rightarrow type (c)\). In this case, the domain \( type (c)\) of such functions is the class of objects of type c and not just a set of references. Likewise, if it is not ordered, the type is \(\mathopen {\llbracket }{Bag( type (c))}\mathclose {\rrbracket }.\)
Also, there may be constraints regarding multiplicities, uniqueness and bidirectionality that restrict the corresponding referential types. Such constraints are encoded as follows:
For referential types, assuming we have a collection of identifiers \( ic \) (either a list or a bag), multiplicity constraints [n..m] are encoded as follows \(| ic | \ge n \;\wedge \; (| ic | \le m \;\vee \; | ic |=*).\) The constraint is encoded likewise for containment types.
For referential types, assuming we have a collection of identifiers \( ic \) (either a list or a bag), the uniqueness constraint is encoded as follows \(| ic |=| set( ic ) |\), where set is the operator that extracts a set from a list or a bag by filtering out duplicates. The constraint is encoded likewise for containment types.
For referential types, when the parameter r in \(\mathopen {\llbracket }{\rho }\mathclose {\rrbracket }_r\) is present, the bidirectionality constraint \(p : ref c[n..m]\#p'\), where \(p(r)= ic \)3 is encoded as follows . For containment types, the constraint is encoded likewise, but we fetch the object identifier of the contained object by inspecting the field \( id \).
For a property \( p : \alpha \) defined in an object type \(\varsigma \), a full encoding of the semantics denoted by the expression \(\mathopen {\llbracket }{\alpha }\mathclose {\rrbracket }_r\), where \(r \in \mathopen {\llbracket }{\varsigma }\mathclose {\rrbracket }\), can be obtained by enumerating the 16 combinations of constraints definable in referential and containment type expressions in addition to the cases for attributes.
For defining model types, we consider the universal value domain \({\textbf {V}}\) of all computable values, the domain \(\mathbf {R}\) of records, the domain \(\mu \) of union values (variants) and the set \(\mathbf {F}\) of continuous functions \(f\) from \({\textbf {V}}\) to \({\textbf {V}}\). We refine the semantics for type expressions as model type expressions in order to consider referential types and the different types of constraints definable in a metamodel as follows:
where the notation \(\langle p, q \rangle \) denotes pairs of values p and q.
4.3 Model subtyping
In this section, we extend the object subtyping (subsumption) relation [10] to model types. Model subtyping emerges from object subtyping, and it is implicitly defined when a pair of model type expressions are given.
To extend the subtyping relation, we need to introduce how referential types and containment types are related by means of an incompatibility relation. To do so, we use the incompatibility relation
which captures the subtyping violations (regarding multiplicities, ordering, uniqueness and bidirectionality) between two property type expressions. That is, an object type expression \(\varsigma _1\) containing a referential type expression \( p : \alpha _1\) that is incompatible with a referential type expression \( p : \alpha _2\), with the same name \( p \), of another object type expression \(\varsigma _2\) means that \(\varsigma _1\) does not denote a subtype of the type denoted by \(\varsigma _2\). The incompatibility relation \( \, \not \sim \, \) is defined as follows4:
where \( \, \not \le :_{} \, \) denotes the negation of the subtyping relation between class names as defined below.
Given two model types \(\mathcal {M}^{<}_{ sub }\) and \(\mathcal {M}^{<}_{ super },\) the extended subtyping relation \( \, \le :_{\beta } \, \;\subseteq \; \mathbf {Type}\times \mathbf {Type}\), where \(\beta \subseteq \mathcal {C}\times \mathcal {C}\) captures the names of those object types that have been related already, is defined as shown in Fig. 4. Whenever \(\beta \) is empty, we will refer to the subtyping relation as \( \, \le :_{} \, \) − without the suffix.
Fig. 4
Definition of the subtyping relation
×
The semantics of subtyping is given by set inclusion of domains [10, Theorem Semantic Subtyping].
The proof is similar to that of Theorem Semantic Subtyping in [10] while considering the 16 types of constraints imposable on referential types and noting that\(\beta \)acts as a memory of already paired class names for traversing referential types effectively.
We generalize the notion subtyping to the notion of model subtyping through the object type of the root objects of a model as follows:
In this section, we show the expressivity of our structural subtyping operation (without OCL constraints) with respect to model typing [17, 20]. We compare our approach to model subtyping by considering their example with the state machine metamodels shown in Fig. 5. Each state machine represents a version of the first one, where changes have been highlighted.
Fig. 5
Expressivity of structural subtyping relation
×
Table1 shows the subtyping relation over the set of state machines in Fig. 5, according to our structural subtyping algorithm, with subtype operands shown on the rows and supertype operands shown on the columns. These results are consistent with those presented in [20] but for the cases where many-bounded references in a supertype are constrained by a lower upper bound in the corresponding subtype. In our approach, those cases are valid.
In this section, we are going to use the notion of metamodel specification to refer to metamodels \(\mathcal {M}^{\rightarrow }_{}\) enriched with a set of OCL constraints \(\Omega \). We are going to abuse the notation \(\mathcal {M}^{\rightarrow }_{}\) to refer to any OO representation for metamodels where object subtyping is represented ontologically and where its semantics corresponds to subclassing (e.g. USE class diagrams, EMF metamodels), abstracting away from the syntactic specificities of each OO representation. Thus, our metamodels \(\mathcal {M}^{\rightarrow }_{}\) may refer to EMF metamodels or to USE class diagrams interchangeably. A subtyping operator is developed for metamodel specifications. This development is both syntactic, enabling a mechanization of the subtyping operator, and semantic, enabling reasoning about soundness of specifications when they are related via subtyping.
Moreover, we will introduce the notion of operation specification for DSLs, based on model transformations, to capture the behavioural requirements of DSLs. Such specifications are declarative, not necessarily executable, and defined in terms of OCL constraints that capture temporal properties. An additional subtyping operator is developed both syntactically and semantically for operation specifications.
Liskov and Wing [14] discussed how structural and behavioural subtyping could be used to reason about safety properties in object-orientated systems. Inspired by this work, metamodel specifications allow us to reason about subtyping of invariants in DSL semantics, properties that must hold for all of the states (or execution configurations) of the interpreter. In contrast, operation specifications allow us to reason about subtyping of behavioural properties (history properties in [14]), which are properties that hold for all sequences of interpreter states.
Next, we introduce a representation for metamodels \(\mathcal {M}^{\rightarrow }_{}\) and recall their semantics as object models \(\sigma (\mathcal {M}^{\rightarrow }_{})\), given in [11], by slightly adapting their syntax. Then, we show how a metamodel \(\mathcal {M}^{\rightarrow }_{}\) determines a model type expression \(\mathcal {M}^{<}_{}\) by means of a syntax transformation \( impl : \mathcal {M}^{\rightarrow }_{} \mapsto \mathcal {M}^{<}_{},\) which is used to triangulate \(\sigma (\mathcal {M}^{\rightarrow }_{})\) with \(\mathopen {\llbracket }{\mathcal {M}^{<}_{}}\mathclose {\rrbracket }\), reflecting the notion of model subtyping from model type expressions to metamodels. Based on this construction to couple ontological typing with linguistic typing, the subtyping relation is defined over metamodel specifications syntactically and semantically. Then, operation signatures are extended with metamodel specifications and the notion of operation specification is introduced to capture behavioural properties. Finally, the subtyping relation is defined for extended operation signatures and for operation specifications. The subtyping relation is illustrated with the three use cases of Sect. 2.
5.1 Syntax of metamodel specifications
As the typical representation of metamodels (normally depicted as class diagrams) is not aware of some type-theoretic constructs (such as union types) and the object subtyping relation is explicitly defined as a subclassing relation, we provide an alternative representation for metamodels \(\mathcal {M}^{\rightarrow }_{}\). Given the countable sets \(\mathcal {B}\) of base type names b, \(\mathcal {E}\) of enumeration type names \(\epsilon \), \(\mathcal {C}\) of class names \( c \), \(\mathcal {P}\) of property names p, a metamodel \(\mathcal {M}^{\rightarrow }_{}\) is a tuple \((\textsc {Class},\prec ,\textsc {Enum},\textsc {Cons})\) where: \(\textsc {Class}\subseteq \mathcal {C}\) is a countable set of class names; \(\prec \,\subseteq \mathcal {C}\times \mathcal {C}\) is a subclassing relation (allowing for multiple inheritance); \(\textsc {Enum}\subseteq \mathcal {E}\) is a countable set of enumeration type names; and \(\textsc {Cons}\) is the set of constraints defined by a metamodel.
The constraints in \(\textsc {Cons}\) are given as propositions of the form: \( isAbstract (c)\) holds if class c is abstract; \( p (c)\) holds if class c contains a structural feature with name \( p \); \( l (\epsilon )\) holds if \( l \) is a literal of the enumeration type denoted by \(\epsilon \); \( type (c, p ) = t\), where \(t \in \mathcal {B} \sqcup \textsc {Enum}\sqcup \textsc {Class}\) defines the type of a structural feature, which is an attribute if \(t \in \mathcal {B} \sqcup \textsc {Enum}\) and a reference if \(t \in \textsc {Class}\); \( cont (c, p )\) holds if the structural feature \( p \) is a containment reference; for \(n \in \mathbf {N}\) and \(m \in \mathbf {N} \cup \{ * \},\)\( lower (c, p ) = n\) and \( upper (c, p ) = m\), such that \(n\le m\), denote the lower and upper bounds of references; \( unique (c, p )\) holds if the structural feature is unique (when \( upper (c, p ) > 1\)); \( ordered (c, p )\) holds if the structural feature is ordered (when \( upper (c, p ) > 1\)); \(opposite(c, p ,c', p ')\) holds if the structural feature \( p (c)\) is defined as opposite of \( p '(c')\), defining a bidirectional association.
5.2 Mapping metamodels to their model types
The interpretation \(\sigma (\mathcal {M}^{\rightarrow }_{})\) of a metamodel \(\mathcal {M}^{\rightarrow }_{}\) is usually given in terms of the set of metamodel-conformant models, which are normally represented as object diagrams. In this section, we map a semantics \(\sigma (\mathcal {M}^{\rightarrow }_{})\) to \(\mathopen {\llbracket }{\mathcal {M}^{\rightarrow }_{}}\mathclose {\rrbracket } \subseteq \mathbf {V}\) in our semantic domain in order to enable structural model subtyping for metamodels \(\mathcal {M}^{\rightarrow }_{}\).
We focus on the abstract syntax of object diagrams by using attributed graphs [24], which are defined in terms of E-graphs. An E-graph has two different types of nodes, graph and data nodes, and three kinds of edges, namely regular edges, and edges for node and edge attribution. An E-graph [24, Def. 8.1] is defined as a tuple
where: \(N_G\) and \(N_D\) are the sets of graph and data nodes, resp.; \(E_G\), \(E_{NA}\) and \(E_{EA}\) are the sets of graph, node attribute and edge attribute, resp.; and source and target functions are defined as
\( src _G, tgt _G: E_G \rightarrow N_G,\)
\( src _{NA}: E_{NA} \rightarrow N_G,\)
\( tgt _{NA}: E_{NA} \rightarrow N_D,\)
\( src _{EA}: E_{EA} \rightarrow E_G,\) and
\( tgt _{EA}: E_{EA} \rightarrow N_D.\)
Let \(DSIG=(S_D,OP_D)\) be a data signature with attribute value sorts \(S'_D \subseteq S_D\), \(\mathbf {AG}\) is defined as the set of attributed graphs of the form (G, D), where G is an E-graph and D is a DSIG-algebra.
To define the model type that corresponds to each metamodel, we need to relate the semantics of a metamodel \(\mathcal {M}^{\rightarrow }_{}\) to a model type \(\mathopen {\llbracket }{\mathcal {M}^{<}_{}}\mathclose {\rrbracket }\). Given the set \(\mathbf {Union}\) of union values, such link will be achieved through a map
that obtains a union value from an attributed graph (or object diagram). Then, we generalize \(\uparrow _{\rightarrow }^{<}\) to all possible attributed graphs definable by a metamodel, mapping the semantics of metamodels to the semantics of model types.
\(\uparrow _{\rightarrow }^{<}\) is defined by the equation
where \( oc \) consists of objects \(\{ id = id(n), ps \}\) defined from nodes \(n \in N_G\), where \( ps \) is defined as the set union of properties defined from edges in \(E_G\) and \(E_{EA}\) as follows:
\( p = v\) where \(v = target(e)\) such that \(e \in E_{NA}\) and \( src (e)=n\) and \(name(e)= p \);
\( p = ic \) where \( ic = \{ id(target(e)) \, | \,e \in E_G, src (e)=n, name(e)= p \}.\)
We denote the function space \(\mathbf {AG}\rightarrow \mathbf {Union}\) as \(\Uparrow _{\rightarrow }^{<}\). The interpretation of a metamodel \(\mathcal {M}^{\rightarrow }_{}\) is given as the set \(\sigma (\mathcal {M}^{\rightarrow }_{})\) of system states definable using \(\mathcal {M}^{\rightarrow }_{}\). Ignoring the representational gap, we assume that5
Note that, in this setting, we are not considering a metamodel \(\mathcal {M}^{\rightarrow }_{}\) as just the abstract syntax for a model type expression \(\mathcal {M}^{<}_{},\) as both syntactic representations, which have different semantics, are only related by \( impl \). The map \( impl \) gives us sufficient equipment for reflecting the subtyping relation from model type expressions to metamodels:
When \(\mathcal {M}^{\rightarrow }_{1} \, \le :_{} \, \mathcal {M}^{\rightarrow }_{2}\), we have that \(\mathopen {\llbracket }{\mathcal {M}^{\rightarrow }_{1}}\mathclose {\rrbracket } \subseteq \mathopen {\llbracket }{\mathcal {M}^{\rightarrow }_{2}}\mathclose {\rrbracket }\).
5.3 Semantics of metamodel specifications
In this section, we present how metamodel specifications \((\mathcal {M}^{\rightarrow }_{},\Omega _{})\) declare model types by extending metamodels \(\mathcal {M}^{\rightarrow }_{}\) with OCL expressions \(\Omega \). The semantics of OCL expressions is reused from [11, 30]. It is worth noting that Clark et al. provided a formal semantics for OCL [8] that is more amenable to our model type expressions from a semantic point of view if we consider the MML calculus [31]. However, the USE semantics comes equipped with the tool support we need in subsequent sections.
We first define the semantics of a metamodel specification \((\mathcal {M}^{\rightarrow }_{},\Omega _{})\) using the original USE semantics \(I\mathopen {\llbracket }{\Omega }\mathclose {\rrbracket }(\mathcal {M}^{\rightarrow }_{},\Gamma )\), where \(\Omega \) is a set of OCL invariants and \(\Gamma \) is the environment of variables for evaluating the OCL invariants \(\Omega \), and then, we define the corresponding model type.
The original OO semantics of a metamodel specification \((\mathcal {M}^{\rightarrow }_{},\Omega _{})\) (representing an object model6) can be extended as follows:
We write \(\not \models _{\mathcal {M}^{\rightarrow }_{}}(\Omega )\) whenever \(\models _{\mathcal {M}^{\rightarrow }_{}}(\Omega )=\emptyset .\) We write \(G \models _{\mathcal {M}^{\rightarrow }_{}}(\Omega )\) whenever a model G conforms to a metamodel specification \((\mathcal {M}^{\rightarrow }_{},\Omega _{})\), that is \(G \in \sigma ((\mathcal {M}^{\rightarrow }_{},\Omega _{})).\)
The model type of a metamodel specification \((\mathcal {M}^{\rightarrow }_{},\Omega _{})\) is defined as follows:
Definition 5
(Model Type of\((\mathcal {M}^{\rightarrow }_{},\Omega _{})\))
To check if there are inconsistencies due to the co-existence of OCL constraints of the model subtype and of the model supertype, an extension metamodel \(\mathcal {M}^{\rightarrow }_{ sub , super }\) is synthesized from metamodels \(\mathcal {M}^{\rightarrow }_{ sub }\) and \(\mathcal {M}^{\rightarrow }_{ super }\). The main purpose of \(\mathcal {M}^{\rightarrow }_{ sub , super }\) is twofold: its semantics \(\mathopen {\llbracket }{\mathcal {M}^{\rightarrow }_{ sub , super }}\mathclose {\rrbracket }\) subsumes the semantics of \(\mathopen {\llbracket }{\mathcal {M}^{\rightarrow }_{ sub }}\mathclose {\rrbracket }\) while it is subsumed by the semantics of \(\mathopen {\llbracket }{\mathcal {M}^{\rightarrow }_{ super }}\mathclose {\rrbracket }\), that is
$$\begin{aligned} \mathopen {\llbracket }{\mathcal {M}^{\rightarrow }_{ sub }}\mathclose {\rrbracket } \;\subseteq \; \mathopen {\llbracket }{\mathcal {M}^{\rightarrow }_{ sub , super }}\mathclose {\rrbracket } \;\subseteq \; \mathopen {\llbracket }{\mathcal {M}^{\rightarrow }_{ super }}\mathclose {\rrbracket };\qquad (1) \end{aligned}$$
and it reifies \(\mathcal {M}^{\rightarrow }_{ sub } \, \le :_{} \, \mathcal {M}^{\rightarrow }_{ super }\) as an explicitly declared (static) subclassing relation \(\prec \) between classes of \(\mathcal {M}^{\rightarrow }_{ sub }\) and classes of \(\mathcal {M}^{\rightarrow }_{ super }\) − that is, for any \(c_ sub \in \textsc {Class}_ sub \) and \(c_ super \in \textsc {Class}_ super ,\)
$$\begin{aligned} c_ sub \prec c_ super \iff \texttt {type}(c_ sub ) \, \le :_{} \, \texttt {type}(c_ super ).\qquad (2) \end{aligned}$$
In the following, the synthesis process is discussed and illustrated with the running example. We assume that the set of classifier names for \(\mathcal {M}^{\rightarrow }_{ sub }\) and \(\mathcal {M}^{\rightarrow }_{ super }\) are disjoint. If that is not the case, a renaming has to be applied to the classifiers of the subtype metamodel first so as to ensure that precondition. Given the metamodels \(\mathcal {M}^{\rightarrow }_{ sub }\) and \(\mathcal {M}^{\rightarrow }_{ super }\), and a subclassing relation \(\prec \) between their classes, the operation \( synth (\mathcal {M}^{\rightarrow }_{ sub },\mathcal {M}^{\rightarrow }_{ super },\prec )\) produces a metamodel \(\mathcal {M}^{\rightarrow }_{ sub , super }\) that is defined as follows:
Initialization. Initially, the set \(\textsc {Class}_{ sub , super }\) of classifiers of \(\mathcal {M}^{\rightarrow }_{ sub , super }\) is formed by those of \(\mathcal {M}^{\rightarrow }_{ sub }\) and of \(\mathcal {M}^{\rightarrow }_{ super }\). Then, the subclassing relation \(\prec _{ sub , super }\) for \(\mathcal {M}^{\rightarrow }_{ sub , super }\) is obtained as follows \(\prec _{ sub , super } \,=\, \prec _{ sub } \cup \prec _{ super } \cup \prec .\) Classes of the supertype are made abstract by adding constraints
to \(\textsc {Cons}_{ sub , super }\). These constraints are added to narrow down the search for inconsistencies to \(\mathopen {\llbracket }{\mathcal {M}^{\rightarrow }_{ sub }}\mathclose {\rrbracket }.\)
Virtual superclass extraction.\(\prec _{ sub , super }\) is analysed and for each class that inherits the same feature f declared in two different superclasses \(sc_1\) and \(sc_2\), we extract an abstract virtual superclass \(sc_{1,2}\), where the order in the subscript 1, 2 is inessential, of the two superclasses \(sc_1\) and \(sc_2\) in order to ensure the diamond property. The feature f is pulled up to the virtual superclass \(sc_{1,2}\) (and removed from the superclasses \(sc_1\) and \(sc_2\)). \(\textsc {Class}_{ sub , super }\) is augmented with \(sc_{1,2}\), and \(\prec _{ sub , super }\) is augmented with \((sc_1,sc_{1,2})\) and \((sc_2,sc_{1,2}).\) This analysis is repeated recursively until all virtual superclasses and the corresponding specialization links are added.
Preserving the semantics of subclassing. The next step consists in pulling up common features from classes in the subtype metamodel \(\mathcal {M}^{\rightarrow }_{ sub }\) to classes in the supertype metamodel \(\mathcal {M}^{\rightarrow }_{ super }\). For each class \(c_{ sub } \in \textsc {Class}_{ sub }\) that declares a feature \( p (c_{ sub }) \in \textsc {Cons}_{ sub }\) such that there is an ancestor class \(c_{ super } \in \textsc {Class}_{ super }\) declaring a feature \( p (c_{ super }) \in \textsc {Cons}_{ super },\) the structural feature \( p (c_ super )\) is added to \(\textsc {Cons}_{ sub , super }\) and removed from \(\textsc {Cons}_{ super }\) together with all the constraints defined for \( p \). In addition, the constraints of feature \( p \) for \(c_ sub \) in \(\textsc {Cons}_ sub \) are redefined for \(c_ super \) and added to \(\textsc {Cons}_{ sub , super }\) while they are removed from \(\textsc {Cons}_ sub \) together with \( p (c_ sub )\). This means that the feature \( p \) is pulled up from \(c_{ sub }\) to the ancestor \(c_{ super }\) (and removed from \(c_{ sub }\)). The rest of constraints from \(\textsc {Cons}_ sub \) and \(\textsc {Cons}_ super \) are added to \(\textsc {Cons}_{ sub , super }\). Hence, \(\mathopen {\llbracket }{\mathcal {M}^{\rightarrow }_{ sub , super }}\mathclose {\rrbracket } \subseteq \mathopen {\llbracket }{\mathcal {M}^{\rightarrow }_{ super }}\mathclose {\rrbracket }.\)
The resulting extension metamodel \(\mathcal {M}^{\rightarrow }_{sm,g}\) for the running example is depicted in Fig. 6, where the multiplicities for the references
and
from \(\mathcal {M}^{\rightarrow }_{sm}\) have been preserved. In \(\mathcal {M}^{\rightarrow }_{sm,g},\) two virtual classes,
and
, have been extracted in two consecutive iterations.
For extending model subtyping to metamodel specifications using the construction presented above, we are going to use the extension metamodel \(\mathcal {M}^{\rightarrow }_{ sub , super }\) synthesized by means of \( synth (\mathcal {M}^{\rightarrow }_{ sub },\mathcal {M}^{\rightarrow }_{ super }, \prec _{ sub , super })\) where
$$\begin{aligned} \prec _{ sub , super }=\,\mathcal {M}^{\rightarrow }_{ sub } \, \le :_{} \, \mathcal {M}^{\rightarrow }_{ super } \cap \textsc {Class}_{ sub }\times \textsc {Class}_{ super }. \end{aligned}$$
Note that property (1) is satisfied as \(\mathopen {\llbracket }{\mathcal {M}^{\rightarrow }_{ sub }}\mathclose {\rrbracket } \subset \mathopen {\llbracket }{\mathcal {M}^{\rightarrow }_{ sub , super }}\mathclose {\rrbracket }\) by definition. In the example, we can have models in \(\mathcal {M}^{\rightarrow }_{sm,g}\), such an object
pointing to an object
through the reference
, that are not valid models in \(\mathcal {M}^{\rightarrow }_{sm}\). In addition, the preservation of the constraints of structural features in \(\mathcal {M}^{\rightarrow }_{ sub }\) when extracting virtual classes forces \(\mathopen {\llbracket }{\mathcal {M}^{\rightarrow }_{ sub , super }}\mathclose {\rrbracket } \subseteq \mathopen {\llbracket }{\mathcal {M}^{\rightarrow }_{ super }}\mathclose {\rrbracket }.\) For instance, in the example, objects of type
are of type
as the properties of
are included in
.
On the other hand, the property (2) is ensured by constructing \(\prec \) as explained above, since the extracted virtual classes have a counterpart in the semantic domain as the meet types of the corresponding object types.
The notion of metamodel extension enables the articulation of syntactic model subtyping of metamodel specifications, coupling the semantics of metamodels with the semantics of OCL constraints, as follows:
Definition 6
(Syntactic Model Subtyping with Metamodel Specifications)
$$\begin{aligned}&(\mathcal {M}^{\rightarrow }_{ sub },\Omega _{ sub }) \, \le :_{} \, (\mathcal {M}^{\rightarrow }_{ super },\Omega _{ super }) \triangleq \\&\qquad \mathcal {M}^{\rightarrow }_{ sub } \, \le :_{} \, \mathcal {M}^{\rightarrow }_{ super } \; \wedge \; \models _{\mathcal {M}^{\rightarrow }_{ sub , super }}(\Omega _ sub \Rightarrow \Omega _ super ) \end{aligned}$$
Theorem 2
(Semantic Model Subtyping)
$$\begin{aligned}&(\mathcal {M}^{\rightarrow }_{ sub },\Omega _{ sub }) \, \le :_{} \, (\mathcal {M}^{\rightarrow }_{ super },\Omega _{ super }) \Rightarrow \\&\qquad \qquad \mathopen {\llbracket }{(\mathcal {M}^{\rightarrow }_{ sub },\Omega _{ sub })}\mathclose {\rrbracket } \subseteq \mathopen {\llbracket }{(\mathcal {M}^{\rightarrow }_{ super },\Omega _{ super })}\mathclose {\rrbracket } \end{aligned}$$
Proof
As \(\mathcal {M}^{\rightarrow }_{ sub } \, \le :_{} \, \mathcal {M}^{\rightarrow }_{ super },\) there is a synthesized metamodel \(\mathcal {M}^{\rightarrow }_{ sub , super }\) in which both \(\Omega _{ sub }\) and \(\Omega _{ super }\) can be satisfied.
By the construction of \(\mathcal {M}^{\rightarrow }_{ sub , super }\), we have that
$$\begin{aligned} \mathopen {\llbracket }{(\mathcal {M}^{\rightarrow }_{ sub },\Omega _{ sub })}\mathclose {\rrbracket } \subseteq \mathopen {\llbracket }{(\mathcal {M}^{\rightarrow }_{ sub , super },\Omega _{ sub })}\mathclose {\rrbracket }. \end{aligned}$$
Since \(\models _{\mathcal {M}^{\rightarrow }_{ sub , super }}(\Omega _ sub \Rightarrow \Omega _ super ),\) then
$$\begin{aligned} \mathopen {\llbracket }{(\mathcal {M}^{\rightarrow }_{ sub , super },\Omega _{ sub })}\mathclose {\rrbracket } \subseteq \mathopen {\llbracket }{(\mathcal {M}^{\rightarrow }_{ sub , super },\Omega _ super )}\mathclose {\rrbracket }. \end{aligned}$$
By the construction of \(\mathcal {M}^{\rightarrow }_{ sub , super }\), we have that
$$\begin{aligned} \mathopen {\llbracket }{(\mathcal {M}^{\rightarrow }_{ sub , super },\Omega _ super )}\mathclose {\rrbracket } \subseteq \mathopen {\llbracket }{(\mathcal {M}^{\rightarrow }_{ super },\Omega _{ super })}\mathclose {\rrbracket }. \end{aligned}$$
Hence, \(\mathopen {\llbracket }{(\mathcal {M}^{\rightarrow }_{ sub },\Omega _{ sub })}\mathclose {\rrbracket } \subseteq \mathopen {\llbracket }{(\mathcal {M}^{\rightarrow }_{ super },\Omega _{ super })}\mathclose {\rrbracket }.\)
5.5 Model transformation operation specifications
In this section, we extend function types to metamodel specifications in order to specify model transformation operations
where \((\mathcal {M}^{\rightarrow }_{pre},\Omega _{pre})\) specifies its preconditions and \((\mathcal {M}^{\rightarrow }_{post},\Omega _{post})\) specifies its postconditions.
First, we extend the notion of model transformation operation signature over metamodel specifications and augment the subtyping relation for operation signatures to enable safe substitution of operations. Second, operation application is defined, showing how operations can be reused across model types that are related via signature subtyping. Third, we develop the semantic notion of model transformation operation specification that enables refinement checking via operation specification subtyping.
Definition 7
(Extended signature for operations) Given a source metamodel specification \((\mathcal {M}^{\rightarrow }_{s},\Omega _{s})\), a target metamodel specification \((\mathcal {M}^{\rightarrow }_{t},\Omega _{t})\), and a model transformation operation signature \(\rho : \mathcal {M}^{\rightarrow }_{s} \rightarrow \mathcal {M}^{\rightarrow }_{t}\), its extended signature over the metamodel specifications is defined as \(\rho _{s\rightarrow t}: (\mathcal {M}^{\rightarrow }_{s},\Omega _{s}) \rightarrow (\mathcal {M}^{\rightarrow }_{t},\Omega _{t})\) iff, for any model \(G \in \mathopen {\llbracket }{(\mathcal {M}^{\rightarrow }_{s},\Omega _{s})}\mathclose {\rrbracket }\), \(\rho (G) \in \mathopen {\llbracket }{(\mathcal {M}^{\rightarrow }_{t},\Omega _{t})}\mathclose {\rrbracket }\).
While an extended operation signature is mostly a syntactic construct, it can also be regarded as the contract of a blackbox operation where the source metamodel specification details the operation pre-conditions, explaining where the operation can be applied. In contrast, the target metamodel specification provides the post-conditions, explaining the effects of the operation. For an extended signature \(\rho _{s\rightarrow t}\) to define a subtype of another extended signature \(\rho _{s'\rightarrow t'}\), the precondition defined by \((\mathcal {M}^{\rightarrow }_{s},\Omega _{s})\) can be more liberal in order to accept all models in \((\mathcal {M}^{\rightarrow }_{s'},\Omega _{s'})\) while the postcondition \((\mathcal {M}^{\rightarrow }_{t},\Omega _{t})\) needs to be constrained in order to produce at most those models in \((\mathcal {M}^{\rightarrow }_{t},\Omega _{t})\). The following definition captures these considerations using the subtyping relation:
Definition 8
(Extended operation signature subtyping) Given two extended operation signatures \(\rho _{s\rightarrow t}\) and \(\rho _{s'\rightarrow t'}\), \(\rho _{s\rightarrow t} \, \le :_{} \, \rho _{s'\rightarrow t'}\) iff
Subtyping of extended operation signatures characterizes when it is safe to substitute model transformation operations. Safe substitution of operations is useful for defining higher-order model transformation operations, like higher-order model transformations (HOTs) [32]. An extended operation signature can be used to define a formal parameter, and subtyping can be used to check if it is safe to replace the formal parameter with a more specific extended operation signature. This check treats operations as blackboxes and only considers their pre-/post-condition contracts.
For example, an extended operation signature \((\mathcal {M}^{\rightarrow }_{pre},\Omega _{pre}) \rightarrow (\mathcal {M}^{\rightarrow }_{post},\Omega _{post})\) can be applied to models conforming to a metamodel specification \((\mathcal {M}^{\rightarrow }_{ac},\Omega _{ac})\) if \((\mathcal {M}^{\rightarrow }_{ac},\Omega _{ac}) \, \le :_{} \, (\mathcal {M}^{\rightarrow }_{pre},\Omega _{pre}).\) On the other hand, we can reuse the results of this operation as models conforming to a (possibly different) metamodel specification \((\mathcal {M}^{\rightarrow }_{ac},\Omega _{ac})\) if \((\mathcal {M}^{\rightarrow }_{post},\Omega _{post}) \, \le :_{} \, (\mathcal {M}^{\rightarrow }_{ac},\Omega _{ac}).\) The first condition ensures that the operation can rely on values of \((\mathcal {M}^{\rightarrow }_{ac},\Omega _{ac})\), and the second condition guarantees that its outputs will not create any problem in the expecting context. In our running example of Sect. 2.2, \((\mathcal {M}^{\rightarrow }_{g},\Omega _{g}) \rightarrow (\mathcal {M}^{\rightarrow }_{g},\Omega _{g})\) can be applied to a model in \((\mathcal {M}^{\rightarrow }_{sm},\Omega _{sm})\)as is for simulating a deterministic state machine. This will result in the creation of objects
, which can be automatically coerced to the type
as explained in Sect. 6.3.
A model transformation operation specification \((\rho _{s\rightarrow t},\Omega _{s\rightarrow t})\) is formed by an extended operation signature \(\rho _{s\rightarrow t}\) and a set of invariant constraints \(\Omega _{s \rightarrow t}\) extending the invariants in the precondition metamodel specification \((\mathcal {M}^{\rightarrow }_{s},\Omega _{s})\) and in the postcondition metamodel specification \((\mathcal {M}^{\rightarrow }_{t},\Omega _{t})\), capturing the operation semantics, that is, its intent. Model transformation operations can be encoded as invariants by considering the notion of transformation model [32], already exploited for encoding model transformations represented in ATL [33], QVT-R [34], and triple graph grammars [34].
For enabling the definition of operations with OCL invariants, the metamodels involved must define a notion of a snapshot capturing the set of models on which the operation is going to be applied, another set of snapshots capturing the models resulting from applying the operation, and a relation over sets of snapshots encoding temporal information in the model type. That is operation invariants must be declared over the relation \(\mathcal {M}^{\rightarrow }_{s} \times \mathcal {M}^{\rightarrow }_{t}\). With this assumption in mind, the semantics of an operation specification is defined as follows. This relation was captured via the
association in the example of Sect. 2.3.
Definition 9
(Operation specification semantics) Given an operation specification \((\rho _{s\rightarrow t},\Omega _{s\rightarrow t})\),
A model transformation operation specification is defined with its signature and intent, thus capturing the operation’s behaviour. The subtyping relation is generalized to model transformation operation specifications as follows.
That is, the extended operation signature \(\rho _{s\rightarrow t}\) must be a subtype of the extended operation signature \(\rho _{s'\rightarrow t'}\) and the behaviour of the supertype operation must be preserved in the subtype operation. The subtyping relation characterizes behavioural subtyping, and it can be used to check stepwise refinement between model transformation operations automatically (within the appropriate selection of bounds for the model finder).
In the example of Sect. 2.3, an operation specification capturing the behaviour of the state machine simulator is introduced for the metamodel specification containing the association
. In this example, operation specification subtyping is trivially satisfied, as the operation is not defined for the supertype. However, subtyping is still helpful for automatically finding unintended inconsistencies between the effects of the operation and the valid class of models. Cabot et al. [34] described an alternative approach for capturing declarative specifications of model-to-model transformations using OCL invariants, without having to include temporal information in the metamodel. Our approach would also work with this alternative representation, after adapting the notion of satisfaction of behavioural constraints, although the resulting behavioural specifications would be more verbose and, thereby, more expensive to verify. While our notion of operation specification is based on invariants, operation specifications given in terms of OCL pre- and post-conditions can be translated to the proposed representation by using the filmstripping technique proposed by Hilken et al. [35], implemented in USE.
6 Tool support
The theory described in previous sections is implemented as a Java library that facilitates reuse in MDE. Specifically, given two metamodel specifications \((\mathcal {M}^{\rightarrow }_{ sub },\Omega _{ sub })\) and \((\mathcal {M}^{\rightarrow }_{ super },\Omega _{ super })\), where \(\mathcal {M}^{\rightarrow }_{ sub }\) and \(\mathcal {M}^{\rightarrow }_{ super }\) are EMF metamodels and \(\Omega _{ sub }\) and \(\Omega _{ super }\) are sets of OCL constraints in USE format (whose contextual types are defined in \(\mathcal {M}^{\rightarrow }_{ sub }\) and \(\mathcal {M}^{\rightarrow }_{ super }\) resp.), the tool will determine whether \((\mathcal {M}^{\rightarrow }_{ sub },\Omega _{ sub })\) denotes a model subtype of the model type denoted by \((\mathcal {M}^{\rightarrow }_{ super },\Omega _{ super }).\) Note that any of the sets of OCL constraints may be empty.
If the check fails, there are two main sources of incompatibilities: the model types denoted by the metamodels and the OCL constraints. In the first case, the tool points at the source of the problem by showing the classes of the supertype metamodel \(\mathcal {M}^{\rightarrow }_{ super }\) that are not extended by classes of \(\mathcal {M}^{\rightarrow }_{ sub }\). That information is useful to assess the advantage of, for example, pruning the supertype metamodel by computing the effective metamodel [23] w.r.t. a specific model transformation operation. In the second case, the tool will provide evidence that contradicts the compatibility property in Definition 6 of \(\mathcal {M}^{\rightarrow }_{ sub }\) w.r.t. \(\mathcal {M}^{\rightarrow }_{ super }\) in the form of a model \(G \in \mathopen {\llbracket }{\mathcal {M}^{\rightarrow }_{ sub , super }}\mathclose {\rrbracket },\) represented in EMF notation (that is in XMI format), that invalidates a constraint in \(\Omega _ super .\)
If the check succeeds, the tool guarantees that \((\mathcal {M}^{\rightarrow }_{ sub },\Omega _{ sub })\) is a structural refinement of \((\mathcal {M}^{\rightarrow }_{ super },\Omega _{ super }).\) Hence, any model transformation operation that is defined for \((\mathcal {M}^{\rightarrow }_{ super },\Omega _{ super })\) can be safely applied to models of \((\mathcal {M}^{\rightarrow }_{ sub },\Omega _{ sub }).\) Going one step further, the tool also facilitates the reuse of such operation, when it is based on EMF, by automatically synthesizing an extension metamodel \(\mathcal {M}^{\rightarrow }_{ sub , super }\) that can be substituted for \(\mathcal {M}^{\rightarrow }_{ super }\) in the signature of the operation ensuring its application to models conforming to \(\mathopen {\llbracket }{(\mathcal {M}^{\rightarrow }_{ sub },\Omega _{ sub })}\mathclose {\rrbracket }\) without any further change.
In the following subsections, we explain how the tool reuses a third-party bounded model finder for verifying the compatibility property of Definition 6, and we discuss how our subtyping relation \( \, \le :_{} \, \) can be used to deal with multiple, dynamic and partial model typing.
6.1 Analysing OCL constraints
In our tool, we have adapted excerpts of TOTEM-MDE [36] in order to integrate the USE Validator [37] with EMF. For computing whether \((\mathcal {M}^{\rightarrow }_{ sub },\Omega _{ sub }) \, \le :_{} \, (\mathcal {M}^{\rightarrow }_{ super },\Omega _{ super })\) holds, the property \(\models _{\mathcal {M}^{\rightarrow }_{ sub , super }}(\Omega _ sub \Rightarrow \Omega _{ super })\) needs to be verified. Assuming \(\Omega _ super \) is of the form
$$\begin{aligned}&\models _{\mathcal {M}^{\rightarrow }_{ sub , super }}(\Omega _{ sub } \;\wedge \; \\&\quad {\texttt {context}} \;c\; {\texttt {inv:}} \bigvee _i \;c_i {\texttt {.allInstances()->exists(}} \lnot \omega _i {\texttt {)}}) \end{aligned}$$
where c is any class name from \(\textsc {Class}_{ super }\).
If the negated property turns out to be satisfiable, a model G conforming to \(\mathcal {M}^{\rightarrow }_{ sub , super }\), that is \(G \in \mathopen {\llbracket }{\mathcal {M}^{\rightarrow }_{ sub }}\mathclose {\rrbracket }\) is returned, showing that there is an inconsistency that needs to be resolved. Subject to the appropriateness of the bounds provided for the analysis, if the negated property turns out to be unsatisfiable, the original property holds and \((\mathcal {M}^{\rightarrow }_{ sub },\Omega _{ sub })\) defines a subtype of the model type denoted by \((\mathcal {M}^{\rightarrow }_{ super },\Omega _{ super }).\) In the running example, we have that \((\mathcal {M}^{\rightarrow }_{sm},\Omega _{sm}) \, \le :_{} \, (\mathcal {M}^{\rightarrow }_{g},\Omega _{g})\) but \((\mathcal {M}^{\rightarrow }_{sm},\emptyset ) \, \not \le :_{} \, (\mathcal {M}^{\rightarrow }_{g},\Omega _{g}),\) where \((\mathcal {M}^{\rightarrow }_{sm},\emptyset )\) denotes a model type of non-deterministic state machines.
6.2 Multiple and strict typing
Given two metamodel specifications \((\mathcal {M}^{\rightarrow }_{1},\Omega _{1})\) and \((\mathcal {M}^{\rightarrow }_{2},\Omega _{2}),\) when we compute \((\mathcal {M}^{\rightarrow }_{1},\Omega _{1}) \, \le :_{} \, (\mathcal {M}^{\rightarrow }_{2},\Omega _{2}),\) we obtain multiple inheritance semantics [10], that is multiple typing, by default. However, we can force strict typing in contexts where multiple typing is not allowed by obtaining the synthesized metamodel using a strict specialization relation \(\prec ^{s} \subseteq \textsc {Class}_ sub \times \textsc {Class}_ super \) where
Note that there may be many such strict specialization relations in \((\mathcal {M}^{\rightarrow }_{ sub },\Omega _{ sub }) \, \le :_{} \, (\mathcal {M}^{\rightarrow }_{ super },\Omega _{ super })\). Our tool enumerates all of them, and for each specialization relation \(\prec ^s,\) it computes: the extension metamodel \( synth (\mathcal {M}^{\rightarrow }_{ sub },\mathcal {M}^{\rightarrow }_{ super },\prec ^s);\) the complement supertype metamodel \(\nearrow (\mathcal {M}^{\rightarrow }_{ sub },\mathcal {M}^{\rightarrow }_{ super },\prec ^s)\) defined as the effective metamodel of those classes in \(\textsc {Class}_{ super },\) including their features and associated multiplicity constraints, that do not appear in the image of \(\prec ^s;\) the complement subtype metamodel \(\searrow (\mathcal {M}^{\rightarrow }_{ sub },\mathcal {M}^{\rightarrow }_{ super },\prec ^s)\) similarly defined for those classes in \(\textsc {Class}_{ sub }\) that do not appear in the preimage of \(\prec ^s;\) and a rank representing the model size of the complement metamodels.
The strict specialization relation \(\prec ^s\) with the lowest rank is the solution that provides the maximal model subtype w.r.t. strict model subtyping. When computing \((\mathcal {M}^{\rightarrow }_{ sub },\Omega _{ sub }) \, \le :_{} \, (\mathcal {M}^{\rightarrow }_{ super },\Omega _{ super })\) using strict typing mode, the tool recommends the specialization relation \(\prec ^s\) with the lowest rank and will compute the satisfaction of OCL constraints using the synthesized metamodel \( synth (\mathcal {M}^{\rightarrow }_{ sub },\mathcal {M}^{\rightarrow }_{ super },\prec ^s).\) In the case of a tie, one strict specialization relation is chosen arbitrarily. However, the user can still inspect the other strict specialization relations enumerated by recommendation order, together with their corresponding synthesized metamodel and complement metamodels.
In the example, when forcing strict model subtyping, the extension metamodel \( synth (\mathcal {M}^{\rightarrow }_{sm},\mathcal {M}^{\rightarrow }_{g},\prec ^s)\) that is recommended is depicted in Fig. 7, together with the complement of the subtype metamodel
Dynamic typing, understood as the property of an object to change its type while preserving its identity, can be implemented by constructing synthesized metamodels. A model operation
which entails the existence of an extension metamodel \(\mathcal {M}^{\rightarrow }_{creation,in}.\) That is the subtyping relation between two model types is inferred in \(\mathcal {M}^{\rightarrow }_{creation,in},\) if it exists within the bounded search space. The extension metamodel is synthesized as explained in Sect. 5.4, but without adding constraints of the form \(( 3 )\) in order to enable side effects of model transformation operations that work with supertype classes. The extension metamodel facilitates the reuse of model transformation operations that may be implemented using EMF-based technology.
6.4 Retyping and type coercion
Throughout the paper, we assume that subtype and supertype have disjoint names. When this is not the case, the tool will automatically rename the classifiers in the subtype to ensure this condition. Metamodels must be defined in the same package for mapping the metamodel spec to USE. In such cases, the subtyping operator can yield several type renamings when computing the extension metamodel. In particular, to resolve this ambiguity, the algorithm that generates the extension metamodel renames classes in the subtype by prefixing the package’s name. The tool reifies the subtyping relation between object types as annotations in the extension metamodel, including any implicit renaming.
As a consequence, as EMF relies on a nominal type system, two cases need to be considered when applying the operation to be reused: following up with the example in the previous section, when no new instances of classes in \(\textsc {Class}_{creation,in}\) are created, but implicit renamings were added in the extension metamodel, that is only queries or updates are applied; and when new instances of classes in \(\textsc {Class}_{creation,in}\) are created. Both cases are illustrated in Fig. 8, where an excerpt of a subtype metamodel and a supertype metamodel with a shared type are shown, together with the extension metamodel that infers their binding with inheritance and a renaming. The bold arrows represent the application of either a retyping or type coercion between models, and the dashed arrows represent the typing of each object, showing to which type each model belongs.
Fig. 8
Retyping and type coercion
×
In the first case, when classifier names are disjoint in the supertype and the subtype, the resulting model conforms to \((\mathcal {M}^{\rightarrow }_{creation},\Omega _{creation})\) without further changes. When implicit renamings are used (case a)), retyping \(G'\) of models \(G \in \mathopen {\llbracket }{\mathcal {M}^{\rightarrow }_{creation}}\mathclose {\rrbracket }\) is required so that \(G' \in \mathopen {\llbracket }{\mathcal {M}^{\rightarrow }_{creation,in}}\mathclose {\rrbracket }.\) Retyping is implemented using the EMF-Syncer [13]. In this context, the EMF-Syncer is a bidirectional synchronization tool between EMF metamodels that automatically matches the structural features of classes from one metamodel to other features in classes of the second metamodel by name, thus relying on a nominal type system for metamodels. Mapping strategies between metamodels may also be defined explicitly when matching cannot be inferred by name. Forward model synchronization can be done either eagerly, when the whole source model needs to be retyped, or on demand, when only those model excerpts that are used by the corresponding model transformation operation need to be retyped, and backward synchronization is done incrementally. The EMF-Syncer will read the annotations that were generated while the extension metamodel was inferred, meta-representing the subtyping relations between specific object types. With such data, the EMF-Syncer instantiates the most concrete object type in the extension metamodel, corresponding to the subtype metamodel. In our tool, retyping is performed via the operations
, for retype a subtype-conforming model, and
, for retyping back the extension-conforming model to its original subtype.
In the second case (b)), also illustrated in Fig. 8, a type coercion operation is needed to cast down objects to classes defined in \((\mathcal {M}^{\rightarrow }_{creation},\Omega _{creation})\). For a model \(G \in \mathopen {\llbracket }{(\mathcal {M}^{\rightarrow }_{in},\Omega _{in})}\mathclose {\rrbracket }\), the coercion operation
$$\begin{aligned} G \; as \; \mathcal {M}^{\rightarrow }_{creation} \; with \; \prec ^s \end{aligned}$$
where \(\prec ^s\) is a strict subtyping relation between classes in \(\textsc {Class}_{creation}\) and \(\textsc {Class}_{in}\), requires all mandatory features in \(\searrow (\mathcal {M}^{\rightarrow }_{creation},\mathcal {M}^{\rightarrow }_{in},\prec ^s)\) to have a default value. That is, those mandatory structural features that are not initialized in the operation need to be properly defined in a model.
The coercion operator changes the type of those objects in G, whose type is a class \(c_{ super } \in \textsc {Class}_{\in }\), for the greatest class \(c_{ sub }\), with respect to \(\prec _{creation}\), in \(\textsc {Class}_{creation}\) such that \(c_{ sub } \prec ^s c_{ super }\). The operator is not defined when the choice of \(c_{ sub }\) is not unique −, e.g. when multiple inheritance is used in \(\mathcal {M}^{\rightarrow }_{in}.\) The coercion operator is also implemented using the EMF-Syncer , as a forward model transformation from supertype to subtype, similar to the retyping operations. The chosen strict inheritance relation, meta-represented as annotations in the extension metamodel, provides the renamings to be used as mapping specification by the EMF-Syncer . The main difference with the retyping operations is that up casting (corresponding to backward propagation of changes) is not needed. In case b) of Fig. 8, newly created objects by a model transformation operation defined for the supertype, need to be casted down and then mapped back to the original subtypes.
6.5 Partial versus total typing
Given two metamodel specifications \((\mathcal {M}^{\rightarrow }_{ sub },\Omega _{ sub })\) and \((\mathcal {M}^{\rightarrow }_{ super },\Omega _{ super })\), if \((\mathcal {M}^{\rightarrow }_{ sub },\Omega _{ sub }) \, \le :_{} \, (\mathcal {M}^{\rightarrow }_{ super },\Omega _{ super })\), then \((\mathcal {M}^{\rightarrow }_{ super },\Omega _{ super })\) totally types the models that conform to \((\mathcal {M}^{\rightarrow }_{ sub },\Omega _{ sub })\). In such case, \(| \searrow (\mathcal {M}^{\rightarrow }_{ sub },\mathcal {M}^{\rightarrow }_{ super }, \prec ) |=0.\) When this equation does not hold, the complement of the subtype metamodel with respect to the inferred specialization relation \(\prec ,\) which may or may not be strict, tells us that \((\mathcal {M}^{\rightarrow }_{ super },\Omega _{ super })\) is only a partial type for models that conform to \((\mathcal {M}^{\rightarrow }_{ sub },\Omega _{ sub }),\) explaining what parts of such models are not typed by \((\mathcal {M}^{\rightarrow }_{ super },\Omega _{ super })\). In the example of Fig. 7, the complement \(\searrow (\mathcal {M}^{\rightarrow }_{sm},\mathcal {M}^{\rightarrow }_{g},\prec ^s)\) of the subtype metamodel shows that the references
and
are not covered by the supertype metamodel in \( synth (\mathcal {M}^{\rightarrow }_{sm},\mathcal {M}^{\rightarrow }_{g},\prec ^s),\) which is useful for selecting a specific strict subtyping.
On the other hand, when in the complement of the supertype, we have that \(| \nearrow (\mathcal {M}^{\rightarrow }_{ sub },\mathcal {M}^{\rightarrow }_{ super },\prec ) |\ne 0,\) then \(\mathcal {M}^{\rightarrow }_{ sub }\) is not a subtype of \(\mathcal {M}^{\rightarrow }_{ super }\). To improve the reuse of model transformation operations in this situation, we can compute the effective metamodel of the model transformation operation inducing a more general model type, removing those OCL constraints that become redundant.
7 Use cases
In this section, a number of use cases show the versatility of the subtyping relation and how it facilitates reuse across modelling languages.
7.1 Semantic structural refinement
The first use case follows from the running example illustrated in Fig. 1, where the subtyping operator can be used to check whether a metamodel specification \((\mathcal {M}^{\rightarrow }_{sub},\Omega _{sub})\) is a refinement of another one \((\mathcal {M}^{\rightarrow }_{super},\Omega _{super})\). This use case demonstrates the optionality of OCL constraints in metamodel specifications when using the subtyping operator.
The model types described by both metamodels are structurally similar in that they both describe languages of graphs. On the one hand, the top metamodel specification characterizes the graph of a function defined over nodes. On the other hand, the bottom metamodel specification characterizes deterministic state machines where an event can trigger transitions (indicated in the name attribute of the transition) or are triggerless, e.g. in the case of completion transitions.
Moreover, consider non-deterministic state machines by removing the OCL constraint defining the deterministic condition from the state machine metamodel specification. We obtain a non-deterministic state machine that does not satisfy the graph constraint, which is represented in object diagram notation in Fig. 9. In this case, subject to appropriate selection of type bounds, the subtyping operator finds a counterexample, showing that the subtyping relation does not hold. The counterexample is a model conforming to the extension metamodel and can be casted down to the subtype as explained in the sections below.
Fig. 9
Counterexample
×
7.2 Multiple typing
The subtyping relation intrinsically supports multiple typing, enabling subtyping where strict typing is too stringent. In the example of Fig. 10, borrowed from Bruel et al. [38], where an abstract structural containment design pattern is modelled in different metamodels. The goal in this example is to define a model transformation operation for the abstract container metamodel (a) in Fig. 10) in order to reuse it in other metamodels.
Metamodel b) describing goals only contains a class
with a containment reference
. The subtyping relation, illustrated with a dashed arrow, identifies the class
as subtype of both
and
at the same time. However, the metamodels defining state machines (c)) and projects (d)) are not valid subtypes of the abstract container metamodel. In the state machine metamodel,
is not a subtype of
since the feature
cannot be matched to the feature
. The reason for this is that the type
is not a subtype of the type
, as it has no feature corresponding to
. In the project metamodel, the type
is not a subtype of the type
because the type of the feature
is not compatible with the type of the feature
, as its type
is not a subtype of the type
.
Fig. 10
Example of multiple typing
×
To enable reuse in metamodels c) and d), metamodel pruning is not enough to extract the effective metamodel, where the class
in c) and the class
in d) would be removed, leaving a singleton class inheritance relationship in each metamodel that would have to be flattened.
7.3 DSML evolution (Reuse, Partial Typing)
In this use case, we are going to show how to reuse a model transformation operation—a model-to-text transformation with ATL—defined for a metamodel
, a modified version of the state machine metamodel, for models of a metamodel
. In Fig. 11, metamodel
enables observable behaviour in state machines, where state observations are timestamped. Code generation from state machines to the format proposed by Fowler [39] is implemented using ATL. Figure 11, bottom part, from left to right, shows the model transformation, a state machine and its serialized counterpart.
Fig. 11
Example of operation evolution. Top (from left to right):
of metamodel (partial supertype),
(pruned, total supertype),
(subtype). Bottom (from left to right): ATL operation defined for
; state machine as instance of
; output of operation
×
In this hypothetical case of evolution, it becomes essential to track which operations are executed, instead of their states. Metamodel
captures the dual notion of observability by using events to mark when a transition is triggered. The metamodel
is not exactly a supertype of the metamodel
. This change is not a structural refinement and is not backward compatible using traditional object-oriented extension mechanisms. In addition, metamodel
is enriched with an OCL constraint on the name of the events that can be created:
Fig. 12
Complement supertype with version 1 (top); extension metamodel with version 1, pruned (bottom)
×
×
Our subtyping operator assists us in determining that
of the metamodel together with the OCL constraint is not a refinement of
. Figure 12 shows the complement of the supertype obtained from the structural subtyping operator, explaining why models of metamodel
can only be partially typed by metamodel
. To resolve this issue, the complement of the supertype is pruned from metamodel
and the subtyping operator is then used to check whether the metamodel
is supertype of metamodel
. The extension metamodel, also shown in Fig. 12, that is generated by the subtyping operator shows that subtyping is satisfied. The extension metamodel contains renamings for the classes
,
and
to avoid name clashes.
The signature of the ATL operation should point to the extension metamodel, and the state machine that is an instance of the metamodel
must be adapted in order to take into account renamings. Such adaptation is automatically handled by the operator
, as explained in Sect. 6.4.
8 Related work
Steel et al. [20] formalized the notion of model type as a type group, generalizing the notion of object typing. Ours is formalized as a union type instead, enabling the possibility of having heterogeneous root objects in a model. In [17], as the isomorphic subtyping relation based on model type matching is too strict, a non-isomorphic subtyping relation based on adaptation was introduced in order to facilitate more flexible reuse of model transformation operations, such as class renamings. However, our subtyping relation approach can work both for nominal and structural type systems providing support for metamodels. Subtyping is not simply isomorphic as it works modulo class renaming for any possible renaming, which need not be known a priori.
Based on the notion of model subtyping in [20], Sen et al. [22] presented a mechanism to reuse model transformations by means of their effective metamodel \(\mathcal {M}^{\rightarrow }_{in}\). A model transformation is then made reusable by manually weaving aspects of the effective metamodel \(\mathcal {M}^{\rightarrow }_{in}\) with the metamodel \(\mathcal {M}^{\rightarrow }_{actual}\) for which the transformation is to be applied so that \(\mathcal {M}^{\rightarrow }_{actual}\) becomes a subtype of \(\mathcal {M}^{\rightarrow }_{in}.\) In our approach, the extension metamodel \(\mathcal {M}^{\rightarrow }_{actual,in}\), which facilitates the satisfiability of the model subtyping relation between two metamodel specifications, corresponds to the weaved metamodel that enables the reuse of the transformation. However, in our case, the extension metamodel is synthesized automatically and OCL constraints are considered.
Degueule et al. [40, 41] define model types using interfaces in Melange, providing support for flexible model loading and structural subtyping. On the one hand, flexible model loading is used to reuse operations across languages, e.g. to load a UML model with a new version of UML, while ensuring safety by checking that the model type of the loading operation and that of the inferred model type of the model (effective footprint of the model) are appropriately related via the subtypeOf relation. To implement this safety check Melange requires the user to declare the model type explicitly. The tool automatically generates adapters for each object type involved in the model type, decoupling object types from their implementation in EMF. On the other hand, model subtyping is used to ensure safe substitutability and corresponds to total isomorphic subtyping studied in [17], as discussed above.
In EMF-Subtyping, model types are represented using model type expressions, which are in correspondence with EMF metamodels via the syntactic transformation \( impl \) as shown in Sect. 5.2. Hence, each metamodel declares a model type, which is built as a union type of the structural types emerging from the classifiers in the package of the metamodel and the EMF metamodel is another representation of a model type expression. Reuse of operations across languages is done via subtyping polymorphism using the synthesized extension metamodel, which reifies the subtyping relation between the model type of the model and that of the operation to be reused as shown in Sect. 5.4. When such subtyping requires renamings or more complex mappings, retyping occurs on-demand and incrementally via the EMF-Syncer. The problem of flexible model loading, where there is uncertainty about the metamodel of a given model, is left out of the scope of this paper. Working on EMF metamodels as direct representations of model types has two advantages while retaining the ability to ensure type safety via subtyping: first, the modeller does not need to add additional syntax to models in order to declare model types and, second, it does not require an intermediate layer of adapters delegating dynamic dispatch to the EMF objects. The signature of model transformation operations needs to be updated to refer to the extension metamodel, although this change does not affect the implementation or body of the operation. Our approach added advantage is that contracts, both for model types and model transformation operations, and the subtyping relation can be semantically enriched with OCL constraints.
Leroy et al. [42] propose a metalanguage for specifying behavioural interfaces for executable DSLs in the GEMOC studio [43]. Such interfaces define sets of events, enabling interoperability and reuse of components for enriching the behavioural semantics of DSLs. Subtyping of interfaces fosters event abstraction hierarchies and implementation relations tie behavioural interfaces to specific operational semantics implementations. The semantics of the proposed metalanguage relies on an event manager to handle message exchange via behavioural interfaces, translating event occurrences from external tools into actual behaviour, and emitting event occurrences to external tools as a reaction to an observable behaviour of the interpreter. Hence, Leroy et al. promote reuse in DSLs equipped with operational semantics, whereas our work focuses on the reuse of structural and declarative behavioural specifications, represented with metamodel and model transformation specifications, and of their implementations. The notion of extension metamodel enables an implicit implementation relation that does not need to be declared explicitly and the re-typing mechanisms, supported by the EMF-Syncer , handle translations of input and output values from the context to the operation, and vice versa. An important difference in our approach consists in the safe reuse of requirements in structural and behavioural specifications, which need not be executable, in addition to reuse of specification implementations. Moreover, our approach comes equipped with tool support for verifying reuse and refinement, whereas guaranteeing the soundness of implementation relations is delegated to the language engineer in [42].
Regarding as-is reuse of model transformations, Lara et al. proposed a-posteriori typing specifications [44] for decoupling the role creation of a metamodel, when regarded as a template for new models, from their role interpretation, when regarded as a classifier for existing models. These specifications can be applied both to the type level and to the instance level, providing support for multiple, partial and dynamic typing. Bidirectional typing specifications are formalized in [45], providing support for backward compatibility to the original metamodel when reusing another operation. Our synthesis of the extension metamodel resembles the construction of the analysis metamodel for reasoning about OCL constraints in [45]. An important difference lies in the inference of inheritance relationships. When there are name clashes in features from the resulting superclasses and subclasses, they rename the features in the superclass and add an OCL constraint to enforce that their values are the same. We solve this problem by applying a refactoring that preserves the type of the feature in the subtype, which may be more restrictive. This refactoring avoids duplicate code and skipping the use of auxiliary OCL constraints. Their approach cannot solve the problem described in the introduction as typing specifications are defined explicitly and require knowledge about the involved metamodel specifications a priori. The motivation behind our approach focuses on checking subtyping automatically without up-front manual intervention, leaving out explicit adaptation. In our case, retyping is implicitly handled through the model subtyping relation, and explicit re-typings (type coercion) are only required when reusing EMF model transformation operations, as explained in Sect. 6.3. On the other hand, our approach is framed at the type level.
Varró et al. also use ontological typing of objects in VPM [46] for defining metamodel conformant models. More interestingly, they provide a refinement calculus that handles (multiple) inheritance and instantiation, which provides a subsumption relationship between metamodels. Although they consider refinement of behavioural specifications, they can only reason with a subset of the metamodels expressible in EMF as they do not consider well-formedness constraints.
Graph constraints, introduced by Heckel et al. in [47] for plain graphs, and later extended by Taentzer et al. to graphs with type node inheritance in [48], capture a notion of metamodel specification that is similar to the one that we are dealing with. Propagation of constraints along model transformations, which can be regarded as adaptations, specified by triple graph grammars, is considered by Harmut in [49]. Constraint propagation determines when a target metamodel, which can have its own constraints, is compatible with respect to the constraints of the source metamodel. Our proposal does not require an explicitly defined up-front mapping, and the underlying theory is available in an executable tool.
Zschaler [50] introduced an abstract notion of model type with constraints as a graph, with class names as nodes and associations as edges, coupled with a conjunction of first-order constraints over the graph signature. A model matching relation is used to match a metamodel to its model type, and a type system is provided to infer the minimal model types of a model transformation operation. The constraints that can be inferred refer to multiplicity bounds and to whether a class is abstract or not. When a model transformation operation is invoked over a model, the type system checks that the model satisfies the constraints of the model type associated with the parameter. Thus, model subtyping is implicitly taken care of by constraint satisfaction allowing for reuse. The inferred minimal model type is similar, in its intent, to the model type of an effective metamodel, which is assumed to be inferred from a model transformation, in our approach. On the other hand, the notion of model type has not been discussed independently of type inference for a model transformation operation and is, then, tied to the language used for defining model transformation operations, which is, at present, less expressive than those used in practice.
Bruel et al. [38] classified state-of-the-art approaches for reuse model transformation operations across metamodels. However, metamodels are not enriched with OCL constraints, and behavioural subtyping for the operations is not considered.
None of the approaches researched above considers reasoning on metamodels, which are unrelated a priori, enriched with OCL constraints in model subtyping.
Regarding refinement, Büttner et al. [51] propose a notion of contract-based transformation specification and of their (weak) refinement that is similar to our notion of operation specification and subtyping, respectively. They also use model finders, integrated into USE, to check the refinement of contract-based transformation specifications. In our presentation, however, we have used subtyping as a unifying framework both for structural and behavioural refinement, in addition to other use cases. Vallecillo et al. [52] proposed Tracts to encode transformation contracts using OCL invariants and proposed a notion of refinement that is semantically equivalent to ours. Refinement checking is based on testing, relying on the manual creation of input test models and the executability of the refined specification. In our case, as well as in [51], operation specifications need not be executable and manual creation of input models is not required.
9 Concluding remarks
The notion of model subtyping has been revisited from a subsumption perspective. Structural model subtyping has been extended to metamodel specifications as the problem of whether two groups of OCL constraints are compatible when their metamodels (or class diagrams) are not related a priori. We have implemented a procedure for solving this problem that, in addition, gives us: an extension metamodel for reusing model transformation operations whose signature involves the supertype metamodel when the metamodel specifications are compatible; and the reason why their metamodels are not subtype of each other, or else a metamodel-conformant model that satisfies the constraints of the subtype but not some of the supertype, when they are not compatible. The procedure is decidable when appropriate bounds are used for finding the witness model.
Structural model subtyping can be used for developing metamodel specification refinements without losing expressive power with respect to other approaches to subtyping. Structural model subtyping is robust enough so as to provide some adaptations for free without having to provide any explicit information relating metamodel specifications a priori, becoming both isomorphic and non-isomorphic [17]. We have also discussed that structural model subtyping provides a convenient theoretical framework to deal with dynamic, partial and multiple model typing. Nevertheless, structural model subtyping suffers from being too liberal in contexts where all the object subtypings need to be analysed. Our tool provides a recommendation algorithm that suggests an optimal strict model subtyping to mitigate this threat to usability. Including a more prescriptive approach that limits the number of valid object subtypings or dictates how subtypings should be performed with user information provided upfront is a potential extension.
Model subtyping has been generalized to model transformation operation specifications, which need not be executable, to ensure safe application of operations, substitutability and operation specification refinement, hence providing support for behavioural subtyping. This approach is independent of the language used to implement model transformations and is amenable for automatically verifying operation specifications.
The logic that was reused from TOTEM-MDE [36] for mapping Ecore models and OCL constraints to the USE validator in [12] has since been generalized in the EFinder [53], which accepts different dialects of OCL and provides support for model consistency, example generation, partial solution completion and scrolling. Exploring structural subtyping together with such additional facilities is left for future work.
Acknowledgements
The author thanks the anonymous reviewers for their insightful and helpful feedback.
Open AccessThis article is licensed under a Creative Commons Attribution 4.0 International License, which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons licence, and indicate if changes were made. The images or other third party material in this article are included in the article’s Creative Commons licence, unless indicated otherwise in a credit line to the material. If material is not included in the article’s Creative Commons licence and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder. To view a copy of this licence, visit http://creativecommons.org/licenses/by/4.0/.
Publisher's Note
Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.
The specification does not mandate how successor snapshots are to be managed. An implementation may involve ATL rules, and the corresponding ATL engine selects how to process snapshots of the system.
The incompatibility relation has been relaxed with respect to bidirectionality of references, so that opposite types only need to be related via subtyping to be compatible, without necessarily requiring the same exact type. The last clause in the incompatibility relation was defined as \( op (\rho _1) \ne op (\rho _2) \) in [12].
This proposition relies on the following observation: a system state for a metamodel \(\mathcal {M}^{\rightarrow }_{}\) is defined as a structure \(\sigma (\mathcal {M}^{\rightarrow }_{})=(\sigma _{\textsc {Class}},\sigma _{\textsc {Att}},\sigma _{\textsc {Assoc}})\) in [11], where \(\sigma _{\textsc {Class}}\) resembles \(N_G\), \(\sigma _{\textsc {Att}}\) resembles \(E_{NA}\), and \(\sigma _{\textsc {Assoc}}\) resembles \(E_G\). The direction of the set inclusion is justified by the fact that E-graphs in \(\mathbf {AG}\) are not necessarily typed.
Noting: that the syntax we introduced for object models only considers binary associations (without an explicit name for the association); that attribute operation signatures \( p : \textsc {Class}\rightarrow \mathcal {B} \sqcup \textsc {Enum}\) can be extracted from propositions of the form \( p (c)\) and \( type ( p )=t\) where \(t \in \mathcal {B} \sqcup \textsc {Enum}\); and that compositions are immaterial in USE format.
attribute of the transition) or are triggerless, e.g. they are completion transitions. These metamodels also include notions for engineering the execution context of a model interpreter, namely the notions of
to mark nodes as already mapped in \(\mathcal {M}_g\), and
to indicate which states have been observed in \(\mathcal {M}_{sm}\).
as the ATL transformation has no awareness of the classifiers in the subtype model. Type coercion is used in the last step to down cast the resulting state machine to an instance of the subtype model, by retyping object
to the class
.
. In its metamodel, the classifier
corresponds to the snapshot notion, which contains a marker for the state currently being observed. In addition, each state machine may have one predecessor, representing the previous snapshot in the execution. The invariant (top, right) specifies the behavioural semantics of the interpretation model transformation in Listing 11. Figure 3 shows the semantics of the model interpreter (bottom), consisting of two transformations, given an initial state machine snapshot. Hence, by comparing metamodel specifications that contain behavioural semantics, the subtyping operation is also able to reason about behavioural properties of DSLs, both to reuse behavioural semantics and to ensure valid behavioural refinements. This example has been chosen to illustrate how the operation specification subtyping relation can be used to check refinement of model transformation operations. However, the operation specification subtyping relation is more general, as it does not require an initial snapshot to determine whether subtyping is satisfied.
) or by designating different types of classes by using references (e.g. by using a reference
from the class
to the class
).
and
is defined as follows:
. For containment types, the constraint is encoded likewise, but we fetch the object identifier of the contained object by inspecting the field \( id \).
and
from \(\mathcal {M}^{\rightarrow }_{sm}\) have been preserved. In \(\mathcal {M}^{\rightarrow }_{sm,g},\) two virtual classes,
and
, have been extracted in two consecutive iterations.
pointing to an object
through the reference
, that are not valid models in \(\mathcal {M}^{\rightarrow }_{sm}\). In addition, the preservation of the constraints of structural features in \(\mathcal {M}^{\rightarrow }_{ sub }\) when extracting virtual classes forces \(\mathopen {\llbracket }{\mathcal {M}^{\rightarrow }_{ sub , super }}\mathclose {\rrbracket } \subseteq \mathopen {\llbracket }{\mathcal {M}^{\rightarrow }_{ super }}\mathclose {\rrbracket }.\) For instance, in the example, objects of type
are of type
as the properties of
are included in
.
, which can be automatically coerced to the type
as explained in Sect. 6.3.
association in the example of Sect. 2.3.
. In this example, operation specification subtyping is trivially satisfied, as the operation is not defined for the supertype. However, subtyping is still helpful for automatically finding unintended inconsistencies between the effects of the operation and the valid class of models. Cabot et al. [34] described an alternative approach for capturing declarative specifications of model-to-model transformations using OCL invariants, without having to include temporal information in the metamodel. Our approach would also work with this alternative representation, after adapting the notion of satisfaction of behavioural constraints, although the resulting behavioural specifications would be more verbose and, thereby, more expensive to verify. While our notion of operation specification is based on invariants, operation specifications given in terms of OCL pre- and post-conditions can be translated to the proposed representation by using the filmstripping technique proposed by Hilken et al. [35], implemented in USE.
, for retype a subtype-conforming model, and
, for retyping back the extension-conforming model to its original subtype.
and
are not covered by the supertype metamodel in \( synth (\mathcal {M}^{\rightarrow }_{sm},\mathcal {M}^{\rightarrow }_{g},\prec ^s),\) which is useful for selecting a specific strict subtyping.
with a containment reference
. The subtyping relation, illustrated with a dashed arrow, identifies the class
as subtype of both
and
at the same time. However, the metamodels defining state machines (c)) and projects (d)) are not valid subtypes of the abstract container metamodel. In the state machine metamodel,
is not a subtype of
since the feature
cannot be matched to the feature
. The reason for this is that the type
is not a subtype of the type
, as it has no feature corresponding to
. In the project metamodel, the type
is not a subtype of the type
because the type of the feature
is not compatible with the type of the feature
, as its type
is not a subtype of the type
.
in c) and the class
in d) would be removed, leaving a singleton class inheritance relationship in each metamodel that would have to be flattened.
, a modified version of the state machine metamodel, for models of a metamodel
. In Fig. 11, metamodel
enables observable behaviour in state machines, where state observations are timestamped. Code generation from state machines to the format proposed by Fowler [39] is implemented using ATL. Figure 11, bottom part, from left to right, shows the model transformation, a state machine and its serialized counterpart.
of metamodel (partial supertype),
(pruned, total supertype),
(subtype). Bottom (from left to right): ATL operation defined for
; state machine as instance of
; output of operation
captures the dual notion of observability by using events to mark when a transition is triggered. The metamodel
is not exactly a supertype of the metamodel
. This change is not a structural refinement and is not backward compatible using traditional object-oriented extension mechanisms. In addition, metamodel
is enriched with an OCL constraint on the name of the events that can be created:
of the metamodel together with the OCL constraint is not a refinement of
. Figure 12 shows the complement of the supertype obtained from the structural subtyping operator, explaining why models of metamodel
can only be partially typed by metamodel
. To resolve this issue, the complement of the supertype is pruned from metamodel
and the subtyping operator is then used to check whether the metamodel
is supertype of metamodel
. The extension metamodel, also shown in Fig. 12, that is generated by the subtyping operator shows that subtyping is satisfied. The extension metamodel contains renamings for the classes
,
and
to avoid name clashes.
must be adapted in order to take into account renamings. Such adaptation is automatically handled by the operator
, as explained in Sect. 6.4.