The SyVOLT tool verifies DSLTrans transformations by generating a state-space for the transformation's execution, and then proving structural contracts on that state-space. As with any verification activity, it is non-trivial to ensure that these contracts are error-free and correspond to the user's intention. SyVOLT detects and localizes errors in the input artefacts for the verification activity to provide the user with assistance in debugging the transformation and/or the contracts. This experience report details the techniques built into the analysis, monitoring, and reporting stages of the tool. These techniques include detection of invalid rules and contracts, a form of reachability analysis during state-space generation, and assisting the user in understanding why a contract fails to be satisfied.
• Computing methodologies → Model verification and validation; • Software and its engineering → Domain specific languages; Automated static analysis;
As the adoption of model-driven engineering increases in both
academia and industry, the verification of model-to-model or
modelto-text transformations becomes a critical part of software
development. Our verification research [
The SyVOLT tool [
However, the result of the verification process only indicates that the contracts are or are not satisfied by the transformation by providing counter-examples. It is still a significant efort to examine these counter-examples and localize the fault in the transformation and/or the contracts. As well, once the fault is localized, it may be non-trivial to modify the artefacts to obtain the desired contract result. One particular problem, partially addressed in this paper by the contract result analysis, is the situation where a contract is expected to fail, but instead is reported as satisfied .
The current paper addresses the dificulty in understanding the interaction of contracts with the transformation under study. As our contribution, we present three stages of fault detection and localization within the SyVOLT tool, at the appropriate level of abstraction. The first stage is analysis (Section 3), where transformation and contracts are examined to record dependency information, and ensure that transformations and contracts are valid before state-space generation begins. The second stage is the monitoring of state space generation (Section 4), where rules are examined to ensure they symbolically execute. Finally, the reporting stage (Section 5) ofers an explanation for why contracts have failed to be satisfied. 2
Our verification research concerns the creation of a symbolic
execution state-space for transformations, and verification of structural
contracts over that representation of the state-space. These
operations are performed by the SyVOLT contract verifier 1, which has
been employed in transformation verification research [
Our symbolic execution technique requires that the transformation
language being verified has reduced expressiveness, as in work by
Varró et al. [
The essential unit of a DSLTrans transformation is the rule. Rules contain matching and production elements and links in the MatchModel and the ApplyModel. In Figure 1 on the following page, the 1Available at https://github.com/levilucio/SyVOLT.
MatchModel is the white box in the top half of the rule, while the ApplyModel is the yellow box in the bottom of the rule. Rule application begins by matching elements and links found in the MatchModel (as well as connected elements in the ApplyModel) onto the input model of the rule. If this can be accomplished, then the elements and links in the ApplyModel (not connected to the MatchModel) are created in the output model.
As well, rules specify how elements of the output model were created from specific elements of the input model during rule application. This traceability information for the transformation is stored as traceability links, which are built between a newly generated element in the output model, and the elements of the input model that originated it.
The backward link construct in DSLTrans rules is used to match over these traceability links. Figure 1 depicts a rule containing two backward links. The backward links are denoted as dotted lines, connecting the Country and Community elements and the Child and Woman elements. These links enforce a dependency that the Community element must have been produced by a rule that matched on the Country element in an earlier layer of the transformation.
Rules are placed into layers in the transformation. The semantics of DSLTrans specify that all rules in a layer fully apply before the next layer is executed. Note that rules in a layer cannot match on the output produced by another rule in the same layer. 2.2
Our contract verification technique builds structures called path conditions, which represent the symbolic application of rules in the transformation by explicitly including the input and output elements and links matched over or created by those rules.
An example path condition is shown in Figure 2, which represents the application of four rules in the transformation. These rules are bounded in dashed boxes and contain elements and links which are typed from the input and output meta-models for the transformation.
The white top-half of the path condition is the input graph, while the grey bottom-half is the output graph. Lines between the input graph and output graph are traceability links, which record how the output elements were created during the execution of the transformation. This path condition can therefore be read as: “If only these four rules apply during a transformation execution, then (at least) these upper elements were present in the input model, and these lower elements are present in the output model.” The structural contracts used in our verification research represent patterns on the input and output models of a transformation.
For example, the input graph of the contract in the upper-half of Figure 3 contains a Family element and four connected Member elements. The output graph of the contract in the lower-half of the figure contains a Community element, two Man elements, and two Woman elements. The dashed lines represent the restriction that the output elements must have been produced by a rule that matched over the connected input element. 2.3.1 Contract Verification. Once the set of path conditions has been created for a transformation, then the pre-condition and postcondition for each contract are matched over these path conditions. In Figure 3, the pre-condition of the contract is composed of the elements in the upper half of the contract. The post-condition of this contract is all elements and links as shown in Figure 3.
If a contract is said to be satisfied by our technique, then whenever a transformation’s input model contains the pattern specified in the pre-condition of the contract, the output model produced by that transformation will contain the pattern specified in the contract’s post-condition (including traceability constraints). Otherwise, if the post-condition does not hold on a path condition, then we have found a counter-example to the contract, and those rule combinations represented by the path condition do not satisfy the contract.
The present paper focuses on how to assist the user in understanding the result of contract satisfaction through a number of debugging techniques. 3
The main operation of the SyVOLT tool is the generation of the state-space of rule execution. However, first an analysis stage occurs, where the transformation and contract are examined to detect dependencies between the contract and rules in the transformation, as well as inter-rule dependencies.
This dependency analysis has three primary objectives in a debugging context. The first objective is a sanity check to ensure that all rules can symbolically execute and all contract elements can be produced, such that the user is alerted to an invalid transformation or a contract which cannot be verified. The second objective is to record which elements of the contract and transformation depend on which rules in the transformation, as this information will be used when presenting the results of verification (Section 5).
Finally, the last objective is to support a slicing optimization [
The analysis process begins by examining all rules in the transformation to determine if any rule produces the elements and links in a particular contract. As well, we ensure that all backward links between input and output elements (denoting dependencies) in the transformation’s rules can be satisfied by earlier rules.
This element-matching allows our analysis to check if there exists an element or link in a contract or a rule that cannot be satisfied in the transformation. In this case, even before the contract prover executes we know that there is an error with the contract or the transformation such that the validation process will fail. When this occurs, the user is alerted to the precise missing element or link in the rule or contract so that it may be fixed. 3.2
Consider an intentional error in the FourMembers contract presented in Figure 3. Instead of having Woman elements in the Output graph (lower half) of this contract, assume that these are Female elements in the erroneous version. This represents the contract builder unintentionally using an old meta-model or making a typo.
When the contract prover is determining which rules the contract depends on, the output in Figure 4 will be produced. In the section marked a), the analysis indicates that the link from the Community element to the Female element cannot be found in the transformation. This indicates that no path condition will exist a) Error: Elements in contract ErrFourMembers link are missing:
Community - directLink_T - Female b) Error: Backward link might be missing in contract ErrFourMembers:
Member - trace - Female c) Looking for meta-model element: `Member' Rule Daughter2Woman contains meta-model element:
`Member' as `Child' Rule Father2Man contains meta-model element:
`Member' as `Parent' ... d) Looking for meta-model element: `Female' Error: Meta-model element `Female' not found in any rule! where the contract’s post-condition can be satisfied, and thus the contract will never hold.
The output marked b) states that there is also a backward link in the contract which cannot be satisfied by the transformation. That is, there is no rule that matches over a Member element and produces a Female element. To assist the user, the rules where these elements are presented are indicated in sections c) and d).
The c) section displays the transformation rules that contain a Member element. Note that these rules may contain the element as a sub-class instead. For example, the Father2Man rule contains a Parent element which is a sub-class of the Member element. This allows the user to focus on the rules which are likely candidates for errors.
Finally, the section marked d) informs the user of the error that no rule contains a Female element. All elements of the contract must be present in the transformation for successful verification, otherwise the user must modify the contract or transformation such that the element exists. 3.3
During our verification research, we noticed that our case studies
sufered from typos/inconsistencies, which meant that a number
of contracts could never be satisfied. For example, a contract for
the mbeddr case study (presented in the thesis of Oakes [
In this section, we wish to emphasize how crucial it is to detect or prevent these simple errors as early as possible in the verification process. These errors can potentially consume a large portion of debugging time, while not addressing the “interesting” reasons for verification failure.
The source of these errors was the manual nature of the
Eclipsebased editing environment used to initially create the
transformations and contracts [
More recently, we have developed an editor plugin2 for the Meta
Programming System (MPS) editor 3. MPS is a language workbench
for the rapid creation and use of domain-specific languages (DSLs),
which can ease the development of software [
As part of our verification research, we created the language
constructs necessary to build DSLTrans transformations and contracts.
The explicit modelling of languages in MPS allows for desirable
features during modelling activities, such as auto-completion and
type checking in the projectional editor [
For example, when creating DSLTrans rules or contracts,
elements and their attributes in the rule must be typed by the input
or output meta-models of the transformation. We (and others [
A rule not symbolically executing may indicate one of three
issues with the transformation which should be reported to the
user to investigate. The first case is where the required dependencies
for the rule were not present in the transformation. This may occur
if a backward link specifies a dependency not satisfied by any other
rules. The second case is where the user has not indicated that a
rule should symbolically execute enough times, as specified by a
dependency analysis [
Finally, the third case is that there may be an undesired
interaction between the transformation and its meta-model that has
4Note that the work of Selim [
The current implementation for the rule reachability analysis involves checking all path conditions periodically to determine which rules they abstract. If a rule appears in no path condition, then it either did not execute in that layer, or it has been removed by the pruning technique. An error is raised informing the user which rule did not execute, as well as the dependency information generated in the first stage of analysis (Section 3). This (rudimentary) information allows the user to debug and understand the execution of the rule, before further layers in the transformation are symbolically executed. 5
The last stage of fault detection and localization is the reporting of results to the user at the end of contract validation. Our aim is to assist the user in understanding why a particular contract has been or has not been satisfied by presenting the rules and rule elements that the contract requires. This allows the user to ensure that their intention for the contract matches the verification result, and if not, where modifications should be made.
In the contract verification step of the SyVOLT tool, we collect two sets of path conditions for each contract. The first set ( success) is where the contract is satisfied, and the second set ( fail) is where the contract is not satisfied. The tool examines these sets and provides the following information: • rulessuccess - Rules found in all successful path conditions • rulesfail - Rules found in all failed path conditions, and not present in rulessuccess • The precise elements and links that the contract requires from the set of rules rulessuccess • The contract is also tested against a failed path condition – The elements and links that could not be found on this path condition are reported – The user can use this information and a visualization of the path condition to better understand the failure of the contract, as in Figure 8 on the facing page
This comprehensive information allows the user to precisely determine how the contract is succeeding or failing, and have assurance that the result is as intended. 5.1
We will present the Neg_SchoolOrdFac contract in Figure 6a as an example for the information reported when a contract has counterexample path conditions.
Note that for this contract we expect counter-examples to be found. This contract represents the statement ‘Every School in the input model will produce an Ordinary Facility’. The rule dfacilities...OrdinaryFacility which performs this production is displayed in Figure 6b. However, the transformation also contains the dfacilities...SpecialFacility rule, which matches over a School element with (a) An example contract for analysing success/failure results.
(b) Rule needed for contract success. a special Service to produce a Special Facility element. Thus, the contract is expected to fail on path conditions that include the dfacilities...SpecialFacility rule.
For the Neg_SchoolOrdFac contract, as seen in Figure 7 on the line marked a), the contract prover indicates that there are six path conditions where this contract holds, and three path conditions where it does not. a) Name: Neg_SchoolOrdFac
Num Succeeded Path Conditions: 6
Num Failed Path Conditions: 3 b) Explaining contract result:
Good rules: (Rules in success set and not failure set)
dfacilities...OrdinaryFacilityPerson Bad rules: (Rules common to all in failure set)
dfacilities...SpecialFacilityPerson c) Contract requires elements from successful rules of type: School
OrdinaryFacility d) Examining failed path condition:
Daughter2Woman-Neigh2District-dfacilities...SpecialFacilityPerson e) Elements of contract that fail on this path condition: Could not find links of type:
OrdinaryFacility - trace_link - School
The contract result analysis indicates in the section marked b) that the dfacilities...OrdinaryFacility rule is common to all the successful path conditions. This is correct, as this rule must symbolically execute for the contract’s pre- and post- condition to match. As well, the dfacilities...SpecialFacility rule is common to all of the failed path conditions. This is sensible as this rule produces path conditions where the School element in the contract pre-condition is found, but the OrdinaryFacility element is not. Note that the analysis does not report rules that are both in the successful and failed path conditions to assist in narrowing down causes of success or failure.
The last two analyses precisely identify why the contract fails on the path conditions. Based on the dependency analysis performed in Section 3, the contract prover has a record of which elements and links the contract depends on for each rule. The analysis marked c) specifies that the contract depends on the School and OrdinaryFacility elements produced by the dfacilities...OrdinaryFacility rule.
On the line marked d), a path condition is selected from the failed set of path conditions to examine further. A matching is performed with extra debugging information which indicates on the line marked e) that the School - OrdinaryFacility traceability link could not be found in the path condition.
Match0 Daughter2
Woman
Family3 Apply1
Match10 Neighborhood2Family14
District daughters
Match19
registeredIn
Apply11 Child Neighborhood family goesTo schools
d...SpecFacPerson
School students special Service
Apply20
District facilities SpecialFacility members
Woman 5.1.1 Visualization. Figure 8 shows a visualization for the failed path condition mentioned in part d) from Figure 7. This information is presented for the user to understand how the contract fails to match on the path condition. However, it is dificult to comprehend as it presents a technical, graph-based representation. In comparison, Figure 2 on page 2 shows a hand-made (but more natural) visualization for a diferent path condition.
Another critique of this visualization is the inability to see the structure which would allow the contract to be satisfied. For example, the Neg_SchoolOrdFac requires a School element connected to a Service element through an ordinary link, not the special link shown in a pale yellow oval in the middle of Figure 8.
In future work, we intend to improve our visualization techniques by creating MPS plugins for visual viewers and editors of transformations, contracts, and path conditions. 6
There is significant previous work in the general field of model
transformation verification [
The work of Burgueneo et al. [
Cuadrado et al. [
The thesis of Amstel [
In this paper, we have discussed three analyses implemented in the SyVOLT tool to detect and report errors in the input transformation and contract to the user so that these errors can be fixed and successful verification can be achieved.
The checks and analyses detailed in this paper arose organically
out of the development of the contract verification tool, and have
been quite successful in detecting errors as well as giving insight
into the behaviour of the contracts and transformations [
An especially crucial feature which is lacking in SyVOLT is the
visualization of transformation execution, both before and after the
application of rules as well as the actual matching and rewriting
steps of each rule [
We note that these debugging questions are relatively simple,
and yet the igraph and T-Core libraries used in the SyVOLT tool
lack suficiently powerful debugging mechanisms, hindering
development. For future work, we are interested in developing and
promoting reusable libraries for graph-matching visualization and
debugging in concert with the ModelVerse [
Developing a systematic approach to developing contracts is also a goal of our research, requiring user experiments to determine how users build contracts and what debugging information they require. As well, an important task is to transfer our contract verification and debugging techniques from the DSLTrans model transformation language to others with more expressiveness.