Model transformations are crucial in model driven engineering (MDE). Automatic execution of model transformations improves software development productivity. However, model transformations should be verified to ensure that the models produced or the transformations satisfy some expected properties. In a previous work we presented a verification approach of graph-based model transformation systems based on relational logic. The approach encodes model transformation systems as Alloy specifications which are examined by the Alloy Analyzer. But experiments showed scalability and performance problems in the approach when complex relations were present in the systems. To solve these problems, we extend our previous work by using three techniques: 1) we change the encoding to decrease the arity of relations in the derived Alloy specifications; 2) we decompose the expressions for the pattern matching into sub-expressions using unique elements; 3) we use annotations to decrease the complexity of the metamodel and the model transformation rules. The results of our experiments indicate that the new techniques lead to better scalability and performance.
In model driven engineering (MDE), models are the first class entities of the software development. They are used to specify the domain under study, to generate program code, to document software, etc. Ideally, models in a development phase can be generated automatically from models in a previous phase by model transformations. Such automation makes MDE appealing by increasing productivity. However, errors may exist in model transformations and be propagated to subsequent phases resulting in erroneous models and software. Thus, verification of model transformations is a necessary task to ensure correctness, i.e. the produced models or the transformations satisfy some expected properties.
In our previous work [
To handle the scalability problem we change the encoding procedure, especially the part for matching the left and right patterns of the model transformation rules, to get rid of relations with high arity. A side effect of this change is that we get longer expressions for the pattern matching. This leads to increased verification time and worse performance. To handle the performance problem we extend our approach with two techniques: decomposition and annotation. With the first technique, we divide the expressions for the pattern matching into sub-expressions using unique elements. With the second technique, we use annotations to specify state information. This will decrease the complexity of the relations and the amount of the constraints in the metamodel.
Section 2 recalls the verification approach and presents some related background information. Sections 3, 4 and 5 present the changes in the encoding procedure, the usage of unique elements and the usage of annotations, respectively. In Section 6, we describe several experiments and present the results to show the effect of the new techniques. Related work is discussed in Section 7 and finally concluding remarks and future work are presented in Section 8. 2
In this section, we recall the verification approach for graph-based model
transformation systems detailed in [
Alloy is a specification language and an analyzing tool for relational models. The language is declarative, suited for describing complex model structures and constraints based on relational logic. Artifacts in a model are defined in Alloy as signatures while relations among them are defined as fields of the signatures. Some predefined signatures are offered, like Int . Constraints on specifications are defined as fact s while reusable constraints with parameters are defined as pred s. The Alloy Analyzer is a constraint solver which verifies Alloy specifications by first translating them into SAT problems and then resolving them using a SAT solver. It can find instances which are well-typed by (and are satisfying the constraints of) the specifications using the run command. One can also use the check command to find counterexamples violating some properties. Notice that Alloy performs a bounded check, i.e. for each signature, a user-defined scope bounds the number of its instances. 2.2
DPF provides formalization of (meta)modelling and model transformation based
on graph transformations [
[xor] nonActive active setTurn start
P [nand]
[
check [xor4]
F2 F1
T g a l F t e s 1 t s t i x e
A model transformation system consists of a metamodel (Fig. 1) together
with a set of model transformation rules (Fig. 2). The transformation rules
specify how a source model can be transformed to a target model. A model
l r
transformation rule p : L ←− K −→ R, consists of the left pattern L, the right
pattern R and the coordination pattern K, together with two injective graph
morphisms l and r. A model transformation consists of a sequence of direct
model transformations (application of one model transformation rule). The
execution of transformations follows the classic Double-Pushout (DPO) approach
as in [
In [
Each node Ni, i∈[1..m] is encoded as a signature SNi while each edge Ej, j ∈ [1..n] as a signature SEj with two fields src : one Ejs and trg : one Et. j The Alloy keyword one encodes that each edge has exactly one source (target) node Ejs (Ejt). Models are encoded as signatures SG with two fields nodes : set SN1 + · · · + SNm and edges : set SE1 + · · · + SEn encoding the contained nodes and edges. 2. The DPF predicates are encoded as preds in Alloy while constraints as f acts. 3. Direct model transformations are encoded as a signature Trans with 7 fields: the rule applied rule, the source and target model source, target, as well as, the deleted and added elements : dns and ans (nodes), des and aes (edges). 4. Each rule application is encoded as a predicate rulei[trans] stating that the transformation trans applies rule i. In this predicate, we encode that the source (target) model has exactly one match of the left (right) pattern in which some matched elements are deleted (added) according to the rule. 5. In order to ensure that each direct model transformation applies only one rule, for each type in the metamodel, a number restricts how many of its instances are deleted (added). 1 sig SNi {} // For each node Ni , i∈[1..m] 2 sig SEj { src: one Ejs , trg: one Ejt} // For each edge Ej , j∈[1..n] 3 sig SG{ nodes : set SN1 + . .s.o+urSceN,mt,aregdegte:so:nseetGrSaEph1 ,+. .d.ns+, aSnEsn:}set SN1 +. . .+SNm , 4 sig Trans { rule : one Rule ,
des , aes: set SE1 +. . .+SEn } 5 fact{ all t: Trans | rule1[t] or . . . or ruler [t ]}
After applying the encoding procedure, we verify the system by using the
Alloy Analyzer to examine the specification. The Alloy Analyzer searches for
counterexamples by executing the command check{constraint} f or scope. If
no counterexample is found, the property is verified correct within the scope.
Otherwise, a counterexample can be visualized to assist the designer to correct
the system. In [
The Alloy Analyzer performs a bounded check within a state space
determined by the scope. Given an Alloy specification consisting of m signatures, a
scope [s1, s2, ..., sm] bounds the size of the ith signature to si. For a relation
of arity n, the size of the state space containing all the possible instances is
2ˆ(Pim=1 si)n [
A direct model transformation is the application of one model transformation
rule. As a result, the source (target) model has a match of the left (right) pattern
of the rule with elements deleted (added) according to the rule. Assuming that
the left (right) pattern of a transformation rule is a connected graph containing
edges e1, . . . , em and nodes v1, . . . , vn (if the pattern is a disconnected graph, each
connected subgraph is encoded separately), the pattern matching is encoded as
one e1, . . . , em|p(e1, . . . , em), where p(e1, . . . , em) is the relational expression
about structure match and change. The Alloy keyword one enforces that only one
pattern is present in the source (target) model. For example, the right pattern
of the rule setF lag in Table 2 is encoded as follows:
1 one a: active &t.aes , s: setTurn &t.aes , pf:PF1&t.aes , f: F1R&t. aes |
2 let p=a.src , f1=pf.trg , r=f. trg |
3 p=a. trg and s.src=p and s. trg=p and pf.src=p and f. src=f1 and f1 in F1&t. ans
4 and r in R&(t. source .nodes -t. dns) and p in P&(t. source . nodes -t.dns)
The quantification one e1, . . . , em in the relational formula causes relations of
high arity in the Alloy specification. The Alloy Analyzer cannot handle such
quantification with larger scopes, especially when using the keyword one [
Thus, the scalability problem due to high-arity relations can be solved by the above mentioned change of the encoding. However, this leads to longer expressions for the pattern matching, which in turn will lead to poor performance during verification. In the following two sections, we introduce two techniques to address this problem and improve the performance. Note that in Section 6 we summarize the gains in translation time and verification time due to the optimization techniques discussed in the following sections. 4
In order to get rid of long expressions for the pattern matching, we decompose them into sub-expressions during the encoding procedure using unique elements. A deleted (added) element is unique if it is the only instance of its type deleted (added) during a direct model transformation. Usually some unique elements share a common structure. Consider the right pattern of the rule setF lag, in a transformation applying the rule, the added arrow :active in Fig. 2 is the only instance of active which will be added. The edges : setTurn and : P → :F1 are unique elements sharing the same :P . In addition, the unique elements :P →:F1 and :F1 →:R share the same :F1 . In the previous section, we encoded the pattern matching so that the whole pattern needed to exist in the target model. Here, we require that the three sub-patterns :ative :P :F 1 , :setT urn :P :F 1 and :F 1 :R exist in the target model. The :P in the first two sub-patterns are the same and the :F 1 in the last two sub-patterns are the same because the unique elements share them. After decomposition using the unique elements, the right pattern of the rule setF lag is encoded as: 1 some a: active &t. aes | let p=a. src|p in (t. source . nodes -t. dns) and p=a. trg 2 and some pf : PF1 &t. aes | let f1 = pf . trg | pf . src =p and f1 in t. ans 3 some s: setTurn &t. aes | let p=s. src|p in (t. source . nodes -t. dns) and p=s. trg 4 and some pf : PF1 &t. aes | let f1 = PF10 . trg | pf . src =p and f1 in t. ans 5 some e: F1R &t. aes | let f1 =e. src ,r=e. trg | f1 in t. ans and r in ( t. source . nodes -t.
dns) Now we use the following lemma to prove that the decomposition is valid. Lemma 1. Assume a pattern L is divided into two sub-patterns L1 and L2 where L1 ∪ L2 = L and L1 ∩ L2 = ΔL containing unique elements. In addition, the source and target nodes of the edges contained by ΔL are also contained by ΔL. We can prove that G has a match of L iff G has matches of g1:L1→G and g2:L2→G, where g1|ΔL = g2|ΔL.
P⇐rool1f.:Δ⇒L→SLt1r,alig2:hΔtfLo→rwLa2rdare the two inclusion maps. Due to the l1 Δ(1L) l2 assumptions, the square (1) in the right figure is a pushout. L1 L L2 Since g1|ΔL = g2|ΔL, we can get l1; g1 = l2; g2. Therefore, g1!g g2 there is a unique map !g:L→G. G In the new encoding procedure we identify sub-patterns sharing the same unique elements. In this way, long expressions for the pattern matching are decomposed into sub-expressions, thus gaining better translation time. 5
In this section, we use annotations to specify state information in the metamodel and the transformation rules. The encoding procedure is changed correspondingly. The complexity of the metamodel is decreased since we reduced the amount of signatures and constraints. 5.1
In Section 2, arrows (e.g. nonActive, start ) and nodes (e.g. F0 ) were used to
specify the states of a process. In this way, complex relations appeared in the
models. Furthermore, we needed to add extra constraints to correctly specify
states; the metamodel in Figure 1 had 28 constraints. In order to reduce the
number of the signatures and constraints, we use annotations to specify the
[
R <active> :R <F1> :P <non1<A:PscettivTeu>rn>
:T
2:P
<check>
:P :T
<check>
<crit> :T
:P :R
<F2>
<nonActive> :R
<F0> :P
<start>
:R
:R
state information; the new metamodel contains only 10 constraints. A similar
technique was used in [
Fig. 3 shows the metamodel using the annotation technique. The nodes R, P , T are the same as in Fig. 1. Annotations, e.g. <nonActive>, <Active> and <F1>, are used to specify state information instead of graph structures (like nodes and edges). We use three groups of annotations; for instance the group <Flag> with three annotations <F0>, <F1> and <F2>. Each group has an applicable type t in the metamodel. In an instance, each element typed by t can be marked with only one annotation from the group. In the example, all the annotation groups can be applied to instances of the type P .
Since the transformation rules in a model transformation system are defined
based on the metamodel, changing the metamodel requires also changing the
transformation rules. Different from the transformation rules in Section 2, the
rules are now defined with constraints as shown in Table 2. This implies that
we need to use constraint-aware model transformations as detailed in [
The three AG in the metamodel in Fig. 3 are encoded as follows: 1 sig AP_Flag { src : one P , trg: one Int} {trg >=0 and trg <2} 2 sig AP_At { src : one P , trg: one Int} { trg >=0 and trg <4} 3 sig AP_IsActive{ src : one P , trg: one Int } {trg >=0 and trg <3} 4 sig Graph { nodes : set P+R+T+ Int , edges : set PR + TP + TR + AP_Flag + AP_At + AP_IsActive} 6
In this section, we present experiments to study how the three techniques tackle the scalability problem and improve the performance. The first experiment shows how the change of encoding affects the scalability. The last two experiments show the effect of each optimization separately (see Table 3). All the experiments perform conformance verification and are executed on an Intel R CoreTMi5-2410M @2.30GHz*4 machine with 4GB RAM. The left column shows the scope, and each group of 3 columns shows the result of applying the techniques. Since the Alloy Analyzer uses SAT solver, we present the time cost for translation from Alloy specification to a SAT problem (TR), the verification time to solve the SAT problem (VE) and the total time (TO). Note that the table shows the total time for verifying all the constraints.
The results show that after changing the encoding procedure the approach scales better since we can verify the transformation system for larger scopes (even larger than 14). The results also indicate that the verification with the new encoding procedure is time consuming with large scopes; e.g. with scope 14 the TR is 33.8 minutes while the VE of is 8.5 minutes for all the 28 constraints.
With the decomposition technique, VE decreases to 30 seconds and the TR is around 3 minutes for the 28 constraints. The annotation technique shows even better performance: since the annotation approach reduces the constraints in the metamodel from 28 to 10, within scope 14, the TR reduces to 10125 ms, while the VE decreases to 16041ms for the 10 constraints.
Scope
Note that although the decomposition technique does not lead to as good performance as application of annotation, it is more generic in the sense that it could be applied to any model transformation system. But the annotation approach can only be used when state information is present in the system.
The literature related to the verification of model transformation systems is
becoming abundant. Some works propose verification approaches specialized for
specific languages. For example, verification of DSLTrans [
GROOVE [
In this paper we have presented an extension of our previous work [