An ocl - Based framework for model transformations

2.2. Animation of Transformation
After each transformation step, we can see
the combination of the source, correspondence,
and target part as a whole model. We could
employ OCL expressions in order to explore
such a model. Mappings within the current rule
application can be highlighted by OCL queries.
This makes it easier for the modeler to check if
the rule application is correct.
6. The RTL Language and Tool Support
Our approach for verification and validation
of transformation is realized with the support of
USE [11], which is a tool for analysis, reasoning,
verification and validation of UML/OCL
specifications. We define the RTL2 language
in order to specify triple rules incorporating
OCL. The declarative specification in textual
form can generate the different operations for
transformation scenarios as illustrated in Fig. 14.
With the full OCL support, USE allows us
to realize transformations and to ensure their
correctness as discussed in Sect. 5: We could
2RTL stands for Restricted Graph Transformation Language
D.H. Dang, M. Gogolla / VNU Journal of Science: Comp. Science & Com. Eng., Vol. 32, No. 1 (2016) 42–57 55
check class invariants, pre- and postconditions
of operations, and properties of models, which
are expressed in OCL. In USE system states are
represented as object diagrams. System evolution
can be carried out using operations based on
basic state manipulations, such as (1) creating
and destroying objects or links and (2) modifying
attributes. In this way a transformation
framework based on the integration of TGGs
and OCL are completely covered by USE.
Figure 15 shows metamodels for the SC2EHA
transformation in USE.
c
o
n
t
e
x
t
R
u
l
e
C
o
l
l
e
c
t
i
o
n
:
:
s
i
m
p
S
t
a
t
e
T
o
p
_
c
o
E
v
o
l
(
m
a
t
c
h
S
L
:
T
u
p
l
e
(
s
c
:
S
t
a
t
e
c
h
a
r
t
,
_
s
_
n
a
m
e
:
S
t
r
i
n
g
)
,
m
a
t
c
h
T
L
:
T
u
p
l
e
(
e
h
a
:
E
H
A
,
a
u
t
:
A
u
t
H
)
,
m
a
t
c
h
C
L
:
T
u
p
l
e
(
s
2
e
:
S
C
2
E
H
A
)
)
p
r
e
s
i
m
p
S
t
a
t
e
T
o
p
_
c
o
E
v
o
l
_
p
r
e
:
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
m
a
t
c
h
S
L
:
T
u
p
l
e
(
s
c
:
S
t
a
t
e
c
h
a
r
t
,
_
s
_
n
a
m
e
:
S
t
r
i
n
g
)
l
e
t
s
c
:
S
t
a
t
e
c
h
a
r
t
=
m
a
t
c
h
S
L
.
s
c
i
n
l
e
t
_
s
_
n
a
m
e
:
S
t
r
i
n
g
=
m
a
t
c
h
S
L
.
_
s
_
n
a
m
e
i
n
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
m
a
t
c
h
T
L
:
T
u
p
l
e
(
e
h
a
:
E
H
A
,
a
u
t
:
A
u
t
H
)
l
e
t
e
h
a
:
E
H
A
=
m
a
t
c
h
T
L
.
e
h
a
i
n
l
e
t
a
u
t
:
A
u
t
H
=
m
a
t
c
h
T
L
.
a
u
t
i
n
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
m
a
t
c
h
C
L
:
T
u
p
l
e
(
s
2
e
:
S
C
2
E
H
A
)
l
e
t
s
2
e
:
S
C
2
E
H
A
=
m
a
t
c
h
C
L
.
s
2
e
i
n
-
-
S
_
p
r
e
c
o
n
d
i
t
i
o
n
-
-
T
_
p
r
e
c
o
n
d
i
t
i
o
n
e
h
a
.
a
u
t
H
-
>
i
n
c
l
u
d
e
s
A
l
l
(
S
e
t
{
a
u
t
}
)
a
n
d
a
u
t
.
r
e
f
i
n
e
d
=
e
h
a
.
t
o
p
a
n
d
-
-
C
_
p
r
e
c
o
n
d
i
t
i
o
n
S
e
t
{
s
2
e
.
s
c
}
-
>
i
n
c
l
u
d
e
s
A
l
l
(
S
e
t
{
s
c
}
)
a
n
d
S
e
t
{
s
2
e
.
e
h
a
}
-
>
i
n
c
l
u
d
e
s
A
l
l
(
S
e
t
{
e
h
a
}
)
p
o
s
t
s
i
m
p
S
t
a
t
e
N
e
s
t
_
c
o
E
v
o
l
_
p
o
s
t
:
ru
le
 s
