Forschungsberichte
der Fakultät IV – Elektrotechnik und Informatik
Propagation of Constraints along
Model Transformations Based on
Triple Graph Grammars:
Long Version
Hanna Schölzel1, Hartmut Ehrig 1,
Frank Hermann 1, and Christoph Brandt 2
1 Institut für Softwaretechnik und Theoretische Informatik,
Technische Universität Berlin,
{hannas,ehrig,frank}@cs.tu-berlin.de
2 SECAN-Lab, Universite du Luxembourg,
christoph.brandt@uni.lu
Bericht-Nr. 2010 – 15
ISSN 1436-9915
Propagation of Constraints along Model
Transformations Based on Triple Graph Grammars:
Long Version
Hanna Sch¨olzel 1, Hartmut Ehrig 1,
Frank Hermann 1, Christoph Brandt 2
1Institut f¨ur Softwaretechnik und Theoretische Informatik, TU Berlin,
{hannas,ehrig,frank}@cs.tu-berlin.de
2SECAN-Lab, Universit´e du Luxembourg,
Abstract
Model transformations based on triple graph grammars (TGGs)
have been applied in several practical case studies and they convince
by their intuitive and descriptive way of specifying bidirectional model
transformations. Moreover, fundamental properties have been exten-
sively studied including syntactical correctness, completeness, termi-
nation and functional behaviour. But up to now, it is an open problem
how domain specific properties that are valid for a source model can
be preserved along model transformations such that the transformed
properties are valid for the derived target model. In this paper, we
analyse in the framework of TGGs how to propagate constraints from
a source model to an integrated and target model such that, when-
ever the source model satisfies the source constraint also the integrated
and target model satisfy the corresponding integrated and target con-
straint. In our main new results we show under which conditions this
is possible. The case study shows how this result is successfully ap-
plied for the propagation of security constraints in enterprise modelling
between business and IT models.
1 Introduction
Model integration and transformation between models as well as the compli-
ance of such models with concrete security requirements have already been
1
studied in different application domains, especially in the context of enter-
prise modelling [2]. In detail, it was possible to present how triple graph
grammars (TGGs) in the sense of Sch¨urr [14] can be used to realize the in-
tegration and transformation of those models. In addition to that, graph
constraints [4] were utilized to verify that business and IT models comply
with given security requirements.
:E/D
CS
PS
1:public
:E/D
Source Constraint publicIsEncrypted2 for IT-models
:Filter
1:public
1:public
CT
PT
Target Constraint publicIsFiltered2 for business models
aT
aS1:public
Filter
E/D
public
E/D
public
NW4:LAN
NW7:LAN
private
private
Private_Banking:Department
Investment_Banking:Department
private
public
private
private
private
public
pq
IT Model and IT Security Requirement Business Model and Business Security Requirement
pq
GSGT
Figure 1: IT and business models with security requirements
However, it remained an open question how graph constraints valid for
an IT model can be soundly propagated towards a corresponding business
model. For example, the IT constraint on the left of Fig. 1 (public commu-
nication has to be encrypted) should be transformed into a corresponding
business constraint (communication over public lines has to be filtered, right
of Fig. 1). This problem was identified as an operational need in the de-
centralized organizational environment of Credit Suisse [2], where security
requirements developed for IT models needed to be understood from the
point of view of the corresponding business models in order to ensure that
the different persons responsible for the business models, IT models and secu-
rity requirements will be able to integrate, transform and verify these models
successfully. While this paper presents the case study in concrete syntax the
presented techniques are based on the underlying typed attributed abstract
syntax graphs [4].
Furthermore, if an IT model satisfies the source constraint the corre-
sponding business model should satisfy the target constraint. In general,
given a requirement for a source model specified by a graph constraint we
would like to construct a corresponding requirement for the corresponding
target model with the following satisfaction property: Whenever a source
model satisfies the given source graph constraint then the target model, de-
2
fined by the model transformation, satisfies the corresponding target graph
constraint. In Fig. 1 the source model GSsatisfies the source graph con-
straint PC(aS:PS−→ CS), because for each match p:PS→GS(occurrence
of the premise graph) there is morphism q:CS→GS(occurrence of the
conclusion graph) with q◦aS=p.
In this paper we show under which conditions we are able to define a
propagation from source graph to target graph constraints such that this
satisfaction property is valid. First of all it makes sense to require strong
functional behaviour of the model transformation, which implies that we
have for each source model a unique target model. Moreover this allows for
each source graph constraint PC(aS:PS−→ CS) with premise PS, conclusion
CSand embedding morphism aSto obtain a unique target graph constraint
PC(aT:PT−→ CT) by applying the model transformation to PSand CS
leading to PTand CT. For this construction we require that PSand CS
are source models, i.e. PS, CS∈VLS, where VLSis the source language of
the model transformation MT :VLSVVLT. In this case the source graph
constraint PC(aS:PS−→ CS) is called MT-consistent and leads to a MT-
consistent target graph constraint PC(aT:PT−→ CT). In Sec. 2 we review
model transformation based on triple graph grammars [5, 14, 15] and prepare
our case study based on a model transformation from business to IT-models.
Our first main result in Sec. 3 shows that the satisfaction property stated
above for the propagation of security constraints is valid for MT-consistent
source and target constraints. In Sec. 4 we discuss how to extend the theory
to the case of partially MT-consistent constraints where premise or conclusion
consist only of model fragments, s.t. model transformations are not directly
applicable. Our constructions and results are illustrated by a case study of
security constraints in enterprise modelling.Acknowledgement: This paper is
a long version of our GT-VMT paper [6], and has been supported by the
DFG-Project Behaviour GT.
2 Model Transformation between Business
and IT Models
Triple graph grammars (TGGs) [14] are a well known approach for bidi-
rectional model transformations and we apply TGGs to define the model
transformation of our case study between business and IT models. For this
purpose we review main constructions and results of model transformations
based on triple graph grammars [15, 5] in this section.
Integrated models are defined as pairs of source and target graphs,
3
which are connected via a correspondence graph together with relat-
ing morphisms between these graphs. More precisely, a triple graph
G=(GS←
sG
−− GC−
tG
−→ GT) consists of three graphs GS,GC, and GT, called
source, correspondence, and target graphs, together with two graph mor-
phisms sG:GC→GSand tG:GC→GT.
(GS
mS
GGC
sG
oo
mC
tG//GT)
mT
(HS
H
mHC
sH
ootH
//HT)
A triple graph morphism m:G→H
with m= (mS, mC, mT) consists of three
graph morphisms mS:GS→HS,mC:
GC→HCand mT:GT→HTsuch that
mS◦sG=sH◦mCand mT◦tG=tH◦mC. A typed triple graph Gis typed
over a triple graph TG by a triple graph morphism typeG:G→TG and
a typed triple graph morphism m: (G, typeG)→(H, typeH) preserves the
typing, i.e. typeH◦m=typeG. Triple graphs may also contain attributed
nodes and edges according to [5] and they form an M-adhesive as well as
weak adhesive HLR category for which several important formal results have
been shown in [4].
(LS
trS
LLC
sL
oo
trC
tL//LT)
trT
(RS
R
tr RC
sR
ootR
//RT)
L
m
tr //R
n
(P O)
G
t
//H
Triple rules synchronously
build up source and target
graphs as well as their corre-
spondence graphs, i.e. they are
non-deleting. A triple rule tr is an injective triple graph morphism tr =
(trS, trC, trT) : L→Rand w.l.o.g. we assume tr to be an inclusion. Given
an (almost) injective triple graph morphism m:L→G, a triple graph trans-
formation (TGT) step G=
tr,m
==⇒Hfrom Gto a triple graph His given by a
pushout of triple graphs with comatch n:R→Hand transformation inclu-
sion t:G ,→H. Given a sequence of TGT-steps G0=
tr1,m1
===⇒G1... =
trk,mk
===⇒Gk
its trace is given by trace =tk◦. . . t2◦t1. A grammar TGG = (TG, S, TR)
consists of a triple type graph TG, a triple start graph Sand a set TR of
triple rules.
Example 1 (Triple Rules).The triple rules in Fig. 2 are part of the rules of
the grammar TGG in [2]. They are presented in short notation, i.e. left and
right hand sides of a rule are depicted in one triple graph. Elements, which
are created by the rule, are labeled with green ”++” and marked by green
line colouring. The rule LANToDepartment creates LAN element in the IT
model and a corresponding Department element in the Business model. The
rule PublicToPublic generates public edges with gluing nodes in both domains
simultaneously. The encryption/decryption nodes (E/D) are created in front
and at the end of a public Reo connector (depicted as black arrows) in the
rule EDToFilter, where in the Business model a Filter is attached to the
corresponding public Reo connector.
4
Loading more pages...