Download A query structured approach for model transformation PDF

TitleA query structured approach for model transformation
LanguageEnglish
File Size4.6 MB
Total Pages90
Table of Contents
                            Article 1
                        
Document Text Contents
Page 1

ACM/IEEE 17th International Conference on

Model Driven Engineering Languages and Systems

September 28 – October 3, 2014  Valencia (Spain)

















AMT 2014 – Analysis of Model Transformations

Workshop Proceedings

Juergen Dingel, Juan de Lara, Levi Lúcio, Hans Vangheluwe (Eds.)







Published on Oct 2014 v1.0

Page 2

© 2014

Re-publication of material from this volume requires permission by the copyright owners.





Juergen Dingel

Queens University, Canada

Juan de Lara

Universidad Autónoma de Madrid, Spain

Levi Lúcio

McGill University, Canada

Hans Vangheluwe

University of Antwerp, Belgium and McGill University, Canada

Page 45


( )

Fig. 3: Example Test Objective

and the target of the assignment are references to variables. This pattern matches
the objects created by ATL rule UDel, and thus requires resolve operations.

5 ATL to Algebraic Graph Transformation

This section introduces our main contribution, the translation of ATL transfor-
mations to artifacts of an algebraic graph transformation: a type graph, graph
transformation rules and a high-level program. Given the rewriting semantics of
AGT and the exogeneous nature of the transformations we consider, we choose
to model the ATL transformation as a rewriting of the input graph that adds the
output elements. Consequently, the type graph includes types corresponding to
both the input and the output metamodels. As explained in Section 3.2, the cor-
respondence of metamodel elements to graph type elements is straightforward
[3], and the resulting type graph is depicted in Figure 4. In addition, tracing
node types are added to support the ATL resolve mechanism. First, an abstract
Trace node relates source objects (SMElement) to target objects (CMElement)
of ATL rules. Second, for each ATL rule, a concrete trace node (named <atlrule-
name>_Trace) references the actual source and target types of this rule. These
trace nodes will be used by the graph transformation rules, as explained next.

Fig. 4: Resulting Type Graph in AGG

Much like the execution semantics of ATL, the graph transformation starts
with a set of instantiation rules that create output nodes without linking them.
For example, O2Var_Inst in Figure 5a matches an Outport and creates a Vari-
able and a concrete trace O2Var_Trace relating the source and target nodes
(numbers indicate mapping by the rule morphism). Then, a second set of resolv-
ing rules rely on the trace nodes produced in the first phase to link output nodes.
For example, S2VExp_Res in Figure 5b matches an Outport and a Trace node

40

Page 46

to find the resulting Variable and create the variable edge. Thus the elements
created in the RHS of Figure 5a (O2Var_Trace and Variable) are matched later
by the LHS in Figure 5b (Trace and Variable). Note the use of abstract Trace
nodes in the resolving rules to allow resolving with any rule as long as the number
and types of source and target elements match, as per the ATL semantics.

Finally, a high-level program implements the two phases by iterating instan-
tiation rules first and resolving rules second, yielding the following for CMG:
P = O2V ar_Inst↓; S2V Exp_Inst↓; UDel_Inst↓; S2V Exp_Res↓;
UDel_Res↓

(a) O2Var_Inst

(b) S2VExp_Res

Fig. 5: GTS rules translated from ATL rules

Having translated the ATL transformation to the AGT semantics, we next
explain how we use precondition construction to back-propagate test objectives.

6 Transformation of Postcondition to Precondition

In [9], Habel, Pennemann and Rensink formally define a construction of weakest
precondition for high-level programs in the interest of proving transformation
correctness. Given a program and a postcondition, the weakest precondition is
a constraint that characterizes all possible input graphs that lead to the termi-
nation of the program with a final graph satisfying the postcondition. A precon-
dition construction is defined for one rule application and applied inductively
to the sequence of rules defined by the program. In the case of P ↓ programs
each number of iterations of P from 0 to ∞ must be considered, making the
construction theoretically infinite.

