The correctness of model transformations and, in particular, behavior preservation is important for model-driven engineering of high quality software. Behavior preservation veri cation techniques have been presented with automatic tool support for the instance level, i.e. for a given source and target model speci ed by the model transformation. However, up until now there is no automatic veri cation approach available for operational model transformations at the transformation level, i.e. for all source and target models speci ed by an operational model transformation. In this paper, we outline a rst approach towards the automatic veri cation of behavior preservation for operational model transformations at the transformation level extending our previous results for relational model transformations. In particular, we show that in restricted cases the behavior preservation problem for an operational model transformation can be reduced to invariant checking for graph transformation with priorities illustrated by a simple example.
Introduction
The correctness of model transformations and, in particular, behavior preservation is a crucial element for
modeldriven engineering of high quality software. In this paper we focus on behavior preservation for operational
model transformations (cf. QVT operational [
We presented a rst approach [
The main result presented in this paper is a scheme for the automatic veri cation of behavior preservation at
the transformation level for operational model transformations given in the form of a restricted Story Diagram
(SD) [
The veri cation scheme presented in this paper shares some elements with our former work on checking
behavior preservation for relational model transformations [
8 SCT 2 MTC(REL) : SCT
CBis (1) 8 SCT
bsim sem(T ) (2):
In this work we have to adapt check (1) for all instances in MTC(REL) into a check (1 ) for all instances
in MTC(OP) conforming to our operational model transformation OP . In contrast check (2) can be reused as
described in [
8 SCT 2 MTC(OP) : SCT
CBis (1 ) 8 SCT
bsim sem(T ) (2):
The paper is structured as follows: In Section 2 we further describe our running example and explain our notion of operational model transformations. In Section 3, we reintroduce brie y all prerequisites for formalizing our notion of operational model transformations presented in Section 4 and the veri cation scheme presented in Section 5. This veri cation scheme is applied and evaluated by means of the running example in Section 6. We close the paper with some nal conclusions and an outlook on future work. 2
Operational Model Transformations with Story Diagrams
We rely on Story Diagrams [
Example 1 (Metamodel for Lifeline2Automaton). Fig. 1(a) shows the metamodel of our running example transformation from lifelines to automata. A lifeline describes the sending/receiving of messages on a timeline. It consists of Events and one distinguished event is marked as rst event. Events are connected with Send or Rcv objects. An automaton consists of States and one distinguished State is marked as initial state. States are connected with TR or TS objects. Events correspond to states, Send (Rcv) objects to TS (TR) objects. Fig. 1(b) shows a constraint forbidding the existence of two Events marked with rst.
1Note that other approaches for checking consistency of graph transformation systems w.r.t. graph constraints such as [
(a) active pre,post first
Story diagrams originate from the Uni ed Modeling Language (UML) [
A story pattern describes a transformation rule. Each story pattern speci es in a condensed format the types of objects and links that need to be matched or added (marked with ++) when applied to a model. These types correspond to a given metamodel containing classes and associations. Story patterns may have negative application conditions specifying which elements are forbidden for a valid match; those are crossed out.
In this paper we assume restricted SDs in particular consisting of a sequence of n > 0 particular WHILE loops containing one non-deleting story pattern without nesting: WHILE( 1);WHILE( 2); : : : WHILE( n): The loop condition coincides with the applicability of the contained story pattern. This is described in story diagrams by a success loop edge attached to the story pattern node and an outgoing failure edge. Finally we restrict to story patterns that obey to the prototypical structure as depicted in Fig. 1(c) (conditions a)-c) are depicted). They a) create a unique correspondence object c, b) have a non-empty fragment of source objects not linked to a correspondence object yet (i.e. to be translated) which will be linked to c (i.e. will be translated), and c) include at least the unique correspondence object for each already translated fragment that is referred to. Furthermore, we require d) that each story pattern contains a NAC forbidding for each source object to be translated by this story pattern that it is already translated. Finally, we require e) that the type of the created correspondence object c of each story pattern i is not present as a type required by some story pattern j occurring earlier in the story diagram. Note that story patterns of this prototypical kind preserve all elements of the source model and thus describe only outplace model transformations. These story patterns also relate source patterns via a unique correspondence objects to its translated target pattern. Each source pattern is only translated once and a story pattern i occurring after a story pattern j in the story diagram does not create new matches for j .
A restricted story diagram is then executed starting with the rst activity node succeeding the initial node. If a match for the story pattern of the current activity node is found, the story pattern is applied and the activity node linked via a success edge becomes the current one. Otherwise, the activity node linked via a failure is chosen. Due to the prototypical structure of the story pattern thus at rst a valid match for the source model is searched and then the prescribed correspondence and target elements are added while the source model is always preserved. Note that the prototypical structure of story patterns ensures termination for each nite source model, since each story pattern connects at least one source object to a correspondence object (i.e. at least one objects is translated) and it forbids source objects to be connected to more than one correspondence object (i.e. each object is translated only once).
Example 2 (SD for Lifeline2Automaton). Fig. 2(b) shows a Story Diagram that describes our example transformation. The story diagram starts with a lifeline and sets up a corresponding automaton related with correspondences step by step. The rst activity node creates an initial state for the rst event. Since there is only one rst event, this is done only once. Afterwards all other events are translated. Activity node three connects the states that belong to already translated events that are connected via a Send object properly. The fourth activity node is the same as the third, but for Rcv obejcts instead of send objects. In the top of Fig. 2(a) an example model transformation instance (with active edges as dynamic elements) is depicted computed by this SD.
The prototypical structure, while appearing to only impose additional restrictions, is actually also a means
of explicitly capturing traceability information required for the transformation. While other approaches and
model transformation languages may do this in an implicit way, they still require similar mechanisms. Moreover,
restricted SDs roughly correspond to the phased construction design pattern [
Formal Model In order to formalize operational model transformations and our veri cation scheme in the subsequent sections, we reintroduce the notions: typed graph, morphism, transformation, transformation system and constraint as well as graph language. Moreover we revisit control conditions for a transformation system and inductive invariants. Finally, we reintroduce how these notions can be generalized to so-called triple graphs, consisting of the following parts: the source (target) component describing the source (target) of a model transformation related by correspondence relationships in the correspondence component.
A graph G = (V; E; s; t) consists of a set V of nodes (also called vertices), a set E of edges, and two mappings
s; t : E ! V , the source and target mappings, respectively. Graphs can be equipped with typing over a given
type graph TG as usual [
We can further constrain this set of typed graphs using graph constraints. We restrict to a speci c kind of
constraints that can be handled by our invariant checker [
A graph rule : (L !r R; N AC ) consists of a graph morphism r, which is an inclusion and a socalled negative application condition (NAC) N AC = ^i2I (:9ni) with ni : L ! Ni. Given a graph rule : (L !r R; N AC ) and a graph G, can be applied to G if there is an occurrence of L in G i.e. an injective graph morphism m : L ! G, called match, such that m N AC . The latter is the case if for each ni in N AC it holds that there does not exist an injective morphism qi : Ni ! G such that qi ni = m. Note that we restrict to non-deleting rules in this paper. A direct graph transformation L r R GGr)ap;hmsTHG. from G to H or short G ) H via and m consists of the pushout (P O) in m (P O) n
For a set of rules R a direct graph transformation G )R G0 is given if a rule 2 R G h H
with G ) G0 exists. A graph transformation, denoted as G0 )R Gn, is a sequence
G0 )R G1 )R )R Gn of direct graph transformations. Graph rules and transformations can be equipped
with typing over a given type graph TG as usual [
The application of graph transformation (GT) rules from a GTS can be restricted via a so-called control
condition [
Triple graphs are de ned as introduced in [
TR s ecs c We say that TRS , TRC , TRT , and TRSC as shown below, ls ect t
lt lt ls
TRS s TRC s ecs c ect t TRT t TRSC s ecs c are the source, correspondence, target and source-correspondence component of TR, respectively.
Analogously, the projection of a graph G typed over TR to TRS , TRC , TRSC , or TRT selects the corresponding component of this graph. A triple graph (G; tripleG) is a graph G equipped with a morphism tripleG : G ! TR. We denote a triple graph as a combination of three indexed capitals, as for example SGCGTG, where SG denotes the source and TG denotes the target component of G, while CG denotes the correspondence component, being the smallest subgraph of G such that all c-nodes as well as all ecs- and ect-edges are included in CG. Note that CG has to be a proper graph, i.e. all target nodes of ecs and ect-edges have to be included. Moreover, CGS denotes the source-correspondence component of G.
Analogously to typed graphs, typed triple graphs are triple graphs typed over a distinguished triple graph
ST T CT T TT T , called type triple graph. In the remainder of this paper, we assume every triple graph SGCGTG
and triple graph morphism f to be typed over ST T CT T TT T , even if not explicitly mentioned. In particular, this
means that SG is typed over ST T , CG is typed over CT T , and T is typed over TT T . We say that SG (TG or CG)
is a source graph (target graph or correspondence graph, respectively) belonging to the language L(ST T ) (L(TT T )
or L(CT T ), respectively). Note that each source graph (target graph) corresponds uniquely to a triple graph
with empty correspondence and target (source and correspondence) components, respectively. Therefore, if it is
clear from the context that we are dealing with triple graphs, we denote triple graphs SG?? (??TG) with empty
correspondence and target components (source components) also as SG (TG), respectively. Typing a graph over
a type triple graph ST T CT T TT T already de nes the triples, i.e. any graph and any morphism typed over the
type triple graph ST T CT T TT T corresponds uniquely to a typed triple graph and a typed triple graph morphism,
respectively. Analogously [
The type graph ST T CT T TT T can be enriched with dynamic types for source and target languages and is then denoted as SRT CT T TRT . In particular, the bisimulation constraint CBis mentioned in the introduction and used throughout the paper is a graph constraint typed over SRT CT T TRT . If some graph SGCGTG, morphism m, rule , or condition ac is typed over a subgraph SSGCSGTSG of SRT CT T TRT , then it is straightforward to extend the codomain of the corresponding typing morphisms to SRT CT T TRT such that SGCGTG, m, ac, or are actually typed over SRT CT T TRT . We therefore do not explicitly mention this anymore in the rest of this paper. 4
Operational Model Transformations Formalized We formalize the source and target modeling language LS and LT of restricted SDs describing our operational model transformations (see Section 2) by a graph language with constraint. Thus we have a source and target graph language L(ST T ; CS ) and L(TT T ; CT ) with source and target type graph ST T and TT T and source and target constraints CS and CT , respectively. For example, Fig. 1(b) shows a fragment of the source constraint CS of our running example. The model transformation instances with correspondences belonging to LSCT are formalized by triple graphs. These instances conform to the metamodel of our model transformation that is formalized by a type triple graph ST T CT T TT T . To further restrict the set of model transformation instances with correspondences, we allow a graph constraint CSCT typed over the type triple graph ST T CT T TT T expressing restrictions on the correspondences between source and target models. W.l.o.g. we assume that CSCT comprises the source and target constraints CS and CT of the source and target graph language L(ST T ; CS ) and L(TT T ; CT ), respectively, such that the target component T of each SCT in L(ST T CT T TT T ; CSCT ) automatically belongs to L(TT T ; CT ).
For our veri cation scheme it will be important that traceability information for source elements is complete as well as unique in the following sense. Note that restricted story diagrams as described in Section 2 only create uniquely traceable model transformation instances.
De nition 1 (Uniquely/Complete Traceability). Given a triple graph SCT , then SCT is completely traceable, if each node s of S is connected via a correspondence edge to at least one correspondence node c of C. Moreover, SCT is uniquely traceable, if each node s of S is connected via a correspondence edge to at most one correspondence node c of C.
We formalize the story patterns present in a restricted SD by a set R of non-deleting triple graph transformation rules and the control ow by a control program P , being a speci c control condition over R. Note that as explained in the previous section, the prototypical structure of SPs in restricted SDs ensures that a control program over rules derived from these patterns terminates. Moreover, w.l.o.g. we assume that each control program P over R is complete meaning that each rule of R is used in P . if 9G00 : G )f 0g;WHILE( 0) G00 ^ G00 )R0;P 0 G0.
De nition 2 (Operational Rules & Control Program). An operational rule is a triple graph rule : (SLCLTL !r SLCRTR; N AC ) typed over ST T CT T TT T . Given a non-empty set of operational rules R, then a control program P over R is de ned recursively, as follows: WHILE( ) is a control program over f g, and WHILE( 0);P 0 is a control program over 0 [ R0 with P 0 a control program over R0 such that 0 is not in R0 and any rule in R0 is not allowed to create any new match for 0. Finally, G )f g;WHILE( ) G0 if G )f g G0 ^ G0 6)f g, and G ) 0[R0;WHILE( 0);P 0 G0
Now we are ready to formalize operational model transformations given as restricted SDs (see Section 2). De nition 3 (Operational Model Transformation OP). An operational model transformation OP = ((R; ST T CT T TT T ); P ); CSCT ) consists of a GTS (R; ST T CT T TT T ) with control program P over a non-empty nite set of operational rules R as given in Def. 2 typed over a uniquely traceable type triple graph ST T CT T TT T and a graph constraint CSCT typed over ST T CT T TT T . The induced model transformation with correspondences MTC(OP) consists of the subset of L(ST T CT T TT T ; CSCT ) containing exactly those triple graphs SCT for which there exists a triple graph transformation S )R;P SCT such that SCT is completely and uniquely traceable. A model transformation instance of MTC(OP) is an element of MTC(OP). 5
Veri cation Scheme for Checking the Bisimulation Constraint
Recall that for solving the behavior preservation problem we want to be able to check for some operational model
transformation OP that all its instances ful ll the bisimulation constraint CBis, i.e. 8SCT 2 MTC(OP) : SCT
CBis (1 ) (see Sect. 1). In our veri cation approach, we aim at reducing this problem to invariant checking. In
principle, this means showing that CBis holds for each valid source model S (induction base) and that CBis is an
inductive invariant of the operational model transformation OP (induction step). We conduct the veri cation
with our invariant checker [
Lemma 1 (Mapping of Control Programs to Priorities). Given a graph transformation system with control program ((R; ST T CT T TT T ); P ) with non-empty rule set R and control program P we can derive a GTS with priorities ((R; ST T CT T TT T ); p) such that
G )R;P G0 =) (
G )R;p G0 ^
G0 6)R ): Proof. We de ne priorities following the recursive de nition of a control program in Def. 2. For W HILE( ) a control program over f g we de ne the priority p( ) := 1. For W HILE( 0); P 0 such that P 0 is a control program over R0 we de ne p( 0) := maxfp( )j 2 R0g+1. More informally, we have that the priority p( 0) is the maximum of the priorities of all rules occurring in P 0 incremented by 1. Now we can prove the above condition. For W HILE( ) the above condition is trivially true. For W HILE( 0); P 0 we assume that the above condition holds for P 0 over R0 ( ). Given G ) 0[R0;WHILE( 0);P 0 G0, then by de nition 9G00 : G )f 0g;WHILE( 0) G00 ^ G00 )R0;P 0 G0. By hypothesis ( ) for G00 )R0;P 0 G0 it follows that G00 )R0;p G0 and G0 6)R0 . Consequently, since 0 has by de nition a higher priority than all rules in R0 and they do not create new matches for 0 it follows that G ) 0[R0;p G0 and G0 6) 0[R0 .
Example 3. The priorities for our model transformation example are depicted in Figure 2(c) by the ordering.
Two problems occur when now trying to check CBis as an invariant of our operational model transformation OP. On the one hand not every constraint in CBis holds for each valid source model S (induction base) and on the other hand CBis might be too weak to be established as an inductive invariant for the operational rules with priorities derived from OP (induction step). In the following theorem we therefore present a derived bisimulation constraint that we can check as an alternative invariant such that in the end 8SCT 2 MTC(OP) : SCT CBis (1 ) holds. w For a successful induction base we argue that CBis can be weakened to a constraint CBis because of completeness and uniqueness of the traceability information in each model transformation instance. For a successful induction step we introduce a so-called transformation constraint CTR that can be used to strengthen CBis. De nition 4 (weakened bisimulation constraint, transformation constraint, derived bisimulation constraint). w Given a bisimulation constraint CBis typed over SRT CT T TRT , then a graph constraint CBis typed over SRT CT T TRT is a weakened bisimulation constraint for CBis if (1) for each completely and uniquely traceable triple graph SCT CBwis also implies SCT CBis and if (2) each graph S 2 L(ST T ; CS ) satis es CBwis. Moreover, a graph constraint CTR typed over SRT CT T TRT is a transformation constraint for CBis if each graph S 2 L(ST T ; CS ) w satis es CTR. The graph constraint CB0is = CBis ^ CTR is then a derived bisimulation constraint for CBis. Theorem 1. Given an operational model transformation OP = (((R; ST T CT T TT T ); P ); CSCT ) as in Def. 3 and a bisimulation constraint CBis typed over SRT CT T TRT , then 8SCT 2 MTC(OP) : SCT CBis if the graph transformation system with priorities ((R; ST T CT T TT T ); p) derived from ((R; ST T CT T TT T ); P ) according to Lemma 1 has a derived bisimulation constraint CB0is as given in Def. 4 as inductive invariant.
Proof. We prove rst that each SCT 2 MTC(OP) satis es CB0is by induction over the length of the graph transformation needed to create some triple SCT 2 MTC(OP). (Induction base) The weakened bisimulation w constraint CBis and also the transformation constraint CTR are ful lled by construction. (Induction step) By construction and by Lemma 1. Then we know by de nition of the weakened bisimulation constraint that also CBis holds. 6
Application of Veri cation Scheme We outline in this section that for a bisimulation constraint CBis ful lling certain restrictions we can determine a related derived bisimulation constraint as required for Theorem 1. We exploit in the following that graph constraints may be trivially true for each potential model transformation instance (CBTirsue), that a graph constraint may hold for each source graph S in L(ST T ; CS ) (CBsrisc), and that for some constraints a weakened bisimulation S2T E2S
State
src TS tgt
State e1:Event a:E2S e1:Event a:E2S State pr:pre pr:pre src po:post s:Send c:S2T , po:post s:Send c:S2T TS tgt e2:Event b:E2S e2:Event b:E2S State constraint (CBwis) can be derived. In addition, we will show how a suitable transformation constraint CTR for CBis can be derived systematically.
T rue summarizes all graph constraints in CBis typed over SRT CT T TRT that
The trivially true constraint CBis are true for each potential model transformation instance SCT 2 L(ST T CT T TT T ). In particular, some of the conditions of CBis refer to dynamic elements required for the semantics de nitions as follows: Conditions of the form ^i2I 8(SPi CPi TPi ; 9SCi CCi TCi ) with SPi CPi TPi typed over SRT CT T TRT but not ST T CT T TT T alone are true for all SCT typed over ST T CT T TT T since the precondition can never be ful lled by a graph typed over ST T CT T TT T . Moreover, conditions of the form ^i2I :9SNi CNi TNi with SNi CNi TNi typed over SRT CT T TRT but not ST T CT T TT T alone are true for all SCT typed over ST T CT T TT T since SNi CNi TNi can never be found for a graph typed only over ST T CT T TT T .
T rue for our example. It is true for Example 4. The constraint fragment shown in Figure 3(a) is part of CBis all triple graphs SCT typed over ST T CT T TT T , since it describes the non-existence of dynamic elements and ST T CT T TT T does not contain dynamic types.
The invariant source constraint CBsrisc further summarizes all graph constraints in CBis typed over SRT CT T TRT that hold for each source graph S in L(ST T ; CSCB)sriasc,nd thus can be directly approached by the invariant checker.
Employing the introduced CBTirsue and we assume that CBis has the form CBTirsue ^ CBsrisc ^ ^i2I 8(SPi ; 9SPi CPi TPi ) and we can observe that in this case only the constraints of the form 8(SPi ; 9SPi CPi TPi ) (typed over ST T CT T TT T ) may be false for each valid source model. This is because they may imply the existence of a non-empty correspondence and target pattern for a speci c source pattern. Obviously, no graph typed only over ST T can ful ll this requirement. Hence, these constraints have to be weakened to ful ll the induction base for our inductive approach. We need a constraint CBwis such that each completey and uniquely traceable w triple graph SCT ful lling CBis also ful ls the original constraints and that each graph in the source language w L(ST T ; CS ) ful ls CBis (cf. Def. 4). ^Lie2mI8m(SaPi2; 9(SWPeiCakPeinTePdi )Btihseimn utlhaetiocnonCstornasitnrtaiCnBwtisCBw=is)C.BTGirsuivee^n CthBseriscb^isi^mi2uIla8t(iSonPi CcoPSnis;t9rSaiPnitCCPBiTisPi=) CisBTirsauew^eaCkBserinsce^d bisimulation constraint for CBis as given in Def. 4.
Proof. We have to show that (1) for each completely and uniquely traceable triple graph SCT with SCT CBwis, SCT CBis also holds and that (2) each graph S 2^Li2(SI8T(TS;PCiSC)PSsia;9tiSsPeiCsPCiBwTisP.i )(2th)ehnoSldCs Tby construction of CBwis. For (1) we in particular have to show that if SCT 8(SPi ; 9SPi CPi TPi ). First, it follows from the complete and unique traceability of the type triple graph ST T CT T TT T in OP and the fact that our constraint to be weakened is typed accordingly that for SPi only a unique extension CS can exist and due to the guaranteed type conformance CPSi must be a subgraph of that. Consequently, any completely and uniquely traceable SCT that matches SPi also matches SPi CS and thus SPi CPSi such that condition (1) must be ful lled as well.
Example 5. The constraint fragment in Figure 3(b) is part of ^i2I 8(SPi ; 9SPi CPi TPi ) for our example. Figure 3(c) shows how this fragment can be weakened such that it holds for each graph S in L(ST T ; CS ), i.e. for each valid source model, because no such graph S can contain correspondence nodes.
We further use a transformation constraint typed over ST T CT T TT T to strengthen the bisimulation constraint CBis = CBTirsue ^ CBsrisc ^ ^i2I 8(SPi ; 9SPi CPi TPi ) describing that the existence of a correspondence or target model node in a graph SCT implies that one of the rules capable of creating the respective correspondence or target model node has been applied and that one of those rules' side e ects (right-hand rule side) is present in SCT . By construction, this transformation constraint is ful lled by all source graphs S typed over ST T as these graphs contain no correspondence nodes and can thus never ful ll the precondition. Since the operational rules are derived from the operational rules, they will usually be inductive invariants. (a)
pre s:S2T , post
Event Event
Send
TS s:S2T E2S
State src tgt State
pre t:TS , post
Event Event
Send S2T E2S
State
src t:TS tgt
State Lemma 3 (Transformation Constraint CT R). Given a set of operational rules R = f iji 2 Ig with i : ri SLi CRi TRi ; N AC i ), then the related transformation constraint for correspondence nodes is (SLi CLi TLi ! CCi = 8(ci; _j2Ji 9SLj CRj TRj ) with ci a correspondence node in CRi but not in ri(CLi ) created by i and Ji = fjj j creates a correspondence node of the same type in ST T CT T TT T as cig I and the related transfor
T mation constraint for target nodes is C i = 8(ti; _j2Ji 9SLj CRj TRj ) with ti a target node in TRi but not in ri(TLi ) created by i and Ji = fjj j creates a target node of the same type in ST T CT T TT T as tig I. Given the bisimulation constraint CBis, then the constraint CT R = ^i2I C i ^ CTi is a transformation constraint for CBis C as given in Def. 4.
Proof. Since CT R = ^i2I C i ^ CTi is a constraint typed over ST T CT T TT T and it holds for each graph S 2
C L(ST T ; CS ), it is a well-de ned transformation constraint for CBis.
Example 6 (Transformation constraint). Two fragments of the transformation constraint CT R are depicted in Figure 4. Note that each valid source model satis es such constraints. In particular, the fragments state that the existence of a correspondence node of type S2T (T S) requires the existence of the side e ect of a rule capable of creating nodes of type S2T (T S, respectively). In both cases, there is only one such rule { the third rule in Figure 2(c), which creates T S and S2T nodes for Send nodes. Hence, the fragments' disjunctions (_j2Ji 9SLj CRj TRj ) contain only one condition each.
We performed the inductive invariant check for ((R; ST T CT T TT T ); p) with priorities p derived from the control
program P in OP according to Lemma 1 and the derived bisimulation constraint CB0is of our running example
Lifeline2Automaton introduced in Section 2 with our invariant checker [
For our example consisting of four transformation rules with at most 9 nodes and constraints with at most 9
nodes, the veri cation of condition (1 ) takes about 10 seconds on an Intel Core-i7-2640M processor with two
cores at 2,8 GHz, 8 GB of main memory and running Eclipse 4.2.2 and Java 8 with a limit of 2 GB on Java
heap space, which is very acceptable. As can be inferred from [
Conclusion and Future Work
In this paper, we presented a rst approach towards the automatic veri cation at the transformation level of
behavior preservation captured by bisimulation for operational model transformations. To achieve this, we also
presented a formalization of restricted Story Diagrams with a mapping to graph transformation systems with
priorities. Our main result has been obtained by reusing parts of our approach for relational model
transformations [
Besides the covered control constructs for operational model transformations such as while loops and sequence, operational model transformations may also employ as special cases single transformation steps, conditionals, general loops, nesting, or speci c means to hand over binding from one rule to another. Also the type of language constraints as well as transformation rules might become more complex and may contain, for example, arbitrary levels of nesting. While in many cases these constructs can be mapped on the outlined restricted form, it remains an open question whether the approach can be extended to also cover these more general forms. Another open question is whether the required correspondence model (traceability information) is really necessarily an element that has to be speci ed explicitly as part of the operational model transformation or whether it can be synthesized systematically in a pre-processing step of the veri cation. As future work we plan to approach the outlined open questions and also study the feasibility by means of larger and more complex case studies.