im
p
S
ta
te
T
o
p
c
h
e
c
k
S
o
u
rc
e
(
s
c
:S
ta
te
c
h
a
rt
){ 
s
:S
im
p
S
ta
te
(s
c
,s
):
O
w
n
s
S
ta
te
[s
.n
a
m
e
<
>
o
c
lU
n
d
e
fi
n
e
d
(S
tr
in
g
)]
[s
.c
o
n
ta
in
e
r=
o
c
lU
n
d
e
fi
n
e
d
(C
o
m
p
S
ta
te
)]
}c
h
e
c
k
T
a
rg
e
t(
e
h
a
:E
H
A
a
u
t:
A
u
tH
(e
h
a
,a
u
t)
:O
w
n
s
A
u
tH
[a
u
t.
re
fi
n
e
d
=
e
h
a
.t
o
p
]
){ 
s
H
:S
ta
te
H
(a
u
t,
s
H
):
C
o
n
ta
in
s
S
ta
te
H
}c
h
e
c
k
C
o
rr
(
(s
c
,e
h
a
) 
a
s
 (
s
c
,e
h
a
) 
in
 s
2
e
:S
C
2
E
H
A
){ 
((
S
ta
te
)s
,s
H
) 
a
s
 (
s
c
,e
h
a
) 
in
 s
2
s
H
:S
2
S
H
S
2
S
H
:[
s
e
lf
.e
h
a
.n
a
m
e
=
s
e
lf
.s
c
.n
a
m
e
] 
}e
n
d (a
) 
ru
le
 s
p
e
c
if
ic
a
ti
o
n
 i
n
 R
T
L
(b
) 
th
e
 g
e
n
e
ra
te
d
 o
p
e
ra
ti
o
n
 f
