In this work, we address the performance problem in the deductive veri cation of model transformations written in the ATL language w.r.t. given contracts. Our solution is to enable incremental veri cation for ATL transformations through caching and reusing of previous veri cation results. Speci cally, we decompose the original OCL contract into sub-goals, and cache the veri cation result of each of them. We show that for ATL, the syntactic relationship between a model transformation change and a sub-goal can be used to determine if a cached veri cation result needs to be re-computed. We justify the soundness of our approach and its practical applicability through a case study.
We have developed the VeriATL veri cation system that soundly veri es the correctness of ATL
model transformations via Hoare-triples [
The ATL transformation ER2REL (Listing 1.1) is de ned via a list of ATL matched rules in a mapping style. The rst three rules map respectively each ERSchema element to a RELSchema element (S2S ), each Entity element to a Relation element (E2R), and each Relship element to a Relation element (R2R). The remaining three rules generate a RELAttribute element for each Relation element created in the REL model.
Then, the correctness of the ER2REL transformation is speci ed by using OCL contracts. As shown in Listing 1.2, two OCL preconditions specify that within an ERSchema, names of Entities are unique (Pre1 ), and names of Entities and Relships are disjoint (Pre2 ). One OCL postcondition requires names of Relations to be unique within each RELSchema (Post1 ). 1 context ER!ERSchema inv Pre1, Pre2 2 3 rule S2S f from s: ER!ERSchema to t: REL!RELSchema (name< s.name)g 4 5 rule R2R f from s: ER!Relship to t: REL!Relation ( name< s.name, schema< s.schema) g 6 7 context REL!RELSchema inv S4: 8 REL!RELSchema.allInstances() >forAll(s j genBy(s, S2S) implies 9 s . relations >forAll(r1 j genBy(r1, R2R) implies 10 s . relations >forAll(r2 j genBy(r2, R2R) implies 11 r1<>r2 implies r1.name<>r2.name ) ) )
Listing 1.3. The problematic transformation scenario of the ER2REL transformation w.r.t. Post1 1 context ER!ERSchema inv Pre1: 2 ER!ERSchema.allInstances() >forAll(s j s.entities >forAll(e1 j 3 s . entities >forAll(e2 j e1<>e2 implies e1.name<>e2.name))) 4 5 context ER!ERSchema inv Pre2: 6 ER!ERSchema.allInstances() >forAll(s j s.entities >forAll(e j 7 s . relships >forAll(r j e.name<>r.name))) 8 9 context REL!RELSchema inv Post1: 10 REL!RELSchema.allInstances() >forAll(s j s.relations >forAll(r1 j 11 s . relations >forAll(r2 j r1<>r2 implies r1.name<>r2.name)))
Listing 1.2. The OCL contracts for ER and REL
The source and target EMF metamodels and OCL contracts combined with the developed ATL transformation form a Hoare triple which can be used to verify the correctness of the ATL transformation. The Hoare-triple semantically means that, assuming the semantics of the involved EMF metamodels and OCL preconditions, by executing the developed ATL transformation, the speci ed OCL postcondition has to hold.
The rst version of VeriATL can successfully report that the OCL postcondition Post1 is not veri ed by the ER2REL transformation, but it does not provide any information to understand why this contract does not hold. To enable fault localization in VeriATL, we have proposed a systematic approach to decompose OCL postconditions into sub-goals based on static analysis and structural induction. Consequently, we can use the information (i.e. static trace information) in the decomposed sub-goals to slice the original transformation into transformation scenarios, and present the problematic ones to pinpoint the fault.
For example, to verify Post1, our decomposition generates 4 sub-goals, where:
The 4 sub-goals therefore yield 4 transformation scenarios to be veri ed. One of the 4 transformation scenarios is problematic (shown in Listing 1.3). VeriATL reports it to the developer to pinpoint the fault in Post1. The scenario consists of the original preconditions (abbreviated at the top), a slice of the transformation (in the middle) and an augmented transcription of the problematic sub-goal (at the bottom).
Notice that the static trace information referred by the sub-goal (the genBy predicate on Line
8, 9, 10) helps the transformation developer to understand that the error may happen only when
the relational schema s is generated from the rule S2S, and when the relations r1 and r2 are both
generated from the rule R2R. Therefore, the only relevant rules for the fault are S2S and R2R.
By analyzing the problematic transformation scenario in Listing 1.3, the transformation developer
observes that two Relships in the source model might have the same name. This would cause their
corresponding Relations, generated by the R2R rule, to have the same name, and thus falsifying
Post1. More examples of our OCL postcondition decomposition for automatic fault localization in
VerATL can be found on our online repository [
Fixing transformation bugs by VeriATL is an interactive process. Each change to the ER2REL transformation launches VeriATL to re-verify the contracts and generated sub-goals. In this work, we aim to improve the turnaround time of re-veri cation by running VeriATL incrementally. Therefore, we propose a solution for determining when the cached veri cation result of sub-goals can be reused.
For example, our approach aims to determine that when xing Post1 by modifying the R2R rule, the veri cation result of the sub-goal for Post1, where s genBy S2S, r1 genBy E2R, r2 genBy E2R can be reused. 3
Our approach for running VeriATL incrementally is summarized by Algorithm 1.
First, we distinguish an ATL transformation (initial transformation ) P from its modi ed version (evolved transformation) P'. The transition from P to P' (line 1) happens through the sequential application of transition operators that we de ne in Section 3.1. As shown by lines 2 - 4, if P' is invalid, e.g. it contains con icting rules, then the incremental veri cation is stopped (and restarted when the user reaches a valid transformation by further modi cations).
Next, we enumerate each sub-goal in P to determine whether the execution semantics of its referred rules in the static trace information is preserved by P' (Lines 5 - 11). The execution semantics preservation results of each sub-goal are cached by the array isPsv. Speci cally, we propose a syntactic approach to determine the execution semantics preservation (Lines 7 - 8), which checks the intersection between the referred rules in the static trace information of a sub-goal and the rule that the transition operator operated on.
Finally, the sub-goal does not need to be re-veri ed if it is a veri ed sub-goal in P, and the execution semantics of its referred rules in static trace information is preserved (Lines 14 - 15).
In what follows, we detail each of these steps, and justify the soundness of our approach. 3.1
Transition Operators The transition operators that are permitted to transit from an initial transformation to its evolved transformation are shown in Fig. 2. Some explanations are in order: { The add operator adds an ATL rule named R that transforms the input pattern elements srcs to the output pattern elements tars. Initially, the add operator sets the lter of the added rule to false to prevent any potential rule con ict. The bindings for the speci ed output pattern elements are empty. The operator has no e ect if the rule with speci ed name already exists in the initial transformation. { The delete operator deletes a rule named R. It hass no e ect if the rule with the speci ed name does not exist in the initial transformation. Algorithm 1 Incremental veri cation algorithm for VeriATL 1: P' = transit(P, operator) 2: if hasCon ict(P') then 3: abort 4: end if 5: for each s Î sub-goals of P do 6: if trace(s) Ï dom(isPsv) then 7: if trace(s) \ a ectedRules(operator, P, P') = ; then 8: isPsv[trace(s)] true 9: end if 10: end if 11: end for 12: for each s Î sub-goals of P 0 do 13: if s Î sub-goals of P then 14: if trace(s) 2 dom(isPsv) ^ isPsv(trace(s)) ^ veri ed(s, P) then 15: continue 16: else 17: re-verify(s) 18: end if 19: end if 20: end for { The lter operator strengthens/weakens the guard of the rule R by replacing its guard with the OCL expression cond. It has no e ect if a rule with the speci ed name does not exist in the initial transformation. { The bind operator modi es the way of binding the structural feature sf of the target element tar in the rule R to the binding OCL expression b. It has no e ect if the rule with speci ed name does not exist in the initial transformation. If the sf or the tar does not exist in R, the bind operator acts like adding a new binding. hoperator i ::= add R from srcs to tars j delete R j lter R with cond j bind R tar sf with b The core idea of our proposal is that a sub-goal s does not need to be re-veri ed after applying a transition operator op if op preserves the execution semantics of the referred rules in the static trace information of s. This is because proving sub-goals is the process of proving Hoare-triples whose correctness depends on contracts and execution semantics of the involved transformation rules: if neither of these artefacts are changed, the correctness of such Hoare-triple will not change.
However, in our experience, we nd that there are many cases when the execution semantics of the referred rules in the static trace information of a sub-goal is not strictly preserved, but the re-veri cation of the sub-goal is not needed. Therefore, we propose a syntactic approach to characterize these cases, thereby determining whether the re-veri cation of a veri ed sub-goal in the initial transformation is necessary.
Our syntactic approach checks the intersection between the referred rules in the static trace information of a sub-goal and the rule that the transition operator operated on. When the intersection is empty, the sub-goal does not need to be re-veri ed.
We justify the soundness of our syntactic approach in two steps. First, we brie y demonstrate
the execution semantics of the ATL matched rule (details can be found in [
The execution semantics of an ATL matched rule consists of matching semantics and applying semantics. The matching semantics of a matched rule involves: { Executability, i.e. the rule is not con ict with any other rules of the developed transformation. { Matching outcome, i.e. all the source elements that satisfy the input pattern, their corresponding target elements of output pattern have been created. { Frame condition, i.e. nothing else is changed in the target model except the created target elements.
Take the S2S rule in the ER2REL transformation for example, its matching semantics speci es: { Before matching the S2S rule, the target element generated for the ERSchema source element is not yet allocated (executability). { After matching the S2S rule, for each ERSchema element, the corresponding RELSchema target element is allocated (matching outcome). { After matching the S2S rule, nothing else is modi ed except the RELSchema element created from the ERSchema element (frame condition).
{ Applying outcome, i.e. the created target elements are initialized as speci ed by the bindings of the matched rule. { Frame condition, i.e. nothing else is changed in the target model except the initializations made on the target elements.
Take the S2S rule in the ER2REL transformation for example, its applying semantics speci es: { After applying the S2S rule, for each ERSchema element, the name of its corresponding
RELSchema target element is equals to its name (applying outcome). { After applying the S2S rule, nothing else is modi ed, except the value of the name for the RELSchema element that created from the ERSchema element (frame condition).
Next, we induct on the type of transition operator to prove the soundness of our syntactic approach, i.e. when the intersection between the referred rules in the static trace information of a sub-goal and the rule that the transition operator operated on is empty, it guarantees the reveri cation of a sub-goal is unnecessary: { add operator. The lter of the added rule is false. Thus, the added rule takes no e ects to the rest of rules in the developed transformation when applying the operator, including the rules referred by the static trace information of a sub-goal. Consequently, our syntactic approach is sound in this case. { delete operator. Strictly speaking, deleting a rule that is not referred by the static trace information of a sub-goal could potentially alter the applying semantics of the referred rules in the static trace information of the sub-goal. However, the fact that the deleted rule is not referred by the static trace information of a sub-goal implies that proving the sub-goal does not depend on the execution semantics of the deleted rule. Thus, our syntactic approach is sound in this case. { lter operator. Altering the lter of a rule that is not in the referred rules of a sub-goal could a ect the executability of those referred rules, i.e. when the modi ed rule con icts with any of the referred rules. However, as shown by lines 2 - 4 of Algorithm 1, our incremental veri cation approach applies only to valid transformation (i.e., free from rule con icts), which guarantees that the lter operator preserves the executability of the referred rules in the static trace information of the sub-goal. When applying the lter operator to a rule that is not in the referred rules of a sub-goal results a valid transformation, the number of source elements that satisfy the input patterns of those referred rules would not change. As a result, the same number of corresponding target elements of output patterns speci ed by those referred rules are generated. Thus, the matching outcome and the frame condition of the referred rules of a sub-goal are not a ected. These facts conclude that altering the lter of a rule that is not in the referred rules of a sub-goal would not a ect the matching semantics of those referred rules. Similar to the delete operator, the fact that the modi ed rule is not referred by the static trace information of a sub-goal implies proving that the sub-goal does not depend on the execution semantics of the lter-modi ed rule. Thus, our syntactic approach is sound in this case. { bind operator. When the rule of modi ed binding is referred by the static trace information of a sub-goal, it implies proving the sub-goal depends on the execution semantics of the bindingmodi ed rule (but not necessarily depends on the modi ed binding). In this case, we defensively reverify the sub-goal. However, similar to the delete operator, the fact that the rule of modi ed binding is not referred by the static trace information of a sub-goal implies proving the sub-goal does not depend on the execution semantics of the binding-modi ed rule. Thus, our syntactic approach is sound in this case. 4
While we used ER2REL for illustrative purposes, we evaluate the performance of our approach
on a more complex case study, i.e. the HSM2FSM transformation that translates a hierarchical
state machine (source) to a attened state machine (target) [
We pick 4 transition operators and manually apply them individually to the initial HSM2FSM transformation for our evaluation: (T1) add CS2RS from cs:HSM!CompositeState to rs:FSM!RegularState (T2) delete SM2SM (T3) lter T2TA with false (T4) bind IS2IS FSM!InitialState stateMachine with null
While other transition operations are possible, the rst two are designed to quantify the performance of our approach when the generated sub-goals in the initial transformation and evolved transformation are di erent, whereas the latter two evaluate our approach when the generated sub-goals are the same.
The impact of the 4 transition operations on the re-veri cation of the generated sub-goals for the 6 postconditions are summarized in Table 1. To fully evaluate our approach, we compute and verify the sub-goals no matter whether the original OCL postcondition is veri ed or not.
The cells in the rst row represents how many sub-goals are generated for the initial transformation, and the number of unveri ed sub-goals are shown in parenthesis. The cells in the next 4 rows represent the ratio reused sub-goals/generated sub-goals for each of the 6 postconditions after applying the designed transition operators.
As shown in the last column of Table 1, when applying our approach, at least 49% of the previous veri cation results can be reused. However, as our case study is small, more case studies are required to claim the generalization for the performance of our approach.
In addition, we can see in some of the cells that for some post-conditions none of the cached results are reused. By manual examination we con rm that in these cases the newly generated sub-goals and the e ects of the transition operation are highly coupled. 5
Incremental veri cation for general programming languages have drawn the attention of researchers
in recent years to improve user experience of program veri cation. Bobot et al. design a proof caching
system for the Why3 program veri er [
Leino and Wustholz design a two level caching for the proofs in the Dafny program veri er [
Logozzo et al. design the Clousot veri er [
Proofcert project aims at sharing proofs across several independent tools by providing a common
proof format [
According to surveys [
In summary, in this work we confront the performance problem for deductive veri cation of the ATL language. Our solution is to evolve the VeriATL deductive veri cation system with the incremental veri cation capability through caching and reusing of previous veri cation results. Speci cally, our incremental veri cation approach is based on decomposing the original OCL postconditions into sub-goals, and caching their veri cation results. We propose a syntactic approach, based on the syntactic relationship between a model transformation change and a sub-goal, to determine when the cached veri cation result of the sub-goal can be reused.
Our current work focuses on the performance aspect. We plan to extend our experimental evaluation with further case studies and investigate how to cache the veri cation results of subgoals more e ciently. In reality, xing a bug can be seen as a sequential application of our transition operators. We want to investigate how to optimize the full chain, e.g. caching the veri cation results of disappeared sub-goals that could reappear in future versions of the model transformation.
Our future work will focus on making the implications of a model transformation change visible
to the developers to guide their next move. When a developer edits source code, the sooner the
developer learns the changes' e ects on program analyses, the more helpful those analyses are [