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 o ers an on-the-fly verification 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 & Verification, Precondition and Postcondition, Invariant.
1. Introduction
are proposed in [8] as a similar approach for
Model transformation can be seen as the heart
of model-driven approaches [1]. Transformations
are useful for di erent goals such as (1) to
relate views of the system to each other;
(2) to reflect about a model from other domains
for an enhancement of model analysis; and
(3) to obtain a mapping between models in
di erent languages. Within such cases it is
necessary to o er 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
bidirectional transformations. In addition to
specificationandrealizationoftransformationsas
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 verification
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 specification and quality assurance
of transformations.
transformationhavebeenintroduced, assurveyed
in [2]. The works in [3, 4] o er 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)
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
a waiting period as usual.
A camera allows the
specification method of transformations and an
system to record cars running illegally in the
OCL-based framework for model transformation.
crossing during the red signal period.
We realize the approach in USE [11], a tool
with full OCL support. This o ers an on-the-fly
verification 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 specification and realization of
transformations. Section 4 proposes an OCL-
based framework for model transformations.
Section 5 explains how the framework could
o er 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.
The example statechart (Fig. 1) shows two
basic states On and Off, reflecting 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 specification the synchronization
betweenthetworegionscurrentlycurrentlyisnot
reflected. 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 refined by concurrently
operating sequential automata, imposing a tree
We
focus
on
a
transformation
situation
structure on them.
The refinement is expressed
between
a
statechart
and
an
extended
by the dotted arrows, e.g., the On state is refined
hierarchical
automaton.
A
UML
statechart
bytwosequentialautomata. Interleveltransitions
(state
machine)
[12]
o ers
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
restriction.
The transition is enabled only if its
a more restricted syntax than statecharts which
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 traffic 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 o er means so that transformations
This section explains foundations for a model-
driven approach to software engineering.
could be specified 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
3.1. Graph Transformation
Definition 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
a transformation.
considered as a
A transformation can be
program taking the source
 VG is a finite set of nodes (vertices),
and target model as the input and output. We
could expect several reasonable assumptions
on such a transformation model to be satisfied.
(3) Validating transformations: The aim is to
ensure a transformation is a “right” one by
executing the transformation in various scenarios
 EG  VGVG isabinaryrelationdescribing
the edges,
 sG;tG : EG ! VG are source and target
functions mapping graph edges to nodes,
and
and comparing the de facto result with the
expected outcome. The process cannot be fully
automated: The modeler has to define relevant
scenarios, so-called test cases, and then to
 lvG : VG ! L and leG : EG ! L are
functions that assign a label to a node and
an edge, respectively.
compare the obtained and expected result.
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

An OCL-Based Framework for Model Transformations

Đăng ngày | Thể loại: | Lần tải: 0 | Lần xem: 0 | Page: 16 | FileSize: M | File type: PDF
0 lần xem

An OCL-Based Framework for Model Transformations. This paper proposes an OCL-based framework for model transformations. The formal foundation of the framework is the integration of Triple Graph Grammars and the Object Constraint Language (OCL). The OCL-based transformation framework offers an on-the-fly verification of model transformations and means for transformation quality assurance.. Cũng như những thư viện tài liệu khác được bạn đọc giới thiệu hoặc do sưu tầm lại và giới thiệu lại cho các bạn với mục đích nâng cao trí thức , chúng tôi không thu phí từ bạn đọc ,nếu phát hiện tài liệu phi phạm bản quyền hoặc vi phạm pháp luật xin thông báo cho website ,Ngoài tài liệu này, bạn có thể download tiểu luận miễn phí phục vụ học tập Một số tài liệu download mất font không xem được, nguyên nhân máy tính bạn không hỗ trợ font củ, bạn tải các font .vntime củ về cài sẽ xem được.

Nội dung


1134923

Tài liệu liên quan