o
r 
c
o
-e
v
o
lu
ti
o
n
Fig. 14: RTL specification and generated OCL operations.
7. Related Work
Triple Graph Grammars (TGGs) have been
proposed in [8]. Since then, many works have
extended TGGs for software engineering [17].
Here we focus on the incorporation of TGGs
and OCL as a foundation for transformations as
proposed in our previous work [18, 19, 20]. This
work is an extended version of our previous work
with a focus on a formal foundation and an OCL-
based framework for model transformations.
Many approaches have been proposed for
model transformation. Most of them are
in line with the standard QVT [5] such as
ATL [3] and Kermeta [4]. Like our work, they
allow the developer to precisely present models
using metamodels and OCL. The advantage
of our approach is that it is based on the
integration of TGGs and OCL, which allows the
developer to automatically analyze and verify
transformations, and supports for bidirectional
model transformation.
Our approach for model transformation is
based on graph transformation like the work in
VMTS [6] and Fujaba [17]. Many other works
focus on the translation of the transformation to a
formal domain for model checking such as Alloy
in [21], Promela in [22], and Maude in [23].
In the field of Model-Driven Engineering,
testing and analysis of model transformations
has been subject to investigations (see, for
example, [24, 25]). The work [26] proposes a
technique for developing test cases for UML
and OCL models. By guiding the construction
process through so-called classifying terms,
the built test cases in form of object models
are classified into equivalence classes. In [9]
the authors propose a method to derive OCL
invariants from TGG and QVT transformations
in order to enable their verification and
analysis. Our approach targets to support
for both declarative and operational features of
transformations. We also introduce a new method
to extract invariants for TGG transformations.
Several other works focus on verification and
validation of transformations. The proposal
in [27] introduces a method to check semantic
equivalence between the initial model and the
generated code. The approach in [7] verifies
transformation correctness with respect to
semantic properties by model checking the
transition system of the source and target models.
The work in [10] aims at developing frameworks
for transformation testing.
56 D.H. Dang, M. Gogolla / VNU Journal of Science: Comp. Science & Com. Eng., Vol. 32, No. 1 (2016) 42–57
Fig. 15: Metamodels for the SC2EHA transformation.
8. Conclusion
We have introduced an approach for
specifying, realizing, and ensuring the quality of
model transformations: (1) The foundation of the
approach is based on the integration of TGGs
and OCL. We have further formulated operation
contracts for derived triple rules in order to
realize them as OCL operations with two views:
Declarative OCL pre- and postconditions are
employed as operation contracts, and imperative
command sequences are taken as an operational
realization. (2) Both declarative and operational
views are obtained by an automatic translation
from the RTL specification of transformations.
This work also embodies a new method to extract
invariants for transformations. The central idea
is to view transformations as models. (3) An
OCL-based framework for model transformation
has been established. As being realized on a
full OCL support environment like USE, the
framework offers a support for validation and
verification of transformations.
Our future work includes the following issues.
We aim to enhance the technique to extract
invariants for transformation models. A control
structure like sequence diagram for the RTL
specification is also in the focus of our future
work. The goal is to increase the efficiency
of transformations. The technique to generate
test cases from the RTL specification will also
be explored. We will focus on other properties
of transformations such as the determinateness
of transformation. These are efforts towards a
full framework for quality assurance of model
transformations. Larger case studies must give
detailed feedback on the proposal.
Acknowledgement
This work has been supported by the project
QG.14.06, Vietnam National University, Hanoi.
We also thank anonymous reviewers for their
comments on the earlier version of this paper.
D.H. Dang, M. Gogolla / VNU Journal of Science: Comp. Science & Com. Eng., Vol. 32, No. 1 (2016) 42–57 57
References
[1] S. Sendall, W. Kozaczynski, Model Transformation:
the Heart and Soul of Model-Driven Software
Development, IEEE Software 20 (5) (2003) 42– 45.
[2] T. Mens, P. V. Gorp, A taxonomy of model
transformation, Electronic Notes in Theoretical
Computer Science 152 (2006) 125 – 142.
[3] F. Jouault, F. Allilaire, J. Bzivin, I. Kurtev, ATL:
A Model Transformation Tool, Science of Computer
Programming 72 (1-2) (2008) 31–39.
[4] P.-A. Muller, F. Fleurey, J.-M. Jzquel, Weaving
Executability into Object-Oriented Meta-languages,
in: Proc. 8th. Int. Conf. Model Driven Engineering
Languages and Systems (MODELS), Vol. 3713,
Springer Berlin, 2005, pp. 264–278.
[5] OMG, Meta Object Facility (MOF) 2.0
Query/View/Transformation Specification, Final
Adopted Specification ptc/07-07-07, OMG, 2007.
[6] L. Lengyel, T. Levendovszky, H. Charaf, Validated
Model Transformation-Driven Software Development,
Int. J. Comput. Appl. Technol. 31 (1/2) (2008) 106–
119.
[7] D. Varr, A. Pataricza, Automated Formal Verification
of Model Transformations, in: J. Jrjens, B. Rumpe,
R. France, E. B. Fernandez (Eds.), Proc. 3rd
Workshop on Critical Systems Development in UML
(UML/CSDUML), Technische Universitt Mnchen,
2003, pp. 63–78.
[8] A. Schrr, Specification of Graph Translators with
Triple Graph Grammars, in: M. Schmidt (Ed.), Proc.
20th Int. Workshop on Graph-Theoretic Concepts in
Computer Science (WG), Vol. 903 of LNCS, Springer-
Verlag, 1995, pp. 151–163.
[9] J. Cabot, R. Claris, E. Guerra, J. d. Lara,
Verification and Validation of Declarative Model-to-
model Transformations Through Invariants, Journal of
Systems and Software 83 (2) (2010) 283–302.
[10] Y. Lin, J. Zhang, J. Gray, A Framework for Testing
Model Transformations, in: S. Beydeda, M. Book,
V. Gruhn (Eds.), Model-driven Software Development
- Research and Practice in Software Engineering,
Springer, 2005, pp. 219–236.
[11] M. Gogolla, F. Bu¨ttner, M. Richters, USE: A UML-
Based Specification Environment for Validating UML
and OCL, Science of Computer Programming 69 (1-3)
(2007) 27–34.
[12] J. Rumbaugh, I. Jacobson, G. Booch, The Unified
Modeling Language Reference Manual, 2nd Edition,
Addison-Wesley Professional, 2004.
[13] E. Mikk, Y. Lakhnechi, M. Siegel, Hierarchical
automata as model for statecharts, in: Advances in
Computing Science, Vol. 1345, Springer Berlin, 1997,
pp. 181–196.
[14] G. Pintr, I. Majzik, Modeling and Analysis of
Exception Handling by Using UML Statecharts,
in: Scientific Engineering of Distributed Java
Applications, Vol. 3409, LNCS, 2005, pp. 58–67.
[15] J. B. Warmer, A. G. Kleppe, The Object Constraint
Language: Precise Modeling with UML, 1st Edition,
Addison-Wesley Professional, 1998.
[16] M. Richters, A Precise Approach to Validating UML
Models and OCL Constraints, Ph.D. thesis, Universitt
Bremen, Fachbereich Mathematik und Informatik
(2002).
[17] J. Greenyer, E. Kindler, Reconciling TGGs with
QVT, in: G. Engels, B. Opdyke, D. C. Schmidt,
F. Weil (Eds.), Proc. 10th Int. Conf. Model Driven
Engineering Languages and Systems (MoDELS), Vol.
4735 of LNCS, Springer, 2007, pp. 16–30.
[18] D. Dang, M. Gogolla, An approach for quality
assurance of model transformations, in: D. V. Hung,
H. T. Vo, J. Sanders, L. T. Bui, S. B. Pham (Eds.), Proc.
4th Int. Conf. Knowledge and Systems Engineering
(KSE), IEEE Computer Society, 2012, pp. 223–230.
[19] D.-H. Dang, M. Gogolla, Precise Model-Driven
Transformation Based on Graphs and Metamodels, in:
D. V. Hung, P. Krishnan (Eds.), Proc. 7th Int. Conf.
Software Engineering and Formal Methods (SEFM),
IEEE Computer Society Press, 2009, pp. 307–316.
[20] D.-H. Dang, M. Gogolla, On Integrating OCL and
Triple Graph Grammars, in: M. Chaudron (Ed.),
Models in Software Engineering, Workshops and
Symposia at MODELS. Reports and Revised Selected
Papers, Vol. 5421, Springer, 2009, pp. 124–137.
[21] K. Anastasakis, B. Bordbar, J. M. Kster, Analysis
of Model Transformations via Alloy, in: Proc. 4th
Workshop on Model-Driven Engineering, Verification
and and Validation (MoDeVVA), 2007, pp. 47–56.
[22] D. Varr, Automated Formal Verification of Visual
Modeling Languages by Model Checking, Software
and Systems Modeling 3 (2) (2004) 85–113.
[23] J. E. Rivera, E. Guerra, J. d. Lara, A. Vallecillo,
Analyzing Rule-Based Behavioral Semantics of Visual
Modeling Languages with Maude, in: Software
Language Engineering, Vol. 5452, LNCS, 2008, pp.
54–73.
[24] L. A. Rahim, J. Whittle, A survey of approaches for
verifying model transformations, Software and System
Modeling 14 (2) (2015) 1003–1028.
[25] G. M. K. Selim, J. R. Cordy, J. Dingel, Model
transformation testing: The state of the art, in:
Proc. 1st Workshop on the Analysis of Model
Transformations, ACM, 2012, pp. 21–26.
[26] M. Gogolla, A. Vallecillo, L. Burguen˜o, F. Hilken,
Employing classifying terms for testing model
transformations, in: T. Lethbridge, J. Cabot,
A. Egyed (Eds.), Proc. 18th Int. Conf. Model Driven
Engineering Languages and Systems (MoDELS),
IEEE, 2015, pp. 312–321.
[27] H. Giese, S. Glesner, J. Leitner, W. Schfer, R. Wagner,
Towards Verified Model Transformations, in:
D. Hearnden, J. G. S, B. Baudry, N. Rapin (Eds.), Proc.
3rd Int. Workshop on Model Development, Validation
and Verification (MoDeVVA), Le Commissariat
l’Energie Atomique - CEA, 2006, pp. 78–93.