However, in contrast with proof of correctness, we actually do not need to
compute the weakest precondition. Since the final goal is to find a test model
satisfying the test objective, computing one sufficient precondition would be
enough. To do so, we limit iterations of rules in the program to a bounded num-
ber, making the precondition construction finite (the choice of bounds remains

41

Page 89

1 %%%% Analysis Model
2 %%%% sets of non-deterministic relations (UML to RDBMS direction):
3 []
4 %%%% sets of non-deterministic relations (RDBMS to UML direction):
5 [(1,class2table), (3,superAttribute2column), (5,superAttribute2column)]
6 [(..), (...)]

Listing 1.4: A fragment of the output of the analysis

The final goal of such analysis is to convey to the transformation implementor enough
information to perform a refinement which resolves the non-determinism. In this re-
spect, the ”guilty” rules are opportunely marked in such a way the sets of rules respon-
sible of the non-determinism sources can be easily recognized by the designer.

6 Related work

Non-determinism is a recurrent aspect affecting model transformation design and im-
plementation. As said, most of the current languages (e.g.,[11, 17, 3, 19, 16, 14, 15] are
able to generate only one model at time; in this way even if the transformation is non-
bijective the solution is normally identified according to details which are often un-
known to the designer rendering such approached unpredictable and therefore unprac-
tical. Existing declarative approaches [6, 12] cope with the non-bijectivity by gener-
ating sets of models at once, i.e., all the admissible solutions of a transformation are
generated as a solution set. Among them, JTL [6] is specifically tailored to support
bidirectionality and change propagation. In [12], the authors propose to use Alloy and
follows the predictable principle of least change [13], by using a function that calcu-
lates the distance between instances reducing the generated models. Non-determinism
is also considered in BiFlux [17], which adopts a novel ”bidirectional programming by
update” paradigm, where a program succinctly and precisely describes how to update
a source document with a target document, such that there is a unique inverse source
query for each update program. Within the Triple Graph Grammars, PROGRES [2]
considers non-deterministic cases by demanding user intervention to rule execution in
order to choose the desired behavior.

Existing approaches and tools involve testing (e.g., test case generation for model
transformations), or analysis performed only on executing programs (e.g., run-time
monitoring) [1]. In contrast, in [1] the author propose an approach to analyze model
transformation specification represented in Alloy. The simulation produces a set of ran-
dom instances that conform to the well-formedness rules and eventually that satisfy
certain properties. Furthermore, existing functional approaches perform model trans-
formation analysis [11, 17], in order to evaluate the transformation validity (generally,
in terms of correctness) before its execution.

7 Conclusion and Future Work
In this paper, we have proposed an approach to detect non-determinism in bidirectional
transformations at static-time, i.e., without executing the transformation. The intention
is to provide transformation implementors with a tool capable of analyzing transforma-
tions in order to return feedback which could resolve potential non-determinism. The
approach has been demonstrated on a small yet significant case study implemented in
JTL. Despite the analysis is completely independent from JTL, in order to make the

84

Page 90

approach completely language-independent additional implementation efforts are re-
quired which we intend to do in the near future. Furthermore, the logical foundation
of the engine makes possible the verification of different formal properties by translat-
ing them in ASP, with the scope to provide a mean for improving the quality of model
transformation specifications.

References

1. K. Anastasakis, B. Bordbar, and J. M. Küster. Analysis of model transformations via Alloy.
In ModeVVa’07, pages 47–56, 2007.

2. S. M. Becker, S. Herold, S. Lohmann, and B. Westfechtel. A graph-based algorithm for con-
sistency maintenance in incremental and interactive integration tools. Software and System
Modeling, 6(3):287–315, 2007.

3. A. Bohannon, J. N. Foster, B. C. Pierce, A. Pilkiewicz, and A. Schmitt. Boomerang: Re-
sourceful lenses for string data. In POPL 2008, pages 407–419, 2008.

4. G. Callow and R. Kalawsky. A Satisficing Bi-Directional Model Transformation Engine
using Mixed Integer Linear Programming. JOT, 12(1):1: 1–43, 2013.

5. K. Chen, J. Sztipanovits, S. Abdelwalhed, and E. Jackson. Semantic Anchoring with Model
Transformations. In ECMDA-FA, 2005.

6. A. Cicchetti, D. Di Ruscio, R. Eramo, and A. Pierantonio. JTL: a bidirectional and change
propagating transformation language. In SLE10, pages 183–202, 2010.

7. K. Czarnecki, J. N. Foster, Z. Hu, R. Lämmel, A. Schürr, and J. F. Terwilliger. Bidirectional
Transformations: A Cross-Discipline Perspective - GRACE meeting. In Procs. of ICMT2009.

8. R. Eramo, A. Pierantonio, and G. Rosa. Uncertainty in bidirectional transformations. In
Procs. of MiSE 2014, 2014.

9. M. Gelfond and V. Lifschitz. The Stable Model Semantics for Logic Programming. In Procs
of ICLP, pages 1070–1080, Cambridge, Massachusetts, 1988. The MIT Press.

10. T. Hettel, M. Lawley, and K. Raymond. Model Synchronisation: Definitions for Round-Trip
Engineering. In Procs. of ICMT 2008, 2008.

11. S. Hidaka, Z. Hu, K. Inaba, H. Kato, and K. Nakano. Groundtram: An integrated framework
for developing well-behaved bidirectional model transformations. In ASE 2011, 2011.

12. N. Macedo and A. Cunha. Implementing QVT-R Bidirectional Model Transformations Us-
ing Alloy. In FASE, pages 297–311, 2013.

13. N. Macedo, H. Pacheco, A. Cunha, and J. N. Oliveira. Composing least-change lenses.
ECEASST, 57, 2013.

14. MediniQVT. http://projects.ikv.de/qvt/.
15. ModelMorf. http://www.tcs-trddc.com/modelmorf/.
16. Object Management Group (OMG). MOF 2.0 QVT Final Adopted Specification v1.1, 2011.

OMG Adopted Specification formal/2011-01-01.
17. H. Pacheco and Z. Hu. Biflux: A bidirectional functional update language for XML. In BIRS

workshop: Bi-directional transformations (BX), 2013.
18. D. Schmidt. Guest Editor’s Introduction: Model-Driven Engineering. Computer, 39(2):25–

31, 2006.
19. A. Schürr. Specification of Graph Translators with Triple Graph Grammars. In in Proc. of

WG94. Springer, 1995.
20. S. Sendall and W. Kozaczynski. Model Transformation: The Heart and Soul of Model-Driven

Software Development. IEEE Software, 20(5):42–45, 2003.
21. P. Stevens. Bidirectional model transformations in QVT: semantic issues and open questions.

SOSYM, 8, 2009.

85

Similer Documents