=Paper=
{{Paper
|id=Vol-1500/paper7
|storemode=property
|title=A Diagrammatic Approach to Model Completion
|pdfUrl=https://ceur-ws.org/Vol-1500/paper7.pdf
|volume=Vol-1500
|dblpUrl=https://dblp.org/rec/conf/models/RabbiLYK15
}}
==A Diagrammatic Approach to Model Completion==
https://ceur-ws.org/Vol-1500/paper7.pdf
A Diagrammatic Approach to Model Completion
Fazle Rabbi Yngve Lamo Ingrid Chieh Yu
Bergen University College Bergen University College University of Oslo
University of Oslo Yngve.Lamo@hib.no ingridcy@ifi.uio.no
Fazle.Rabbi@hib.no
Lars Michael Kristensen
Bergen University College
Lars.Michael.Kristensen@hib.no
Abstract
Metamodelling plays an important role in model-driven engineering as
it can be used to define domain-specific modelling languages. During
the modelling phase, software designers encode domain knowledge
into models which may include both structural and behavioural as-
pects of a system. In this paper we propose a diagrammatic approach
to aid the software designer to complete partial models and thereby
reduce modelling effort. We introduce a declarative approach where
we define completion rules that are executed by the use of model
transformations. We also study the termination of such model trans-
formation systems and provide sufficient conditions for termination
by generalizing existing work on termination of model transformation
systems.
1 Introduction
Model Driven Engineering (MDE) [Sch06] is considered to be an efficient way of improving the quality of
software and enhance software development productivity by automating repetitive, error-prone, and time-
consuming tasks. In MDE, models are first–class artefacts of the software development process where models
are incrementally refined starting from requirements and eventually used for code generation. Metamodels serve
as the underlying foundation defining the modelling languages used to capture domain-specific knowledge and
concepts.
In the process of development, software designers are often confronted with a variety of inconsistencies
and/or incompleteness in the models under construction [MVDS07]. In particular, the modeller will most of
the time be working with a partial model not conforming (i.e., not being typed by and satisfying modelling
constraints) to the metamodel that defines the modelling language being used [SBP07]. As an example, consider
the following example from the healthcare domain. Figure 1(a) shows a metamodel M2 (in this case a class
diagram) and Figure 1(b) shows a partial model (in this case an object diagram) M1 typed by M2. The typing of
the nodes are represented by dotted arcs. In this example, Bryan works at Ward10; Ward10 is controlled by the
Emergency department. The model M1 is a partial model as it is not satisfying the following domain constraint:
“An employee who is involved in a ward must work in the controlling department”. This constraint is defined
in the metamodel M2 by the OCL constraint shown to the upper right at Figure 1. Since Ward10 is controlled
by the Emergency department, Bryan must work at the Emergency department.
In the above example, the partial model M1 can be transformed into a model conforming to the metamodel
M2 by adding an arc from the Emergency department to Bryan which is missing in M1. Figure 1(c) shows a
model M1∗ that conforms to the metamodel M2. Clearly, the productivity of the modeller could be improved by
providing editing support that could either automatically add such missing model elements or make suggestions
Attached OCL constraint
wards context Ward
Ward * inv rule:
worksAt *
self.caregivers ->
(a)
includesAll(self.department.caregivers)
caregivers * 1..1 department
caregivers 1..*
Caregiver * departments Department
M2
Bryan Emergency Bryan Emergency
(b) (c)
Ward10 M1 Ward10 M1*
Figure 1: (a) Model M2, (b) a partial model M1 (not conforming to M2), (c) a completed model M1∗ (conforming
to M2)
based on completion rules to assist the modeller in completing the model. In many respects, this idea is similar
to code completion features as found in IDEs. More generally, modelling effort could be reduced by providing
editing support for automated rewriting of models so that they conform to the modelling language used. Such
rewriting may also involve the deletion of model elements.
The contribution of this paper is a framework for rewriting partial (incomplete) models so that they conform
to the underlying metamodel. Our approach is based on rewriting of models by means of model transformation
rules which supports both addition and deletion of model elements. We refer to them as completion rules.
The proposed framework has been developed as an extension of the Diagram Predicate Framework (DPF)
[LWM+ 12] which supports multilevel metamodelling. This approach is, however, general and could be used
for other modelling frameworks as well. DPF is a language independent formalism for defining metamodelling
hierarchies which provides an abstract visualization of concrete constraints. In the extended DPF, one can
graphically specify completion rules. Our framework exploits the locality of model transformation rules and
provides a foundation that enables automated tool-support to increase modelling productivity. In order to
guarantee termination of the rewriting, we provide a set of sufficient termination criteria. A link to the
prototype implementation of the proposed framework is available at http://dpf.hib.no where one can graphically
design modelling artefacts in a web browser, apply the completion rules and check for termination.
The rest of this paper is organised as follows. Section 2 provides background knowledge on DPF, section
3 provides an outline of the partial model completion with an example, section 4 formalizes the concept of
diagrammatic rewriting systems, and section 5 presents sufficient termination criteria. In section 6, we briefly
discuss some related work. We assume that the reader is familiar with basic category theory and graph
transformation systems[BW95], [EEPT06].
2 Diagrammatic Modelling with DPF
In order to work with partial models and completion rules in a formal framework; we extend the Diagram
Predicate Framework (DPF) [Rut10]. DPF provides a formal diagrammatic approach to metamodelling based
on category theory and model transformations. In the DPF approach, models at any level are formalised as
diagrammatic specifications which consist of graphs and diagrammatic constraints. Figure 2 shows an example
of a DPF model (specification) S1 with its metamodel (specification) S0 . The graphs represent the structure of
the models; constraints are added into the structure by predicates. The metamodel (specification) S0 provides
the typing for the model (specification) S1 . Nodes in model (specification) S1 are either of type Class or
DataType; edges in S1 are either of type Reference or Attribute. Table 1 shows a list of predicates used for
constraining the specification S1 . Each predicate has a name (p), a shape graph (α(p)), a visualisation and a
semantic interpretation. The semantic of a predicate is provided by a set of instances. The (atomic) constraining
constructs which are available for the users of the modelling language are provided in the signature Σi . A
signature consists of a collection of diagrammatic predicates. Table 2 shows how the predicates are constraining
the specification S1 by a graph homomorphism δ : α(p) → S from the shape graph to the specification.
In DPF, a modelling language is formalised as a modelling formalism (Σi , Si , Σi−1 ) where i and i − 1 represent
two adjacent modelling levels. The corresponding metamodel of the modelling language is represented by the
specification Si which has its constraints formulated by predicates from the signature Σi−1 . A DPF metamod-
elling hierarchy consists of (a possible stack of) metamodels, models, and instances of models. A metamodel
specification determines a modelling language, the specification of a model represents a software system, and
Table 1: Predicates of a sample signature Σ0
p αΣ0 (p) visualisation Semantic Interpretation
f must have at least n and at most m instances. For-
[mult(n,m)] f X f Y
1 2 [n..m] mally, ∀x ∈ X : m ≤ | f (x)| ≤ n, with 0 ≤ m ≤ n and
n≥1
f f For each instance of f there exists an instance of g or
[inverse] 1 2 X [inv] Y vice versa. Formally, ∀x ∈ X, ∀y ∈ Y : y ∈ f (x) iff
g g x ∈ g(y)
2 Y
g f
[composite] g f S f ), there exists an instance of
For each instance of (g;
[comp] h. Formally, ∀x ∈ X : { f (y) | y ∈ g(x)} ⊆ h(x)
1 3 X Z
h h
the instances of models typically represent possible states of a software system. In this paper, we present a new
type of DPF construct named completion rules based on model transformation rules. The completion rules are
connected to (domain) constraints.
Reference 0
Attribute
Data Type Class (a)
Typing
1
Ward
wardDeps
[comp]
wardPats
wardEmps
[comp]
(b)
systolic
[1.. 1]
empDeps [1.. ]
8
Nat Patient Caregiver [inv] Department
diastolic dataAccess
depEmps
Figure 2: a) Metamodel S0 , b) Model S1
3 Model Completion Example
The completion rules defined in a metamodel are used to complete a partial model. We introduce requirement
R1-R5 for an envisioned system from the healthcare domain. These requirements specify the constraints of a
system. Completion rules are used to automatically complete a partial model not satisfying these constraints.
R1. A Caregiver (e.g., nurse, doctor) must work for at least one Department.
R2. A Caregiver may work for more than one Department.
R3. A Ward must be controlled by exactly one Department.
R4. A Caregiver who is involved in a Ward, must work for its controlling Department.
R5. All Caregivers assigned to a Ward have access to the patients information who are admitted to the same Ward.
Figure 3(a) shows a DPF model (specification) S1 developed from the above requirements. The metamodel
(specification) of S1 was shown in Figure 2(a). In S1 we used the signature Σ0 from Table 1 to define the set
CS1 of atomic constraints. R1 and R2 is encoded in S1 by the [mult(1, ∞)] predicate on the edge empDeps; R3
by the [mult(1, 1)] predicate on the edge wardDeps; R4 by the [composite] predicate on edges wardEmps, wardDeps
and empDeps where (wardEmps; wardDeps) ⊆ empDeps; and R5 by the [composite] predicate on edges wardEmps,
wardPats and dataAccess where (wardEmps; wardPats) ⊆ dataAccess.
Figure 3(b) shows a candidate instance ι : I → S of S1 (also represented as (I, ι)) where S is the underlying
graph of specification S1 . Even though I is typed by S, (I, ι) is not a valid instance of S1 since it does not satisfy
the predicates [mult(1, ∞)] and [composite]. This can be checked from the pullback operation shown in Figure 4.
Table 2: The set of atomic constraints CS1 of S1
(p, δ) αΣ0 (p) δ(αΣ0 (p))
empDeps
f
([mult(1, ∞)], δ1 ) 1 f 2 Caregiver
1 Department 2
wardDeps
([mult(1, 1)], δ2 ) 1 f 2 Ward1
f
Department2
depEmpsf
f
Caregiver1 Department2
1 2
([inverse], δ4 ) g empDepsg
Ward2
2
wardDeps f
g f wardEmpsg
empDeps
1 3 Caregiver h
Department3
([composite], δ5 ) h 1
Ward2
2
wardPats f
g f wardEmpsg
dataAccessh
1 3 Caregiver1 Patient3
([composite], δ6 ) h
1
Ward
wardDeps
[comp]
wardPats
wardEmps
[comp]
(a)
systolic [1.. 1]
empDeps [1.. ]
8
Patient Caregiver [inv] Department
Nat dataAccess
diastolic
depEmps
I
Joseph
140 :sy
sto
lic
John Bryan Emergency (b)
ps
m
st olic
dE
:wardEmps
:dia
ar
90
:w
Ward10
:wardPats :wardDeps
Figure 3: a) A DPF model S1 = (S, CS1 : Σ2 ), and b) an instance (I, ι) of S1
δ1 ι
By performing a pullback of αΣ0 ([composite]) −→ S ← − I, we extract the fragment of the graph that is affected by
the [composite] constraint. The graph homomorphism ι∗ (see Figure 4) is not a valid instance of the [composite]
as the semantics of the [composite] predicate is not satisfied. In this example, Bryan works at Ward10; Ward10
is controlled by the Emergency department. Since Ward10 is controlled by the Emergency department, Bryan
must work at the Emergency department. Also, the caregivers are supposed to work for at least one department
which is missing in ι : I → S of S1 . Figure 5 shows a screenshot of the editor that highlights which part of the
model instance violates the constraints.
In the next section, we extend DPF with model transformation rules which allows us to incorporate model
completion rules. We augment the above mentioned example with completion rules at the meta-model level
that can be used as a basis for automatically removing the inconsistencies of the partial model (I, ι). Table 3
shows some completion rules linked to predicates. Completion rules for a predicate ensures that the predicate
becomes satisfied. The semantics of completion rules are defined by coupled transformation rules [SLK11]
[Bec08] with negative application conditions as in Table 3. Negative application conditions are typically used
0([composite])
1 2
Ward
1 f
wardDeps
[comp] g
wardPats
wardEmps
[comp] 1 3
h
systolic [1.. 1]
empDeps [1.. ]
8
Patient Caregiver [inv] Department
Nat dataAccess
diastolic
depEmps
PB *
I
Joseph
140 :syst
olic Bryan Emergency
John Bryan Emergency
ps
c
m
toli :wardEmps
:wardEmps
ias
90 :d dE
ar
Ward10
:w
:wardDeps
:wardPats Ward10 :wardDeps *
1
ι∗ δ∗1 δ1 ι
Figure 4: Pullback αΣ0 ([composite]) ←
− O∗ −→ I of αΣ0 ([composite]) −→ S ←
−I
Figure 5: An inconsistent instance (I, ι) (bottom) of S1 (top)
in graph transformations to prohibit an infinite number of rule applications. We use a special type of coupled
transformations where the metamodels remain unchanged [RMWL12]. Notice that the matching patterns and
negative application conditions are represented in the same diagram in Table 3 to make it more readable.
Negative application conditions on model elements are represented by a strike through the corresponding
model elements in the diagram to represent that they must not exist while matching.
By applying the completion rules from Table 3 on (I, ι), the partial model is updated to become a model, (I∗ , ι)
which conforms to its metamodel. Once we apply the completion rules for [inv − comi[inv] and [comp − comi[comp]
Table 3: Completion scheme for predicates and completion rules of S1
ζ(Cp )
Cp Interpretation
(N → αΣ (p)) ← (L → αΣ (p)) (K → αΣ (p)) (R → αΣ (p))
f f
f [inv]
X [inv] Y X Y
X [inv] Y
g g
g :f
:f
:f
x y x y
:g x y :g :g
[inv-comi[inv] derive an edge y − → x (if
f f f
it does not exist) from
[inv] X [inv] Y X [inv] Y
X Y the existence of an edge
g g :f
g
x−
→ y or vice versa.
:f :f
x y x y x y
:g :g :g
:h
[comp-comi[comp] derive an edge x − → z (if
Y Y Y
it does not exist) from
g
f
g
f
g
f the existence of edges
[comp] [comp] [comp] :g :f
X Z X Z X Z
x−
→ y and y −
→ z.
h h h
x z x z x z
:h :h
:g :g :g
:f :f :f
y y y
1
Ward
wardDeps
wardPats
[comp]
wardEmps
[comp]
(a)
systolic [1.. 1]
empDeps [1.. ]
8
Patient Caregiver [inv] Department
Nat dataAccess
diastolic depEmps
:e
m
I*
Joseph pD
s :d
140 :sy Acces ep ep
sto
lic :data Em s
John :empDeps ps
Emergency (b)
:dataAccess Bryan
c
toli :depEmps
ps
s
:dia
m
90 :wardEmps
dE
ar
:w
:wardPats Ward10 :wardDeps
Figure 6: a) A specification S1 = (S, CS1 : Σ0 ) and b) an instance (I∗ , ι) of S1
on (I, ι), we obtain the instance of specification S1 shown in Figure 6. Bold arcs (also shown with a green color)
in Figure 6 represent the additional edges derived from the application of completion rules. We do not have
deleting rules in this example, but in general it is possible to have deletion rules to repair e.g., multiplicity
constraints [TMAL13].
4 Diagrammatic Model Completion
Our diagrammatic rewriting system is based on completion rules. Completion rules are typed coupled trans-
formation rules where type graphs are not changed by the transformation. The rules are linked to predicates
and they are applied to a partial model to correct inconsistencies. We use the standard double-pushout (DPO)
approach [EEPT06] for defining completion rules. In this section we give a formal definition of completion rules
and formalize its application and matching.
Definition 1 (Completion scheme of a predicate and completion rules) Let Σ = (PΣ , αΣ ) be a signature. A
completion scheme Cp for a predicate p ∈ PΣ , is given by a symbol cp, and a set of completion rules ζ(Cp ) where the
meta-models remain unchanged. A rule r ∈ ζ(Cp ) of a completion scheme of a predicate Cp has a matching pattern (L), a
gluing condition (K), a replacement pattern (R), and an optional negative application condition, NAC (n : L → N) where
L, N, K, R are all typed by the arity αΣ (p) of the predicate p.
A completion rule as defined in Definition 1 is illustrated in the following figure. The matching pattern and
replacement pattern are also known as left-hand side and right-hand side of a rule, respectively. In the figure,
k and l are injective morphisms. A completion rule is nondeleting if K = L. In this case we have an injective
morphism L ,→ R.
id id id
αΣ (p) αΣ (p) αΣ (p) αΣ (p)
ιN ιL ιK ιR
N n L K R
k l
Figure 7 illustrates a rule associated with the [composite] predicate where the graphs L, N, K, R are all typed
by the arity of the [composite] predicate.
([composite])
Y
g [comp]
f
X h Z
Typing
y y y y
:f :f :f :g :f
:g :g :g
x z x z x z x :h
z
:h
N LHS (L) Glue (K) RHS (R)
Figure 7: A transformation rule linked to the [composite] predicate
Since the rules are not directly linked to a model, they can be reused by constraining a model with appropriate
predicates.
Definition 2 (Match of a completion rule). Let Cp be a completion scheme of a predicate with a set of completion rules
ζ(Cp ). A match (δ, m) of a rule r ∈ ζ(Cp ) is given by an atomic constraint δ : αΣ (p) → Si−1 and a match m : L → Si such
that constraint δ and match m together with typing morphisms ιL : L → αΣ (p) and ιSi : Si → Si−1 constitute a commuting
square: ιL ; δ = m; ιSi as in the diagram below.
δ
αΣ (p) Si−1
ιL = ιSi
m
L Si
Now we consider the satisfaction of a negative application condition of a completion rule. A rule is applied
as long as it satisfies its negative application condition which is typically expressed by a graph structure in a
graph transformation system.
Definition 3 (Satisfaction of a NAC of a completion rule) A match (δ, m) of a rule r ∈ ζ(Cp ) satisfies a NAC (n :
L → N) if there does not exist an injective graph morphism q : N → Si with n; q = m such that the typing morphisms
ιN : N → αΣ (p) and ιSi : Si → Si−1 constitute a commuting square: ιN ; δ = q; ιSi as shown in the diagram below. This is
written (δ, m) |= NAC.
δ
αΣ (p) αΣ (p) Si−1
id δ
ιN ιL ιSi
n m
N L Si
,
q
Definition 4 (Application of a completion rule) Let Cp be a completion scheme of a predicate with a set of completion
rules ζ(Cp ). A rule r = ((N → αΣ (p)) ← (L → αΣ (p)) ← (K → αΣ (p)) → (R → αΣ (p))) ∈ ζ(Cp ) transforms a partial
model (Si , ιSi ) to (S∗i , ιS∗i ) if there exists a match (δ, m) where (δ, m) |= NAC. The transformation consist of two commuting
cubes and two pushout diagrams (PO1 and PO2) as shown below:
id id id
αΣ (p) αΣ (p) αΣ (p) αΣ (p)
δ δ δ δ
id0 id0
Si−1 Si−1 Si−1
ιN
ιSi ιS∗i
N n , L K R
m (PO1) (PO2) m∗
q 0
Si Si S∗i
Note that (S∗i , ιS∗i ) could be a partial model and in that situation, further application of completion rules are
required to obtain a a model that satisfies all the constraints. Our framework supports the execution of rules
in two different ways: one can interactively apply the rules where the user guides the execution order; or
automatically considering all possible orderings of rule execution. In the latter case, it is important to perform
an analysis to ensure that the execution of the transformation rules will eventually terminate.
5 Termination Criteria
In this paper we propose a termination analysis based on the principles adapted from layered graph grammars
[EEPT06]. In a layered typed graph grammar, transformation rules are distributed across different layers. The
transformation rules of a layer are applied as long as possible before going to the next layer. Ehrig et al [EEPT06]
distinguished between deletion and nondeletion layers where all transformation rules in deletion layers delete
at least one element and all transformation rules in nondeletion layers do not delete any elements. A set of
layer conditions was specified in [EEPT06] that need to be satisfied by each layer k to guarantee termination.
Transformation rules in nondeletion layers must have negative application conditions. The layer conditions
do not permit a rule r to use an element x of a given type t for the match if any element of type t has been
created in a layer k0 ≤ k. The layer conditions also imply that the creation layer of an element of type t must
precede its deletion layer. This restriction prevents the repetitive application of a particular rule. This layered
typed graph grammar approach is suitable for situations where repetitive application of rules are not required.
Unfortunately, there are many situations where repetitive application of rules are desirable such as to compute
transitive closure operations [LPE07].
We generalize the layer conditions from [EEPT06] allowing deleting and non-deleting rules to reside in the
same layer as long as the rules are loop-free. Furthermore, this generalization permits a rule to use newly
created edges allowing us to perform transitive closure operations. To achieve this, we rely on a loop detection
algorithm that overestimates the existence of a loop from a set of rules. The loop detection algorithm is based
on the following sufficient conditions for loop freeness. Let Rk be the set of rules of a layer k.
• If a rule ri ∈ Rk creates an element x of type t, then ri must have an element of type t in its NAC,
• If a rule ri ∈ Rk deletes an element of type t, then there is no rule in r j ∈ Rk that creates an element of type t
Note that we are assuming, that there is a finite number of rules in each layer and that the rules are applied
on a finite input graph. The algorithm guarantees termination if all the rules for each layer satisfies the above
mentioned conditions. A complete specification of the algorithm and a formal proof of correctness is available
as technical report on http://dpf.hib.no/publications.
6 Related and Future Work
Partial models have been used in MDE for various purposes. It has been used for modelling with uncertainty
by Salay et al. in [SFC12]. They proposed four types of partiality that can be defined in a modelling language–
independent way. Their definition of metamodel consists of a First Order Logic theory that includes a set of
sentences representing the well–formedness constraints. Modelling with uncertainty is essential in situations
such as: i) the requirements are not clearly specified, ii) alternative resolution to inconsistency is present, and
iii) stakeholders opinions differ. In this article, we focus on precise modelling of systems with metamodelling
assuming the requirement is clearly specified.
An approach similar to our work was presented in [SBP07] where the authors presented a methodology to
automatically solve partial model completion problems. They transformed a partial model, its metamodel, and
additional constraints to a constraint logic program (CLP). The metamodel specifies the domain of possible
assignments for each and every property. This information is being used by the CLP to complete a partial
model object. They provided an algorithm to generate code that assigns a domain of values to the attributes and
relationships. When the CLP is queried, a solver selects values from the domain of each property such that the
conjunction of all the constraints is satisfied. In our approach, we use multilevel metamodelling for specifying
domain models. We use diagrammatic approach to define completion rules and use model transformations to
derive a complete model instance that satisfies the predicate constraints.
An automated approach for detecting and tracking inconsistencies in real time was presented in [Egy11].
The author listed 24 consistency rules that cover the most significant concerns of keeping sequence diagrams
consistent with class and statechart diagrams and evaluated the rules on UML design models. While their
approach is based on the syntactical constraints of UML diagrams, ours is based on domain specific diagrammatic
constraints. In our approach, the completion rules are graphically formulated, customizable, and vary from one
domain to another.
The eMoflon tool [ALPS11] is built on the Eclipse Modelling Framework (EMF), using Ecore for metamod-
elling that supports rule-based unidirectional and bidirectional model transformation. eMoflon is featured with
MOF 2.0 compliant code generation and concentrates on bidirectional model transformations with triple graph
grammars and their mapping to unidirectional transformations. In contrast, we proposed metamodelling with
partial model completion based on coupled model transformation and provided termination analysis for such
model transformation.
In [BPP10], Bottoni et al. proposed an approach to the identification of a sufficient criterion for termination
of graph transformations with negative application conditions. Their approach is based on labelled transition
systems and they use a double pushout approach to graph transformation. Their approach is focused on the
termination of a single non-deleting rule. A graph transformation system typically have multiple rules and
termination becomes a complex issue with multiple rules. Ehrig et al. presented a layered graph transformation
systems where rules are grouped into different layers [EEPT06]. Mixing deleting and non-deleting rules in a
layer is not possible. In this paper, we generalize the layer conditions from [EEPT06] allowing that deleting and
non-deleting rules remains in the same layer as long as the rules are loop-free. Furthermore, we permit a rule
to use newly created edges allowing us to perform transitive closure operation.
Termination criterion for double pushout transformation that covers transitive closure was addressed in
[LPE07] by Levendovszky et al. where the authors proposed a transformation based on E-concurrent produc-
tion which is an amalgamation technique for concurrent execution of rules. This approach is based on the
construction of concurrent rules from different combination of productions. A disadvantage of their approach
is that it is hard to find all the possible sequences of graph productions, and prove that the corresponding series
of cumulative ‘left-hand side’ exceeds all limits which is required to show termination.
An application of partial model completion is in the evolving software engineering process. In many cases,
software models need to migrate because of the evolution of software requirements and/or modelling languages
[TMAL13]. The concept of partial models is applicable also in this setting if accompanied by rewriting rules
and would potentially be able to automate the model migration process.
References
[ALPS11] Anthony Anjorin, Marius Lauder, Sven Patzina, and Andy Schürr. eMoflon: Leveraging EMF
and Professional CASE Tools. In 3. Workshop Methodische Entwicklung von Modellierungswerkzeugen
(MEMWe2011), 2011.
[Bec08] Steffen Becker. Coupled model transformations. In Proceedings of the 7th International Workshop on
Software and Performance, WOSP ’08, pages 103–114, NY, 2008. ACM.
[BPP10] Paolo Bottoni and Francesco Parisi-Presicce. A termination criterion for graph transformations with
negative application conditions. ECEASST, 30, 2010.
[BW95] Michael Barr and Charles Wells, editors. Category Theory for Computing Science, 2nd Ed. Prentice Hall
International (UK) Ltd., Hertfordshire, UK, 1995.
[EEPT06] Hartmut Ehrig, Karsten Ehrig, Ulrike Prange, and Gabriele Taentzer. Fundamentals of Algebraic Graph
Transformation. Monographs in Theoretical Computer Science. Springer, 2006.
[Egy11] Alexander Egyed. Automatically detecting and tracking inconsistencies in software design models.
Software Engineering, IEEE Transactions on, 37(2):188–204, March 2011.
[LPE07] Tihamer Levendovszky, Ulrike Prange, and Hartmut Ehrig. Termination criteria for dpo transfor-
mations with injective matches. Electr. Notes Theor. Comput. Sci., 175(4):87–100, 2007.
[LWM+ 12] Yngve Lamo, Xiaoliang Wang, Florian Mantz, Wendy MacCaull, and Adrian Rutle. Dpf workbench:
A diagrammatic multi-layer domain specific (meta-)modelling environment. In Roger Lee, editor,
Computer and Information Science 2012, volume 429 of Studies in Computational Intelligence, pages
37–52. Springer, 2012.
[MVDS07] Tom Mens and Ragnhild Van Der Straeten. Incremental resolution of model inconsistencies. In
Recent Trends in Algebraic Development Techniques, volume 4409 of LNCS, pages 111–126. Springer,
2007.
[RMWL12] Adrian Rutle, Wendy MacCaull, Hao Wang, and Yngve Lamo. A metamodelling approach to
behavioural modelling. In Proceedings of the Fourth Workshop on Behaviour Modelling - Foundations and
Applications, BM-FA ’12, pages 5:1–5:10, NY, USA, 2012. ACM.
[Rut10] Adrian Rutle. Diagram Predicate Framework: A Formal Approach to MDE. PhD thesis, Department of
Informatics, University of Bergen, Norway, 2010.
[SBP07] Sagar Sen, Benoit Baudry, and Doina Precup. Partial model completion in model driven engineering
using constraint logic programming. In INAP’07, Germany, 2007.
[Sch06] Douglas C. Schmidt. Guest editor’s introduction: Model-driven engineering. 39(2):25–31, February
2006.
[SFC12] Rick Salay, Michalis Famelis, and Marsha Chechik. Language independent refinement using partial
modeling. In Fundamental Approaches to Software Engineering, volume 7212 of LNCS, pages 224–239.
Springer, 2012.
[SLK11] Christoph Schulz, Michael Löwe, and Harald König. A categorical framework for the transformation
of object-oriented systems: Models and data. J. Symb. Comput., 46(3):316–337, March 2011.
[TMAL13] Gabriele Taentzer, Florian Mantz, Thorsten Arendt, and Yngve Lamo. Customizable model migra-
tion schemes for meta-model evolutions with multiplicity changes. In 16th International Conference,
MODELS 2013, Miami, Proceedings, volume 8107 of LNCS, pages 254–270. Springer, 2013.