We report on the use of a formal veri cation tool for a graph-based transformation language in the context of a case study. The tool identi ed two bugs in the transformation that had eluded all previous testing e orts. The paper describes what we learned about the analysis of model transformations and how we intend to use these insights to improve the veri cation tool.
Model transformations are used to achieve many tasks in MDD, one of which is facilitating the analysis of models by translating them into an analyzable language in such a way that analysis results are preserved [LAD+15].
UML-RT [Sel98] is a UML pro le that has been used for the development of event-driven, soft real-time systems. It is supported by commercial MDD tools such as IBM RSA-RTE [IBM] and the open-source tool Papyrus-RT [Fou]. To enable analysis, a translation of UML-RT state machine diagrams and capsule diagrams into a language called Kiltera was recently developed [PD14].
Kiltera [PD10a] is a language for expressing, simulating, and analyzing systems that are either concurrent or distributed. Kiltera allows for code to be executed in di erent, dynamically changing locations, and supports a notion of time that in uences execution behaviour. A Kiltera program consists of processes that communicate asynchronously over channels. Its formal semantics is based on an timed extension of the -calculus [PD10b]. As in the -calculus, channels can be sent as parts of messages which allows for the easy implementation of, e.g., (1) call-backs by providing a called process with a \handle" to be used to send computation results back to the caller, and (2) the dynamic aspects of UML-RT (such as optional and dynamic capsules).
Paen [Pae12] has implemented a transformation of UML-RT state machines into Kiltera process models [PD14] in ATL. We refer to this transformation as the UML-RT-to-Kiltera model transformation. We now summarize the relevant parts of the metamodels of this transformation. 2.1
The Source UML-RT metamodel In UML-RT, a system's structure is speci ed as a capsule diagram composed of system components or capsules. The behavior of these capsules is speci ed using state machine diagrams (e.g., Fig. 1). We discuss the concepts of UML-RT metamodel by stating class names (which correspond to UML-RT concepts) in italics, and referring to examples of these concepts in Fig. 1.
A UML-RT state machine has one or more (hierarchical) States, for example, states `n2' and `n3' in Fig. 1. States are traversed through Transitions, such as transition `t1' in Fig. 1. Transitions can be sibling transitions between states in the same hierarchical level, incoming transitions from a state to one of its sub-states, outgoing transitions from a sub-state to its containing state, or initial transitions from a state's InitialPoint (e.g., `init1' in Fig.1) to one of its sub-states (classes SIBLING0, IN1, OUT2, and association initialTransition). Transitions can have Trigger s, where each trigger is composed of a Signal received on a Port. For example, transition `t1' in Fig. 1 is triggered by signal `sig1' on port `p1'. A transition crossing state boundaries is broken into segments, where each segment links EntryPoints (e.g., `a1' in Fig. 1) and/or ExitPoints (e.g., `b1' in Fig. 1). 2.2
The Target Kiltera Metamodel Next we introduce the concepts of the Kiltera metamodel considered by Posse and Dingel [PD14]. Kiltera includes ve classes of constructs: expressions (class Expr ), patterns (class Pattern), guards (Class ListenBranch), de nitions (Class Def ), and processes (class Proc). Expressions and patterns can be constants, variables, and tuples. Expressions also include function calls. Table 1 enumerates a subset of the guards, de nitions, and processes relevant to this study (including their syntax and their corresponding classes from the Kiltera metamodel). We discuss the semantics of these Kiltera constructs in the following.
A process de nition of the form proc A(x1; : : : ; xn) = P de nes a process A with parameters xi that are used in the body of the process P . Thus, the instantiation process A(E1; : : : ; En) instantiates a process de ned by P roc A(x1; : : : ; xn) = P where the parameters xi are substituted in P by the values of the expressions Ei. The process done represents a successfully terminated process. A trigger (i.e., a!E) outputs the value of expression E over channel a. In listener processes (i.e., whenfG1 ! P1j : : : jGn ! Png), Gi is an input guard which takes the form ai?Ri@yi, where ai is a channel, Ri is a pattern, and yi is a variable. A listener listens to channels ai of the guards Gi. When a channel ai is triggered with a value matching the pattern Ri of guard Gi, three steps are carried out: (1) process Pi is executed, (2) variable yi of guard Gi stores the time waited by the listener, and (3) the alternative guards are ignored. The new process (i.e., new a1; : : : ; an in P ) creates the channels ai that are private to process P . Conditionals have the standard semantics. Local de nitions (i.e., deffD1; : : : ; Dngin P ) declare the de nitions Di and executes P , where the scope of Di is the entire term. Parallel and sequential processes represent the parallel and sequential composition of the processes in the term. 2.3
The UML-RT-to-Kiltera Model Transformation Mapping Rules Due to space limitations, we describe the required mapping informally, using the examples shown in Figs. 1 and 2. The detailed mapping rules between the UML-RT and Kiltera metamodels are described in [PD14].
Fig. 1 shows a state machine with one composite state n2 and Fig. 2 shows the equivalent Kiltera mapping of state n2. The UML-RT-to-Kiltera transformation, in general, maps (a) any state n to a Kiltera process de nition named Sn, (b) the entering of a state n to an instantiation of Kiltera process Sn, and (c) signals of transitions' triggers to Kiltera channels in the output. Thus, the composite state n2 in Fig. 1 is mapped to a process de nition Sn2 (Fig. 2) with some parameters. Sub-states n3 and n4 of state n2 are mapped to nested process de nitions Sn3 and Sn4 of process Sn2 (line 3 of Fig. 2).
To encode transitions with triggers for state n2, process Sn2 has a sub-process Handler (lines 9-15 in Fig. 2) which is a listener process that handles all events of state n2. For example, one branch of the Handler subprocess waits for input on channel sig1 (representing waiting for the reception of sig1 by state n2). Once an input is received, the Handler sends an exit request to state n2's active sub-state on the exit0 channel. When the sub-state sends an acknowledgement on the exack0 channel, the Handler `instantiates' process Sn1 corresponding to the transition's target state n1.
When state n2 is entered, the choice of the sub-state to enter next is encoded using sub-process Dispatcher of process Sn2 (lines 6-8 in Fig. 2). If state n2 is entered through entry point a1 (identi ed by the argument passed to parameter enp of the Dispatcher) that is connected to sub-state n4, then the Dispatcher instantiates Sn4. If, however, state n2 is entered through an entry point that is not explicitly connected to a sub-state, then the Dispatcher follows state n2's initial transition and enters the initial sub-state (i.e., instantiates Sn3).
Exit point b1 of state n2 is mapped to a sub-process Bb1 of process Sn2. Subprocess Bb1 executes two steps in parallel: (1) triggers a stop handler request on channel sh (short for stop handler), and (2) instantiates process Sn1 corresponding to the target state n1 of the transition leaving the exit point.
We brie y overview the DSLTrans model transformation language, the property prover we built for verifying DSLTrans transformations, and properties that are provable using our prover. DSLTrans [BLA+11] is a graphical model transformation language that is Turing incomplete, i.e., DSLTrans can not specify unbounded loops. Transformations built using DSLTrans are con uent and terminating by construction. In DSLTrans, a transformation is composed of a set of ordered layers that are executed sequentially. A layer contains one or more transformation rules that execute in a non-deterministic order but produce a deterministic result. Each rule is a pair (MatchModel, ApplyModel ) where the MatchModel/ApplyModel is a pattern of source/target metamodel elements (called match/apply elements in DSLTrans). Match elements can be of two types: Any match elements are bound to all matching instances in the input model, and Exists match elements are bound to only one matching instance in the input model.
Fig. 3 shows an example of a DSLTrans rule (called `State2ProcDef') from the rst layer of the UML-RT-toKiltera transformation. The MatchModel of the `State2ProcDef' rule has a `State' element of type Any from the UML-RT metamodel and the ApplyModel has one `ProcDef' element and three `Name' elements from the Kiltera metamodel. This means that every `State' input model element will be transformed into a `ProcDef' output model element connected to three `Name' elements (with literals exack, exit, and enp). The attribute name of the `ProcDef' element is the concatenation of S and the name of the State element in the MatchModel. When a DSLTrans rule executes, traceability links are created between each element in the rule's MatchModel and each element in the ApplyModel. These keep track of which output elements came from which input elements.
Rule `MapBasicStateNoTrans' in Fig. 4 shows three additional DSLTrans constructs: attribute conditions on match elements, free variables, and backward links. Attribute conditions on match elements (e.g., the conditions on the attributes `isComposite' and `hasOutgoingTransitions' of the `State' match element in Fig. 4) act as a lter on the matching process, where only `State' elements ful lling these attribute conditions are matched. DSLTrans uses free variables and backward links to allow a rule to refer to a speci c element that has already been created in a previous layer.
The two rules in Figs. 3 and 4 show an example of how free variables and backward links are used, where (i) both rules have a free variable with a value of `procdef' in the apply element `ProcDef', and (ii) rule `MapBasicStateNoTrans' has a backward link appearing as a vertical dashed line between the `ProcDef' apply element and the `State' match element. The rst occurrence of the free variable `procdef' (without a backward link) in rule `State2ProcDef' (Fig. 3) of the rst transformation layer binds the `procdef' variable to the `ProcDef' element generated by the rule. Any occurrences of the free variable `procdef' in successive layers with backward links (e.g., in rule `MapBasicStateNoTrans' of the second transformation layer shown in Fig. 4) matches only previously generated `ProcDef' elements that have been bound to the same free variable `procdef'. Thus, rules with apply elements that are not connected by backward links (e.g., `ProcDef' element of rule `State2ProcDef' in Fig 3)
State2ProcDef MatchModel
State Type=Any ApplyModel 1 2 3 4 5 6
State2ProcDef State MapBasicStateNoTrans State MapBasicState State MapCompositeState State ExitPoint2ProcDef State, ExitPoint State2Handler State State2Dispatcher Trans2InstSIB Trans2InstOUT Trans2Inst Trans2ListenBranch MapExitWithTrans Trans2HListenBranch MapStatesINtrans MapNesting ProcDef, Name ProcDef, Null ProcDef, Listen, ListenBranch, Trigger ProcDef, LocalDef, New, Par, Inst, Name LocalDef, ProcDef, Name, Par, Trigger LocalDef, ProcDef, Name, Listen, Listen
Branch, Null, Seq, Trigger State, Transition, EntryPoint, StateMacine LocalDef, ProcDef, Name, ConditionSet, Inst Transition, Vertex, StateMachine, SIBLING0 Inst, Name Transition, StateMachine, Vertex, OUT2 Inst, Name State, Transition, EntryPoint, StateMacine, Inst, Name IN1 State, Transition, Trigger, Signal Listen, ListenBranch, Inst ExitPoint, Transition Par, Inst State, Transition, Vertex, StateMachine, Trig- Listen, ListenBranch, Seq, Trigger, Inst ger, Signal State, Transition, IN1, Vertex ConditionSet, ConditionBranch, Expr, Inst
State LocalDef, ProcDef create output elements of the same type each time the MatchModel of the rule is found in the input. However, apply elements that are connected by backward links (e.g., `ProcDef' element of rule `MapBasicStateNoTrans' in Fig 4) are used to match an element that has been previously created. 3.2
DSLTrans Implementation of the UML-RT-to-Kiltera Transformation
DSLTrans Symbolic Model Transformation Property Prover Fig. 5 demonstrates the architecture of our property prover [SLC+14], now called SyVOLT. Our prover takes four inputs: the DSLTrans transformation of interest, the transformation's source and target metamodels, and the property to verify. Veri cation is then carried out in two steps, as shown in Fig. 5.
In the rst phase, the prover generates the set of path conditions representing all possible symbolic executions of the input transformation. Each path condition is generated by accumulating a possible combination of rules that can be triggered by some input model. We refer to the accumulated MatchModels (or ApplyModels) of all the rules in a path condition as the path condition's match pattern (or apply pattern). The path condition generation algorithm is explained in detail in [LOV14].
In the second phase, the prover veri es the input property on each path condition generated in the rst phase. The prover renders the property to be either true (if the property holds for each of the generated path conditions) or false with a counter example (if the property does not hold for at least one path condition). Our property prover is input-independent [ACL+15], i.e., property veri cation is performed once for the transformation and the veri cation result is guaranteed to hold for the transformation when run on any input model. 3.4
Properties Veri able Using the Symbolic Model Transformation Property Prover Three property types can be expressed and veri ed using our property prover: AtomicContracts, propositional formulae on AtomicContracts, and rule reachability. For this study we focus only on the rst two property types.
An AtomicContract is a pair (pre, post ) that speci es a property of the form: \if the input model satis es the precondition pre, then the output model should satisfy the postcondition post ". A (pre- or) postcondition is a constraint on the (input or) output model of the transformation in the form of a structural relation between Precondition Postcondition
Par freeVar = PAR (input or) output model elements. Pre- and postconditions are expressed using the same constructs as rules (described in Section 3.1). Postconditions may also have traceability links to link postcondition elements to precondition elements. Traceability links in postconditions signify that the property will only match an output model element that was previously created from (and hence, linked to) the input model element.
Fig. 6 demonstrates an AtomicContract AC1 used to express a property (referred to as P1 ) of the UMLRT-to-Kiltera transformation. AC1 (Fig. 6) is interpreted as: \two nested States in the input will always be transformed to two nested ProcDef s in the output". Using three traceability links in Fig. 6 (appearing as three vertical, dashed lines) mandates that AC1 will only match ProcDef and LocalDef elements that were previously created from State elements. Our property prover should prove that AC1 will always hold for the UML-RT-to-Kiltera transformation.
AtomicConstracts can be composed using standard propositional connectives. For instance, the implication `AC2 =) AC3' in (Fig. 7) captures the `2..*' multiplicity invariant (referred to as M1 )1: In the output, every Par element (i.e., a parallel composition) is associated with two or more Proc elements (i.e., processes) through the association p. More precisely, if an element of type `Par' (referred to as variable `PAR') is generated in the output (again as variable `PAR') in AC2, then this element must be connected to at least two `Proc' elements. 4
Testing and Veri cation of the UML-RT-to-Kiltera Model Transformation We begin by brie y describing how the transformation was tested during its development (Section 4.1). We then identify some relevant properties that the transformation should satisfy to be considered correct (Section 4.2). The application of our property prover to the transformation then follows (Section 4.3). 4.1
Testing The transformation was extensively unit tested using the following process: Each time a rule was created, appropriate input models to test that rule were created depending on the complexity of the rule. If the rule produced the expected output, development would proceed with the next rule; otherwise, the rule would be debugged. In total, the transformation was tested on 25 di erent input models, none of which revealed any bugs. 4.2
Properties of Interest We divide the desired properties of the UML-RT-to-Kiltera transformation into four categories: pattern contracts, multiplicity invariants, syntactic invariants, and rule reachability. Contracts are properties that relate elements of the source and target metamodels, and are expressed using AtomicContracts. Invariants are properties de ned on elements of the target metamodel only, and are expressed using propositional formulae of AtomicContracts. We summarize the four property categories and we demonstrate how exemplar properties from the four categories are formulated in our prover. The property categories are described in detail in [Sel15].
Pattern contracts require that if a certain pattern of elements exists in the input model, then a corresponding pattern of elements exists in the output model. For example, pattern contract P1 (Section 3.4, Fig. 6) ensures that \two nested States in the input will always be transformed to two nested ProcDef s in the output". 1Note that the two AtomicContracts in Fig. 7 have empty preconditions meaning that they will match on any input model. Precondition Postcondition
Inst freeVar = INST name=`Dispatcher Precondition Postcondition
Inst freeVar = INST name=`Dispatcher The rst phase of the veri cation, the generation of the path constraints (Figure 5), completed in less than 14 seconds2 and resulted in 57 di erent path conditions, i.e., 57 di erent feasible sequences of rule applications.
In the second phase of the veri cation, the path conditions are checked to see whether or not they satisfy the property input. For properties P 1, M 1, and S1 described in Section 4.2, this check completed in 12.72 secs, 1.59 secs, and 5.5 secs, respectively. Overall, none of the 11 multiplicity invariants took more than 2 secs to check, while the veri cation of the 5 pattern contracts took between 3 and 22 secs. The check of two syntactic invariants completed in less than 6 secs, while the third required 241 secs; the reason is that it is by far the most complex property, with 20 elements distributed over 4 atomic contracts. 4.3.2
Bugs found To our surprise, SyVOLT determined that the transformation was not correct, because it did not guarantee properties M1 and S1 (Figs. 7 and 8). More precisely, there are input models for which the transformation generates: (i) an output in which a Par is associated to fewer than two Procs (violating M1 ), and (ii) an output where an Inst named Dispatcher is created but a corresponding ProcDef named Dispatcher is not created (violating S1 ). After examining the generated counter examples, we determined that both bugs were caused by two rules R1 and R2 in di erent layers that were not guaranteed to be \applied together", i.e., that it was possible that R1 was applied, but not R2.
Neither of these bugs had been exposed by our rule testing while developing the transformation, and when we went back to the the original UML-RT-to-Kiltera transformation in ATL presented in [Pae12], it too, although also having been tested quite thoroughly, turned out to also contain the exact same two bugs.
An investigation of the source of these bugs revealed the following: 2All timings were done on a 2.8 GHz AMD Opteron processor running Ubuntu Linux.
exitPoints
ExitPoint Type=Any
Name literal=`sh_in p
Par freeVar=parexitpoint p
Trigger channel=`sh_in
MapExitWithT rans
Bug 1: Rule `ExitPoint2ProcDef' in layer 3 (Fig. 9) and rule `MapExitWithTrans' in layer 5 (Fig. 10) are supposed to generate the two Proc elements belonging to a Par element. First, rule `ExitPoint2ProcDef' (Fig. 9) generates a Par element associated to a Trigger element (which extends Proc). Then, rule `MapExitWithTrans' (Fig. 10) associates an Inst element (i.e., a second Proc element) with the same Par element previously generated by rule `ExitPoint2ProcDef' in layer 3, as shown by the free variable `parexitpoint'. However, execution of rule `ExitPoint2ProcDef ' does not mandate execution of rule `MapExitWithTrans' : e.g., a composite State in the input model with an ExitPoint that has no outgoing Transitions will cause rule `ExitPoint2ProcDef' (layer 3) to execute but not rule `MapExitWithTrans' in layer 5, resulting in an output containing a Par associated with only one Proc, violating M1.
Bug 2: Rule `MapCompositeState' in layer 2 generates an Inst named `Dispatcher' and rule `State2Dispatcher' in layer 3 generates a ProcDef named `Dispatcher'. Rule `State2Dispatcher' matches composite States with a positive application condition, or a PAC (speci ed using Exists match elements, described in Section 3.1). On the other hand, rule `MapCompositeState' matches any composite State, without specifying a PAC. Thus, rule `MapCompositeState' will match some composite States that are not matched by rule `State2Dispatcher' (if they do not satisfy the PAC), resulting in an output containing an Inst named Dispatcher, but not a ProcDef named Dispatcher (violating SS2 ). 4.3.3
Fixing the bugs For the rst bug, we merged the two rules `ExitPoint2ProcDef' and `MapExitWithTrans' into a new rule in layer 5. For the second bug, the MatchModel of the rule `MapCompositeState' (layer 2) was updated to include the PAC (speci ed as Exists match elements) of rule `State2Dispatcher' (layer 3), to guarantee that the two rules necessarily execute together. Due to page limitations, the new rules are not shown here (see [Sel15] for details). After these changes, our prover proved the revised transformation correct with respect to all 11 properties. 5
Our case study allowed us to make the following observations:
O1: \Bugs not triggered by a test input will not be found": The limits of testing are well-known, of course. However, the unwarranted trust we subconsciously placed in our tests surprised us and highlights the value of formal veri cation.
O2: \Make sure test inputs cover the input metamodel": Testing proved insu cient, because the metamodel was assumed to be more restrictive than it actually was, i.e., the input models produced by the prover as counter examples had been assumed to be malformed, but proved to be permissible state machines.
O3: \E ective input-independent veri cation of graph-based model transformations is possible": While the performance of an earlier version of our prover [SLC+14] was already quite good, the performance of SyVOLT observed in this non-trivial case study is encouraging and provides additional, albeit still anecdotal, evidence that the formal veri cation of transformations with respect all possible inputs is feasible and practical.
O4: \Refactoring is hard": The rst bug was introduced by a refactoring step that broke a single rule into the two rules 'ExitPoint2ProcDef' and 'MapExitWithTrans' described in the previous section. Unfortunately, the refactoring did not preserve correctness and was undone to x the bug.
O5: \Input/output-level properties" vs \rule-level properties": The bugs suggested to us that it is useful to distinguish two di erent kinds of properties: 1) input/output-level properties, i.e., pre- and postcondition-type properties that describe the desired shape of the output (e.g., all properties in Section 4.2); and (2) rule-level properties, i.e., properties that impose restrictions on the way the rules are applied in a transformation execution (e.g., \Rule R1 res in an execution if and only if rule R2 also res"). Input/output-level properties capture user-level requirements, while rule-level properties capture when the rules in an implementation work together properly to guarantee the requirements. The relationship is akin to standard pre- and post-conditions for programs (i.e., \contracts") and, e.g., behavioural interface speci cation and API method usage rules such as \method close should only be invoked after method open". The bene t of rule-level properties thus is that they, in some sense, describe how the transformation works and may provide necessary conditions useful for transformation development and documentation.
O6: Towards a development methodology for provably correct DSLTrans transformations: A hallmark of DSLTrans is that transformations are structured in sequentially executed layers L1; : : : ; Ln. The property language supported by SyVOLT is perfectly suited to capture the purpose of each layer Li+1 through a pair of formulas Fi and Fi+1 capturing input/output-level properties, such that the rules in Li+1 are deemed correct, if they transform input satisfying the pre-condition Fi into output satisfying the post-condition Fi+1. Development of the rules in layer Li+1 would go hand-in-hand with the development of the formulas Fi+1 with the iterative use of the prover until (i) the rules are correct with respect to Fi+1, and (ii) Fi+1 is considered strong enough to allow the construction of Li+2 and a suitable Fi+2. Failure to establish Fi+1 may force the developer to revisit a previous level Lj (j i) and revise Fj and, possibly, also the rules in Lj . 6
This paper presents results from our ongoing work on verifying graph-based model transformations. While an earlier version of the prover has been described before [SLC+14], the UML-RT-to-Kiltera case study and our experience verifying it is new to this paper.
The use of contracts for the veri cation has already been proposed in [EGdLW+13, CBBD09]. In contrast to our work, only input-dependent veri cation is supported. Input-independent veri cation has been realized in, e.g., [SCGDL14, CCR+10, BECG12]; of these, the rst two approaches allow analysis only with respect to speci c properties, while the third approach performed markedly worse than our approach in a comparison [SBC+13]. More information on approaches to verifying model transformations can be found in [ACL+15].
Tools to evaluate the coverage provided by a set of input models with respect to a given metamodel have been proposed [FBMLT09] and may have revealed the limitations of our initial tests. Recently it has been suggested that even stronger coverage is required [GS15] than we suggest in O2.
Tools that allow what we call \rule-level properties" include Groove [GdMR+12] and AGG [Tae03]. AGG supports a \critical-pair analysis" which checks if transformation rules are con uent. Groove's analysis is more comprehensive and supports a complete exploration of the state space of the transformation using CTL formulas.
The advantages of modularizing transformations in a way similar to DSLTrans' sequential layering (O6) has also been discussed by both [CM09] and [LKR13]. 7
The case study has been useful in the following ways: First, it has reinforced some already widely held, but unproven, beliefs (Observations O1, O2, and O4). It provides some additional evidence of the promise of our approach to model transformation veri cation (Observation O3). It provides us with a stimulus to think more about di erent kinds of properties. Rules form the building blocks transformations are made of, and occupy a higher level of abstraction than, say, statements in programming languages, while also being more uniform in their e ect and role than, say, methods and procedures in programming languages. This may mean that the development of rule-based transformation systems in general and graph-based model transformation systems in particular may bene t greatly from the kind of rule-level properties discussed in Observation O4. Finally, the case study has given us new ideas on how to evolve our work into a transformation system providing suitable tool support for rigorous development of correct DSLTrans transformations (Observation O5). In particular, support for the expression and veri cation of properties of individual layers and rule-level properties will be a focus (Observation O6). Encouragingly, it should be fairly straight-forward to extend our prover to support these additions.