VNU Journal of Science: Comp. Science & Com. Eng., Vol. 32, No. 1 (2016) 42–57
An OCL-Based Framework for Model Transformations
Duc-Hanh Dang1;, Martin Gogolla2
1VNU University of Engineering and Technology, Hanoi, Vietnam 2University of Bremen, Bremen, Germany
Abstract
Model transformation is an important building block for model-driven approaches. It puts forward a necessity andachallengetospecifyandrealizemodeltransformationaswellastoensurethecorrectnessoftransformations. ThispaperproposesanOCL-basedframeworkformodeltransformations. Theformalfoundationoftheframework is the integration of Triple Graph Grammars and the Object Constraint Language (OCL). The OCL-based transformation framework oers an on-the-ﬂy veriﬁcation of model transformations and means for transformation quality assurance.
Received 06 December 2015, revised 25 December 2015, accepted 31 December 2015
Keywords: Model Transformation, OCL, Validation & Veriﬁcation, Precondition and Postcondition, Invariant.
1. Introduction
Model transformation can be seen as the heart of model-driven approaches [1]. Transformations are useful for dierent goals such as (1) to relate views of the system to each other; (2) to reﬂect about a model from other domains for an enhancement of model analysis; and (3) to obtain a mapping between models in dierent languages. Within such cases it is necessary to oer methods to specify and realize model transformation as well as to ensure the correctness of transformations. This is really a challenge because of the diversity of models and transformations.
Problem. Many approaches to model transformationhavebeenintroduced, assurveyed in [2]. The works in [3, 4] oer mechanisms for model transformations in line with the Query/View/Transformation (QVT) standard [5]. The ideas in [6, 7] focus on the graph transformation-based approach for unidirectional transformations. TripleGraphGrammars(TGGs)
are proposed in [8] as a similar approach for bidirectional transformations. In addition to speciﬁcationandrealizationoftransformationsas proposed by these works, several papers discuss how to ensure the correctness of transformations. In [9] the authors introduce a method to derive Object Constraint Language (OCL) invariants from declarative transformations like TGGs and QVT in order to enable their veriﬁcation and analysis. The work in [10] aims to establish a framework for transformation testing. To the best of our knowledge, so far there has not been any suitable approach yet to support both speciﬁcation and quality assurance of transformations.
Contribution. (1) In this paper we focus on the integration of TGGs and OCL as a foundation for model transformation. Incorporating OCL conditions in triple rules of a triple graph grammar allows us to express better transformations. (2) Our approach targets both declarative and operational features
of transformations. Within the approach a Corresponding author. Email: hanhdd@vnu.edu.vn new method to extract invariants for TGG
42
D.H. Dang, M. Gogolla / VNU Journal of Science: Comp. Science & Com. Eng., Vol. 32, No. 1 (2016) 42–57 43
transformations is introduced. (3) We propose a speciﬁcation method of transformations and an OCL-based framework for model transformation. We realize the approach in USE [11], a tool with full OCL support. This oers an on-the-ﬂy veriﬁcation of transformations and means for quality assurance of transformations.
Outline. The rest of this paper is structured as follows. Section 2 motivates our work by meansofexamples. Section3introducesaformal foundation for speciﬁcation and realization of transformations. Section 4 proposes an OCL-based framework for model transformations. Section 5 explains how the framework could oer means for transformation quality assurance. Section 6 shows how the approach is realized in the USE tool. Section 7 comments on related work. The paper is closed with a conclusion and a discussion of future work.
a waiting period as usual. A camera allows the system to record cars running illegally in the crossing during the red signal period.
The example statechart (Fig. 1) shows two basic states On and Off, reﬂecting whether the system is turned on or o. There is a concurrent decomposition of the On state. The region on the left corresponds to the lamp state, and the region ontherightcorrespondstothecamerastate. Each of these regions is concurrently active. The On state is referred to as an orthogonal state, i.e., a composite state containing more than one region. Note that in our speciﬁcation the synchronization betweenthetworegionscurrentlycurrentlyisnot reﬂected. TheOffstate,whichdoesnothavesub-states, is referred to as a simple state.
The example EHA is another representation of theexamplestatechart. ThisEHAconsistsoffour
sequential automata (denoted by rectangles),
each of which contains simple states and
2. Motivating Example transitions. States can be reﬁned by concurrently operating sequential automata, imposing a tree
We focus on a transformation situation structure on them. The reﬁnement is expressed between a statechart and an extended by the dotted arrows, e.g., the On state is reﬁned hierarchical automaton. A UML statechart bytwosequentialautomata. Interleveltransitions (state machine) [12] oers a light-weight in statecharts are transitions which do not respect notation for describing the system behavior. the hierarchy of states, i.e., those that may In order to model-check statecharts, it is cross borderlines of states. The EHA expresses necessary to transform them and represent them them using labeled transitions in the automata in a mathematical formalism like Extended representing the lowest composite state that Hierarchical Automata (EHAs). EHAs have been contains all the explicit source and target states proposed in [13] as an intermediate format to of the original transition. For example, the facilitate linking new tools to a statechart-based interlevel transition from Count2 to RedYellow environment. This formalism uses single- in the statechart is represented by the transition source/single-target transitions (as in usual from Red to RedYellow together with the label automata), and forbids interlevel transitions. Count2. This label is referred as a source
The EHA notation is a simple formalism with a more restricted syntax than statecharts which
restriction. The transition is enabled only if its source and all state in the source restriction set
nevertheless allows us to capture the richer (fCount2g) are active. The interlevel transition formalism [13]. Figure 1 presents models for from Off to On is represented by the similar a trac supervisor system for a crossing of a transition in the corresponding automaton main road and a country road [14]. The lamp together with labels Green and CameraOff, controllerprovideshigherprecedencetothemain called a target determination. When taking the road as follow: If more than two cars are waiting transition, the target and all states in the target at the main road (this information is provided by determination set (fGreen, CameraOffg) are a sensor), the lamp will be switched from red entered and become active.
to red-yellow immediately, instead of obeying
44 D.H. Dang, M. Gogolla / VNU Journal of Science: Comp. Science & Com. Eng., Vol. 32, No. 1 (2016) 42–57
Statechart of the traﬃc light example
Target Determination = {Green, CameraOff}
Target Determination = {Count0}
Source Restriction={Count2}
Extended Hierarchical Automata (EHA)
Fig. 1: Statechart and extended hierarchical automaton for the trac light example. (adapted from [14])
The transformation example motivates 3. Foundations for a Model-Driven Approach
our work with the following requirements: (1) Specifying and realizing of transformations: We need to oer means so that transformations could be speciﬁed and performed, as well as source and target models could be represented and taken as the input and output of transformations. (2) Verifying transformations: We need to check if there are any defects in a transformation. A transformation can be considered as a program taking the source and target model as the input and output. We could expect several reasonable assumptions on such a transformation model to be satisﬁed. (3) Validating transformations: The aim is to ensure a transformation is a “right” one by executing the transformation in various scenarios and comparing the de facto result with the expected outcome. The process cannot be fully automated: The modeler has to deﬁne relevant scenarios, so-called test cases, and then to compare the obtained and expected result.
This section explains foundations for a model-driven approach to software engineering.
3.1. Graph Transformation
Deﬁnition 1 (Graphs and Morphisms). Let a set of labels L be given. A directed, labeled graph is a tuple G = (VG;EG;sG;tG;lvG;leG), where
VG is a ﬁnite set of nodes (vertices),
EG VGVG isabinaryrelationdescribing the edges,
sG;tG : EG ! VG are source and target functions mapping graph edges to nodes, and
lvG : VG ! L and leG : EG ! L are functions that assign a label to a node and an edge, respectively.
A graph is said to be empty, if the VG and EG are empty sets.
Let two directed, labeled graphs G = (VG;EG;sG;tG;lvG;leG) and H = (VH;EH;sH;tH;lvH;leH) be given. A graph
D.H. Dang, M. Gogolla / VNU Journal of Science: Comp. Science & Com. Eng., Vol. 32, No. 1 (2016) 42–57 45
morphism f : G ! H is a pair (fV; fE), where fV : VG ! VH, fE : EG ! EH preserves sources, targets, and labels, i.e., fV sG = sH fE and
fV tG = tH fE.
:Statechart sc
owner owner owner
onState:CompState
isConcurr=true name='On'
container
s2e:SC2EHA
c2s1:S2SH
eha eha:EHA
owner owner
onStateH:StateH name = 'On'
refined
lampAut:Automata
G
a:X
p
q c:Y
b:Y
H
a1:X
d:Z v
s c1:Y
b1:Y
lampState:CompState
isConcurr=false name='Lamp'
container
redState:CompState
isConcurr=false name='Red'
s2a1:St2Aut
c2s2:S2SH
s2a2:St2Aut
name = 'Lamp' container
redStateH:StateH name = 'Red'
refined
counterAut:Automata
name = 'Red'
Fig. 2: Two directed, labeled graphs G and H and a graph morphism G ! H (informally speaking, H contains G).
Figure 2 shows two directed, labeled graphs G and H and a graph morphism G ! H. The
Fig. 3: Triple graph for an integrated SC2EHA model.
Deﬁnition 3 (Triple Graph Grammar).
A triple rule tr = L ! R consists of triple graphs L and R and an injective triple morphisms tr.
mapping is represented by dashed lines between the nodes and edges of G and H.
Triple graph grammars (TGGs) have been
proposed as a means to specify bidirectional
L = (SL sL CL tL TL) tr s c t
R = (SR sR CR tR TR)
translations between graph languages. Integrated graphs obtained by triple derivations are called triple graphs.
Deﬁnition 2 (Triple Graphs and Morphisms). Three graphs SG, CG, and TG, called source, connection, and target graph, together with two graph morphisms sG : CG ! SG
and t : CG ! TG form a triple graph G = (SG sG CG ! TG). G is said to be empty,
if SG, CG, and TG are empty graphs. A triple
graph morphism m = (s;c;t) : G ! H between two triple graphs G = (SG sG CG ! TG) and H = (SH sH CH ! TH) consists of three graph
morphisms s : SG ! SH, c : CG ! CH and t : TG ! TH such that s sG = sH c and t tG = tH c. It is injective, if the morphisms s, c and t are injective.
Figure 3 shows a triple graph containing a statechart together with correspondence nodes pointing to the extended hierarchical automata (EHA). References between source and target models denote translation correspondences.
An application of a triple rule tr = (s;c;t) : L ! R to a given triple graph G to yield a triple graph H consists of the following steps:
Choose an occurrence of the LHS L in G by deﬁning a triple graph morphism m = (sm;cm;tm) : L ! G, called a triple match.
Glue the graph G and the RHS R according to the occurrences of L in G so that new items that are presented in R but not in L are added to G. This yields a gluing graph Z. Formally, we have m(L \ R) = G \ Z. Here, graphs can be seen as a set of items including vertices and edges.
Remove the occurrence of L from Z as well as all dangling edges, i.e., all edges incident to a removed node. This yields the resulting graph H. Formally, we have H = Z nm(L).
The gluing step allows us to obtain the so-called comatch morphism n = (sn;cn;tn), where sn = SR ! SH, cn = CR ! CH, and tn = TR ! TH. The induced morphisms sH : CH ! SH and tH : CH ! TH could be obtained from the comath morphism n.
46 D.H. Dang, M. Gogolla / VNU Journal of Science: Comp. Science & Com. Eng., Vol. 32, No. 1 (2016) 42–57
SL CL TL sm cm tm
3.2. The Object Constraint Language
G = (SG
SR tr s’ sn
H = (SH sH
CG
CR
c’
cn
CH tH
TG)
TR
t’ tn
TH)
The Object Constraint Langauge (OCL) [15] is a formal language to describe expressions on UML models, e.g., as shown in Fig. 5:
A triple graph grammar is a structure TGG = (TG;S;TR) where TG includes a so-called triple type graph and a typing function mapping so-called typed graphs to the type graph, S is an initial graph, and TR = ftr1;tr2;::::;trng is a set of triple rules. Triple graph language of TGG is the set fG j G is typed by TG ^ 9 triple graph transformation S ) Gg.
(1) OCL expressions, that might be object constraints or queries, do not have side eects. (2) The OCL is a typed language. Each valid (well-formed) OCL expression has a type, which is the type of the evaluated value of this expression. The type system of OCL includes basic types (e.g., Integer, Real, String, and Boolean), object types, collection types (e.g., Collection(t), Set(t), Bag(t), and Sequence(t) for describing collections of values of type t), and message types. (3) OCL is often employed for the following purposes:
{new} {new}
{new}
{new} {new}
Fig. 4: Triple rule for the SC2EHA transformation.
Figure 4 is part of a triple graph grammar thatgeneratesstatechartsandcorrespondingEHA models. This rule may create a simple state of a statechart and its corresponding state of the corresponding EHA model at any time.
Such an integrated triple graph is often deﬁned by a triple derivation. Derived triple rules allows us to compute the triple graph by taking the source (target or both) model as the input. A detailed explanation of how to apply derived
Fig. 5: Object model visualized by a class diagram.
To specify invariants, i.e., conditions that must be true for all instances of the class in all system states. Example:
-- The number of cars is -- greater than 10. context CarModel inv: self.car.size() > 10
triples is shown in SubSect. 3.5. To describe pre- and post conditions
Deﬁnition 4 (Derived Triple Rules). Each triple rule tr = L ! R derives forward, backward, and integration rules as follows:
on operations.
-- When a car is picked up. context Rental::assignCar(cr:Car) pre self.car = null
(SR s o sL CL tL TL) id c t
(SR sR CR tR TR)
forward rule trF
(SL sL CL t o tL TR) s c id
(SR sR CR tR TR)
backward rule trB
(SR s o sL CL t o tL TR) id c id
(SR sR CR tR TR)
integration rule trI
post self.car = cr
To describe guards within a statechart.
As a query language, i.e., to query the given where id is the identify function. system state by OCL expressions.
D.H. Dang, M. Gogolla / VNU Journal of Science: Comp. Science & Com. Eng., Vol. 32, No. 1 (2016) 42–57 47
OCL expressions are developed on the basis Aninterpretationofanobjectmodelisreferred of an object model. The aim is to allow us to as a snapshot (a system state). A snapshot is to express attribute values and logic conditions constituted by objects, links, and attribute values. on the structure deﬁned by the object model.
Speciﬁcally, the object model structure is extended with an OCL algebra [16].
Deﬁnition 5 (Object Models). An object model is the structure
M = (CLASS;ATTc;OPc;ASSOC;associates; roles;multiplicities;) where
1. CLASS N isasetofnamesrepresentinga
setofclasses,whereN A+ isanon-empty Fig. 6: A snapshot visualized by an object diagram. set of names over alphabet A. Each class
c 2 CLASS induces an object type tc 2 T. The values of the type refer to the objects of the class.
2. ATTc is the attributes of a class c 2 CLASS, deﬁned as a set of signatures a : tc ! t, where the attribute name a is an element of N, tc 2 T is the type of class c, and t 2 T is the type of the attribute.
3. OPc is a set of signatures for user-deﬁned operations of a class c with type tc 2 T. The signatures are of the form ! : tc t1 ::: tn ! t,where!isthenameoftheoperation, and t, t1, ... , tn are types in T.
4. ASSOC is a set of association names.
(a) associates : ASSOC ! CLASS+ is a
function mapping each association name to a list of participating classes. This list has
at least two elements.
(b) roles : ASSOC ! N+ is a function
mapping each association to a list of role names. It assigns each class participating
in an association a unique role name.
(c) multiplicities : ASSOC ! P(N0)+ is a function mapping each association to
a list of multiplicities. It assigns each class participating in an association a multiplicity. Amultiplicityisanon-emptyset of natural numbers (an element of the power set P(N0)+) dierent from f0g.
5. is a partial order on CLASS reﬂecting the generalization hierarchy of classes.
Figure 5 visualizes an object model in the form of a UML class diagram.
Deﬁnition 6 (Snapshots). A snapshot of an object model M is the structure
(M) = (CLASS;ATT;ASSOC) such that:
1. For each c 2 CLASS, the ﬁnite set CLASS(c) contains all objects of class c 2 CLASS existing in the snapshot: CLASS(c) oid(c).
2. Functions ATT assign attribute values for
each object in the state. ATT(a) : CLASS(c) ! I(t) for each a : tc ! ATT.
3. For each as 2 ASSOC, there is a set of current links: ASSOC(as) IASSOC(as). A link set must satisfy all multiplicity speciﬁcations: 8i 2 f1;:::;ng;8l 2 ASSOC(as): jfl0jl0 2 ASSOC(as) ^ (i(l0) = i(l))gj 2 i(multiplicities(as))
where
I(t) is the domain of each type t 2 T.
oid(c)istheobjectsofeachc 2 CLASS. The