=Paper=
{{Paper
|id=Vol-1514/paper2
|storemode=property
|title=Towards Safe Model Transformation for Constraint-driven Modeling
|pdfUrl=https://ceur-ws.org/Vol-1514/paper2.pdf
|volume=Vol-1514
|dblpUrl=https://dblp.org/rec/conf/models/DemuthRLE15
}}
==Towards Safe Model Transformation for Constraint-driven Modeling==
https://ceur-ws.org/Vol-1514/paper2.pdf
Towards Safe Model Transformation for
Constraint-driven Modeling
Andreas Demuth, Markus Riedl-Ehrenleitner, Roberto E. Lopez-Herrejon, and Alexander Egyed
Johannes Kepler University (JKU)
Linz, Austria
Email: {firstname.lastname}@jku.at
Abstract—Model transformation is a key technology in model- designer would like to provide to the transformation user
driven engineering. Unfortunately, transformations are typically (software engineer) – that the transformation result will always
written manually and thus they are likely to contain errors and be correct with respect to the defined criteria, regardless of the
to produce incorrect or undesired output. Safe transformation
is the guarantee that for every possible source model, the trans- given input model.
formed target model is valid with respect to user-definable well- This work demonstrates safe transformation on Constraint-
formedness criteria. This paper introduces safe transformation driven Modeling (CDM) [4]. CDM avoids premature design
for constraint-driven modeling (CDM), an approach that em- decisions by constraining target models instead of generating
ploys model transformation to generate target model constraints them directly. CDM uses model transformations to automate
instead of generating a target model directly. Safe transformation
for CDM ensures that transformations only produce correct and the generation of model constraints and to perform required
non-contradictory constraints. We demonstrate the feasibility of updates. Hence, designers only have to write and maintain
safe transformation and present a formal framework for applying transformation rules instead of managing specific model con-
it to CDM in arbitrary domains. straints. However, transformation rules in CDM—and most
other MDE-approaches—are written manually. This means
I. I NTRODUCTION that there is always a chance that these rules contain errors.
With the increasing popularity of Model-Driven Engineer- CDM thus benefits from safe transformation as much as
ing (MDE) and modeling languages such as the Unified any other transformation-based approach would. Since CDM
Modeling Language (UML), there is also an increasing need transforms source models into constraints, an incorrect trans-
for validating the correctness of design models as they are used formation may result in contradictory constraints which make
for safety-critical systems or other systems that are subject to the problem of finding a valid model unsatisfiable. As an
strong regulations [1]. This verification consists of checking example, imagine two constraints forcing a model element to
whether a model is syntactically and semantically correct. The have two different values at the same time. Safe transformation
desired conditions are usually expressed in form of model for CDM ensures that defined transformation rules for a given
constraints, using constraint languages such as the Object source metamodel will never lead to contradictory constraints.
Constraint Language (OCL).To date, there exist efficient ap- This is a satisfiability test for which we apply the formal
proaches for checking constraints (e.g., [2]) on design models. modeling and reasoning engine FORMULA [5]. Safe transfor-
However, these approaches are not readily applicable to model mation generally ensures that all possible target models meet
transformations [3] where both the source model and the structural and static semantical conformance criteria [6]. For
target model must adhere to defined syntactic and semantic CDM, for instance, it ensures that no unsatisfiable constraints
constraints. Of course, it is possible to verify a target model can be generated.
once it has been generated. However, what if we want to ensure In this paper we present a formal approach for safe model
that all generated target models are correct? The dilemma is transformation. The approach is generic and validates the cor-
that there are likely infinite possible source models and thus it rectness of arbitrary transformations on arbitrary metamodels
is unscalable to generate all possible target models and verify and models by using a formal reasoning engine for automatic
them. solution space exploration and transformation effect analysis.
Safe model transformation ensures that transformations al- The approach uses only validity conditions and transforma-
ways produce results that meet defined criteria. These cri- tion definitions to automatically find input models suitable
teria are typically defined by designers based on either a for validating transformation correctness. The feasibility and
specific metamodel or domain knowledge. For example, an applicability are demonstrated in the context of constraint-
important criterion may be that every transformation result is driven modeling using the FORMULA [7] reasoning engine.
syntactically and semantically correct with respect to the target For enabling reasoning about constraints as the result of model
metamodel – i.e., the transformation will not generate an ill- transformations, we used a formal (meta)modeling framework
formed target model. This implies that the applied criteria are and formalized a basic consistency checking technique. In
likely to differ for different metamodels and domains. Safe addition to a theoretical foundation, we validated the correct-
model transformation is thus a warranty the transformation ness of the implementation through systematic testing and by
decision through a model transformation can be dangerous
as it might produce undesired models. In the next section
we will discuss how the constraint-driven modeling approach
addresses this issue and also illustrate why safe transformation
is important when transformations are used.
III. C ONSTRAINT- DRIVEN M ODELING
As the illustration shows, using model transformation in
(a) situations where more than one valid solution may exist is
not straightforward and deciding which solution is correct
involves domain knowledge that often cannot be generalized.
Using constraints avoids ambiguous transformations that may
produce invalid results. However, managing them manually
is non-practical in large models. The CDM approach tackles
this problem and uses transformations that generate constraints
on a model automatically instead of directly generating or
changing model elements. When using a traditional transfor-
mation, the target model is generated or adapted automatically
(b) (c) through the transformation execution on the source model. In
contrast, the constraint-driven modeling approach executes the
Fig. 1. Metamodel (a) and model (sequence (b) and class diagram (c)).
transformation Tc on the source model SM to generate the
constraints C, as shown in Eq. (1). Compared to traditional
applying it to typical UML-like models. transformations, the source model SM remains unchanged.
The core idea is that defining invariants and desired conditions
II. RUNNING E XAMPLE of valid models through constraints requires less knowledge
As a running example, we use an excerpt of a meta- and is therefore easier than defining a fixed set of rules that
model not unlike the UML metamodel as depicted in Fig. always produce a specific result that is always correct, (e.g.,
1(a). The metamodel consists of the following elements: it is easier to define that two model elements must not have
InstanceSpecification, Message, Class, Method, the same name than defining a rule that assigns meaningful
and ADClass. The element Class is used for modeling names to all elements automatically). Moreover, constraints
types. Such classes must provide a description, may have for similar elements (e.g., different instances of the same
an arbitrary number of Method assigned, and may be part of metamodel element) typically require similar constraints in
a hierarchy if they have supertypes assigned (super). The which only specific parts differ, hence transformation rules can
element ADClass is a specialization of Class and provides be seen as a structural template for a specific kind of constraint
an additional description, hence the prefix ”AD” and an that can be instantiated and filled with data for specific model
array of size 2 for the field description. The element elements. Note that the target model TMc (the subscript c
InstanceSpecification is used for modeling specific indicates that it is constrained) is not manipulated directly in
instances of modeled classes and Message elements are used our approach, neither through a transformation nor through
for modeling method calls between instance specifications. constraints.
We use this metamodel to build the models shown in Fig. cT
1(b) and Fig. 1(c). In Fig. 1(b) a sequence diagram is shown SM −→ C TMc (1)
that defines instance specifications a and b of the types A and Let us now illustrate how the approach can be applied to
B, respectively. Fig. 1(c) shows a class diagram in which the our running example. As we have shown, there is more than
types A, B, and S are defined. A is a Class, B and S are one possibility for changing the class diagram in Fig. 1(c)
instance of ADClass. S is also defined as superclass of B. to accommodate the change in the input models and thus
The message named m, sent from a to b and highlighted by the defining a single transformation that always generates the right
rounded frame in Fig. 1(b), is added to the model. According solution is not possible. However, we can use the knowledge
to UML semantics, this means that the class B must provide a provided in the model to define some requirements that must
method named m. At first sight, a simple model transformation be fulfilled1 :
that automatically adds a method with the appropriate name
• B must provide a method m (based on the message from
to the defining type of the message receiver would solve the
a to b).
problem. Note, however, that adding a method to any of B’s
• A must provide a description (based on its type
superclasses and interfaces (e.g., S) would also be a valid
Class).
option. Clearly, deciding where to add the required method –
if a new method is required at all – is non-trivial and requires 1 We omit other invariants (e.g., that instances of Class and ADClass
knowledge of the modeled system. Thus automating such a must provide a name) for space reasons.
1 r u l e RuleM only produce the discussed constraints C1–C4, but – because
from s : Message
3 to t : Constraint (
instances of ADClass are also instances of Class – they
e l e m e n t <− s.receiver.type will also create the following constraints C5–C6:
5 i n v <− ” s e l f . p r o v i d e d M e t h o d s−>
e x i s t s (m|m. name = ’ ” + s.name + ” ’ ) ” )
C5 element B: self.description->size()=1
7 r u l e RuleC C6 element S: self.description->size()=1
from s : C l a s s Obviously, the constraint combinations C3 ∧ C5 and C4 ∧ C6
9 to t : Constraint (
e l e m e n t <− s are overconstraining the elements B and S, respectively. Both
11 i n v <− ” s e l f . d e s c r i p t i o n −>s i z e ( ) =1 ” ) elements B and S are forced to have two different numbers of
r u l e RuleADC
13 from s : ADClass descriptions at the same time. Hence, the transformation leads
to t : Constraint ( to contradictory constraints.
15 e l e m e n t <− s
i n v <− ” s e l f . d e s c r i p t i o n −>s i z e ( ) =2 ” ) The reason for this, somehow unexpected, result is that the
Listing 1. ATL-like transformation rules to generate constraints. transformation rules for cardinality checking constraints are
defined for instances of the types Class and ADClass (lines
7 and 12 in Listing 1). Because ADClass is a subclass of
Class, as defined in the metamodel depicted in Fig. 1(a),
•S and B must provide two description fields (based RuleC is also executed for all instances of ADClass. Indeed,
on their type ADClass). the transformation rules RuleC and RuleADC need addi-
These requirements can be easily stated as constraints, for tional guarding statements that ensure the execution of only
example written in OCL. To generate them automatically, we one of the rules per element. In fact, automating constraint
use ATL [8] to define the three transformation rules shown generation may even increase the risk of contradictions be-
in Listing 1. The first rule RuleM (lines 1–6) is defined for tween constraints and overconstraining of models as designers
messages in the model and creates constraints that require the specify transformation rules that are executed when certain
receiver element’s defining class to provide a corresponding requirements are fulfilled. This means that – in contrast to
method. Note that this does not require the class to directly manual addition of constraints to individual model elements –
provide the method; it is sufficient that the method is defined the aggregation of constraints restricting a model element is no
somewhere in the class hierarchy (e.g., in a superclass). longer directly visible for a designer. Note that this situation is
Rule RuleC (lines 7–11) is executed for Class instances not unique to constraint transformations. Such issues may arise
and generates constraints that check the cardinality of the in other domains as well. Using transformations to generate
attribute description. Finally, the third rule RuleADC target models implies that the generated model is not known
(lines 12–16) checks that instances of ADClass provide two before rule execution. Automating model generation typically
descriptions. Note that for simplicity we treat the two diagrams involves large numbers of transformation rules that are writ-
shown in Fig. 1(b) and Fig. 1(c) as one model (SM). When ten for complex metamodels. Visualization of dependencies
executing the transformation rules on the model in Fig. 1 we between these rules is usually not available and thus the risk
expect the following constraints to be generated: of overlooking possible side-effects increases with the number
C1 element B: self.providedMethods->exists(m| of rules. Checking the correctness of transformation rules by
m.name=’m’)
C2 element A: self.description->size()=1
looking at the results for existing sample models is not a valid
C3 element B: self.description->size()=2 solution to this problem as source models may change and
C4 element S: self.description->size()=2 thus cause errors in target models. This can also occur later
We expect one constraint to be generated for the message during model refactoring, updates, or extensions when target
m and three constraints to be generated for checking the models have to be re-generated. Next, we present how safe
description attributes of Class and ADClass instances. The transformation helps designers avoid errors in target models.
constraint C1 will show the inconsistency in our running
example that b provides no method m. IV. S AFE M ODEL T RANSFORMATION
Although the constraints in such a small example could be As we have shown in the previous section, writing trans-
written manually, maintaining a large number of constraints formation rules – regardless of the specific domain – can be a
during the modeling process where the metamodels and mod- highly complex task as there may be source models that cause
els change frequently is error prone. Consequently, constraints the execution of combinations of rules that are not supposed
should be managed automatically. We have shown that CDM to be executed together or also the execution of rules for
is practical in [4]. elements where the rule should not be executed at all. Safe
However, even with automated constraint management, model transformation guarantees that a transformation
designers manually write transformation rules or templates will always produce valid results. Validity rules are defined
for desired constraints that can be executed or instantiated, by designers and typically stem from both the metamodel of
respectively. Thus there is no guarantee that these transforma- the transformation’s target model (syntax rules) and domain
tion rules or templates produce constraints that are syntacti- knowledge (semantic rules). Intuitively, safe transformation
cally and semantically correct. Coming back to our running can be easily proven for a single source model by executing
example, the transformation rules in Listing 1 actually not the transformation and validating whether the target model
is valid with a SAT-solver. However, our definition of safe V. A PPLYING S AFE M ODEL T RANSFORMATION TO
transformation is that a transformation must not, under any cir- C ONSTRAINT- DRIVEN M ODELING
cumstances, produce invalid results, meaning that there must As discussed in Section III, constraints can be contradicting.
not be any possible source model that causes invalid results. Because we need to formally specify such a contradiction in
Based on the conventional notation for model transformation, order to apply safe transformation, let us first give formal
we can formally define a transformation as the function shown definitions of constraints and the models they are applied to.
in Eq. (2). A transformation is a function that uses a source
model sm ≺ SMM and a set of transformation rules T as A. Formalizing Model Constraints and Consistency Checking
input and returns a target model tm ≺ TMM2 . The signatures Constraints restrict model elements, therefore we need a
of the validity functions for both input and target model are formal definition of metamodels and models along with con-
shown in Eq. 3 and Eq. 4, respectively. We can then define a straints definitions. Eq. (7) defines a metamodel MMcdm that
transformation to be safe if the condition in Eq. (5) holds for consists of a set of types T ypes and the set of expressions
T . Proving that this condition holds requires the execution available for individual constraints, called CExpr. An in-
of the transformation rules specified in T for all possible stance of the metamodel is then a model M ≺ M Mcdm ,
instances sm ≺ SMM, which is indeed not a feasible option as defined in Eq. (8), consisting of model elements N ,
because common metamodels often allow an infinite number connections E that link model elements, and constraints C.
of different instantiations.
MMcdm := hT ypes, CExpri (7)
M ≺ M Mcdm := hN, E, Ci|
trans : (sm ≺ SMM, T ) → tm ≺ TMM (2)
N = {x|x ≺ y ∈ T ypes}∧
validS : sm ≺ SMM → {true, f alse} (3)
E = {ha, b, ci|a ∈ N ∧ b ∈ N ∧ c ⊆ N }∧
validT : tm ≺ TMM → {true, f alse} (4)
C = {hcontext, expi|context ∈ N ∧ exp ≺ CExpr)}
Saf e(SMM, T ) ⇔ ∀sm ≺ SMM : validS (sm) (8)
(5)
⇒ validT (trans(sm, T )) value : (N, N ) → P(N ), (x, y) 7→ z : ∃hx, y, zi ∈ E (9)
U nsaf e(SMM, T ) ⇔ ∃sm ≺ SMM : validS (sm)∧ (
(6) inconsistent if c is violated
¬validT (trans(sm, T )) validate(c ∈ C) 7→ (10)
consistent otherwise
However, we take Eq. (5) as the condition that must hold for allowed(ha, b, ci ≺ M Mcdm ) 7→ {hn, e, v, ri|
a transformation to be safe and use it to define the condition n ∈ a ∧ e ∈ a ∧ v ⊆ a ∧ r ⊆ c∧
that holds for any unsafe transformation, as shown in Eq. (6).
Proving that a transformation is unsafe thus requires only a (∃hh, i, ji ∈ E : n = h ∧ e = i)∧ (11)
single instance sm ≺ SMM to lead to a result tm ≺ TMM (y = value(n, e) ∧ y ∈
/ v ⇒ ∃rx ∈ r :
that is not valid. validate(rx ) = inconsistent)}
The FORMULA reasoning engine supports automatic
contradiction(m ≺ M Mcdm ) ⇔
proofs through solution space exploration and transformations, (12)
thus it is an ideal choice for implementing safe transformation. ∃hn, e, v, xi ∈ allowed(m) :v = ∅
However, any reasoning engine for automatic proofs can be Note that a connection between model elements in Eq. 8
used in principle, even though this could require the additional consists of three parts: i) the source model element (a), ii)
formalization of transformations. The solver is capable of a connection identifier (b) which is also a model element, and
expanding models on its own for finding proofs and partial iii) the source of the connection (c). Such a connection can
models can be used for reasoning. For details about the be interpreted as a value c being assigned to the property b
reasoning mechanism please refer to [7] and [5]. of element a. Thus, we can define a helper function value to
Note also that safe transformation does not rely on static retrieve the value assigned to a given model element property,
analysis and thus allows arbitrary input/output (meta)models, as shown in Eq. 9.
transformation languages, and conditions. The approach there- We define the generic constraint validation function as
fore is generic and not limited to specific domains or lan- shown in Eq. (10). We omit a detailed discussion of con-
guages. Moreover, the complete integration of input model straint validation because of space restrictions and the fact
construction, the transformation, and the validity conditions that validation functions heavily depend on the used consis-
means that both the validity conditions and the transformation tency checking technique. Additionally, we define the function
itself are available to the solver for reasoning, potentionally allowed that returns the set of allowed values for model
enabling higher efficiency and precision. element properties, as shown in Eq. (11). This set includes
tuples of a model element (n), a property of n (e), a set
of values (v) that may be assigned to the model element’s
2 We use the notation a ≺ b to indicate that a is an instance of b. property without causing a constraint to become inconsistent,
and a set of constraints (r) that restricted the allowed values. model will fail and the solver will tell us that it could not find
The function contradiction takes a model as input and checks such an example, meaning that the transformation is safe.
it for contradictions, as shown in Eq. (12). A contradiction
occurs if there is at least one element for which no value can VI. VALIDATION
be assigned without causing an inconsistency. We omit more In addition to the presented theories, we demonstrate the
detailed definitions as they would strongly depend on the used applicability of the generic safe transformation approach by
modeling and constraint languages. implementing it for constraint-driven modeling. We also dis-
Now that the metamodel and the corresponding functions cuss threats to validity in this section.
for constraint validation and the detection of contradictions
are defined, we can use this information to check the trans- A. Correctness
formations from Section III. In the paper we presented the theoretical foundations of safe
model transformation. The presented conditions are correct
B. Ensuring Safe Constraint Transformation and they capture the ideas and principles of safe transforma-
We converted the ATL-like transformations shown in Listing tion. The correctness was further assessed by implementing
1 to transformations Tcdm that can be executed by the FOR- those conditions and functions in a program that produced
MULA solver. A constraint transformation CT can be written correct results as we discuss next.
as shown in Eq. (13). When executing the transformation for
a source model sm ≺ MMcdm , the result is the constrained B. Implementation
model tmc ≺ MMcdm which includes all model elements To ensure the feasibility of safe transformation and the
defined in sm and a set of constraints generated for these validity of the theoretical foundations presented in the paper,
element. The last part needed for safe transformation are the we have implemented a safe transformation framework for
source and target validity functions validScdm and validT cdm , CDM using the FORMULA language. This implementation
respectively. For the former, the conditions are domain-specific is a straight forward translation of the presented formal
and thus independent of CDM. Therefore, we omit a formal definitions to type declarations and functions, thus we omit
definition in Eq. 14. For the latter, results to be valid if they a detailed discussion. It allows the definition of metamodels
are free of contradicting constraints, as shown in Eq. (15). and models (based on an existing metamodeling framework
By substituting the constraint transformation function (13), the [5]), and it supports the definition of constraints. Moreover, it
metamodel definition (7), and the validity conditions (14) and provides functions for constraint evaluation and for reasoning
(15) in Eq. (6) we get the unsafe condition as shown in Eq. about constraints. For this feasibility study we used a subset
(16). of the constraint expressions available in OCL. The correct
Tcdm behavior of the implementation was ensured through testing
CT : sm ≺ MMcdm −− −→ tm ≺ MMcdm (13)
with systematically varied inputs for expressions.
validScdm (x ≺ MMcdm ) ⇔ x is syntactically correct As mentioned in Section V, we used the implementation
(14)
and valid w.r.t. domain semantics with the model discussed in Section II and the transformation
rules from Listing 1. For the running example and the incorrect
validT cdm (x ≺ MMcdm ) ⇔ ¬contradiction(x) (15) transformation rules, the FORMULA solver returned different
U nsaf e(MMcdm ) ⇔ ∃sm ≺ MMcmd : solutions (i.e., sample models) that all included an instance of
(16) ADClass and contained contradicting constraints. Moreover,
validScdm (sm) ∧ ¬validT cdm (CT (sm))
the resulting facts derived by FORMULA included as many
Note that we use the transformation function CT directly on constraint contradictions as there were ADClass instances.
the right-hand side of the equation and thus we eliminate After fixing the transformation rules, the problem was not
the corresponding argument on the left-hand side. We now satisfiable anymore – as expected. This indicates that the
ask the FORMULA solver to prove this condition and search translation to FORMULA is correct and the approach produces
for examples of source models sm that lead to invalid target the desired result in practice.
models: solve CT sm Unsafe. The solver will return an
input that leads to a contradiction, which tells us that the C. Applicability
transformation is unsafe. In particular, this input will include The presented framework is suitable for ensuring safe
an instance of ADClass and also include facts that help transformation for CDM in arbitrary modeling domains. To
designers find the constraints and the transformations that enable safe transformation in general (i.e., for transformations
caused the contradiction). different to those used in CDM), the following three steps
Assume that, after taking a closer look at the transformation are necessary: i) define source and target metamodels using
rules RuleC and RuleADC based on the solver output, an existing metamodeling framework, ii) describe transforma-
we identified the error and added guarding statements (e.g., tion rules in FORMULA, and iii) describe desired validity
s.getClass().getName()="Class") so that RuleC conditions. We believe that the metamodel definition can be
is no longer executed for instances of ADClass. Asking the automated for metamodels based on common frameworks
solver again for an example sm of a contradiction-causing (e.g., MOF). The transformation description in FORMULA
is straightforward and uses concepts similar to common trans- VIII. C ONCLUSIONS AND F UTURE W ORK
formation languages such as ATL – this step may also be In this paper we presented the safe transformation approach
automated. Overall, we deem the effort needed for using safe that allows the use of formal modeling languages for proving
transformation acceptable given the importance of transforma- assumptions about arbitrary model transformations for either
tion correctness and the effort required for locating and fixing arbitrary source models or also source models with specific
errors caused by unsafe transformations in later development characteristics. In particular, we demonstrated its applicability
stages. Overall, we believe that the steps required for using for the constraint-driven modeling approach by ensuring con-
the framework are manageable. straint satisfiability and checking the semantical correctness
of transformation rules and their results. The safe transfor-
D. Threats to Validity mation approach was validated by implementing it using the
We have used the FORMULA solver for finding input FORMULA language. For future work we plan to integrate the
models for which a transformation is unsafe with respect to framework in existing tools that use CDM and also implement
defined criteria. Indeed, FORMULA is capable of searching the approach for other domains.
solutions efficiently. Nevertheless, it can only guarantee that R EFERENCES
there is no solution for a defined maximum size of solution
[1] Anda, B., Hansen, K., Gullesen, I., Thorsen, H.K.: Experiences from
models [5]. In [9], Sen et al. use Alloy for constructing introducing uml-based development in a large safety-critical project.
test models that meet defined well-formedness criteria from Empirical Software Engineering 11(4) (2006) 555–581
partial models. We use this principle more extensively as our [2] Egyed, A.: Instant consistency checking for the UML. In: ICSE. (2006)
381–390
input data for constructing input models for transformations [3] Czarnecki, K., Helsen, S.: Classification of model transformation
is often empty. Although we expect target model errors to approaches. In: OOPSLA Workshop on Generative Techniques in the
typically involve only a relatively small number of elements, Context of Model-Driven Architecture. (2003)
[4] Demuth, A., Lopez-Herrejon, R.E., Egyed, A.: Constraint-driven mod-
the bounded search space is a practical threat to validity. Even eling through transformation. Software and Systems Modeling (2013)
if current solvers might not find input models that unveil DOI: 10.1007/s10270-013-0363-3.
errors in transformations, manually written test models are far [5] Jackson, E.K., Levendovszky, T., Balasubramanian, D.: Reasoning about
metamodeling with formal specifications and automatic proofs. In:
from finding all errors [9], thus our approach gives designers MoDELS. (2011) 653–667
additional confidence in the correctness of their work. [6] Amrani, M., Lucio, L., Selim, G.M.K., Combemale, B., Dingel, J.,
Vangheluwe, H., Traon, Y.L., Cordy, J.R.: A tridimensional approach
for studying the formal verification of model transformations. In: ICST.
VII. R ELATED W ORK (2012) 921–928
[7] Jackson, E.K., Sztipanovits, J.: Towards a formal foundation for domain
Model transformation has become a very active field of specific modeling languages. In: EMSOFT. (2006) 53–62
research. We now discuss other approaches closest to our topic. [8] OBEO, INRIA: ATLAS transformation language (ATL).
Sen et al. [9], [10] presented techniques for finding input http://www.eclipse.org/atl/ (2014)
[9] Sen, S., Mottu, J.M., Tisi, M., Cabot, J.: Using models of partial
models for testing model transformations. They use Alloy knowledge to test model transformations. In: ICMT. (2012) 24–39
to expand partial models automatically to complete models [10] Sen, S., Baudry, B., Mottu, J.M.: Automatic model generation strategies
that conform to well-formedness rules. The fact that they use for model transformation testing. In: ICMT. (2009) 148–164
[11] Guerra, E., de Lara, J., Wimmer, M., Kappel, G., Kusel, A., Retschitzeg-
different languages and strategies for finding sample models ger, W., Schönböck, J., Schwinger, W.: Automated verification of model
shows that our generic approach can be implemented with a transformations based on visual contracts. Autom. Softw. Eng. 20(1)
range of languages. Note, however, that safe transformation (2013) 5–46
[12] Cabot, J., Clarisó, R., Guerra, E., de Lara, J.: Verification and valida-
integrates the construction of test input models and the exe- tion of declarative model-to-model transformations through invariants.
cution of transformations. Guerra et al. [11] propose the use Journal of Systems and Software 83(2) (2010) 283–302
of contract for validating transformation correctness. This is
basically the same concept safe transformation uses. However,
they use QVT to enforce defined pre- and post-conditions of
transformations and rely on existing input models while safe
transformation uses such contracts to actively search for input
models that lead to a violation of the target model constraints.
Cabot et al. [12] proposed an approach for deriving OCL con-
straints from declarative transformation specifications. Their
approach generates invariants that must hold between source
and target models. Our approach can be used to ensure that,
for example, only non-contradicting invariants are generated.
Jackson et al. [5] previously used FORMULA for describing
a general purpose (meta)modeling framework.The reasoning
they did about transformations based on their framework can
be seen as an application of the safe transformation approach
to identify undesired behavior of transformations.