=Paper=
{{Paper
|id=Vol-2245/mdebug_paper_1
|storemode=property
|title=Debugging of Model Transformations and Contracts in SyVOLT
|pdfUrl=https://ceur-ws.org/Vol-2245/mdebug_paper_1.pdf
|volume=Vol-2245
|authors=Bentley James Oakes,Levi Lucio,Clark Verbrugge,Hans Vangheluwe
|dblpUrl=https://dblp.org/rec/conf/models/OakesLVV18
}}
==Debugging of Model Transformations and Contracts in SyVOLT==
https://ceur-ws.org/Vol-2245/mdebug_paper_1.pdf
Debugging of Model Transformations and Contracts in SyVOLT
Bentley James Oakes Clark Verbrugge
McGill University, Montreal, Canada McGill University, Montreal, Canada
bentley.oakes@mail.mcgill.ca clump@cs.mcgill.ca
Levi Lucio Hans Vangheluwe
fortiss GmbH, München, Germany McGill University, Montreal, Canada
lucio@fortiss.org University of Antwerp, Antwerp, Belgium
Flanders Make, Belgium
Hans.Vangheluwe@uantwerpen.be
ABSTRACT then proved over the state-space, yielding combinations of rules
The SyVOLT tool verifies DSLTrans transformations by generating where the contract is satisfied, and combinations where it is not.
a state-space for the transformation’s execution, and then proving The SyVOLT tool and its input artefacts are presented in Section 2
structural contracts on that state-space. As with any verification to provide background information.
activity, it is non-trivial to ensure that these contracts are error-free However, the result of the verification process only indicates
and correspond to the user’s intention. that the contracts are or are not satisfied by the transformation by
SyVOLT detects and localizes errors in the input artefacts for providing counter-examples. It is still a significant effort to examine
the verification activity to provide the user with assistance in de- these counter-examples and localize the fault in the transformation
bugging the transformation and/or the contracts. This experience and/or the contracts. As well, once the fault is localized, it may be
report details the techniques built into the analysis, monitoring, and non-trivial to modify the artefacts to obtain the desired contract
reporting stages of the tool. These techniques include detection of result. One particular problem, partially addressed in this paper
invalid rules and contracts, a form of reachability analysis during by the contract result analysis, is the situation where a contract is
state-space generation, and assisting the user in understanding why expected to fail, but instead is reported as satisfied.
a contract fails to be satisfied. The current paper addresses the difficulty in understanding the
interaction of contracts with the transformation under study. As our
CCS CONCEPTS contribution, we present three stages of fault detection and localiza-
tion within the SyVOLT tool, at the appropriate level of abstraction.
• Computing methodologies → Model verification and vali-
The first stage is analysis (Section 3), where transformation and
dation; • Software and its engineering → Domain specific lan-
contracts are examined to record dependency information, and en-
guages; Automated static analysis;
sure that transformations and contracts are valid before state-space
ACM Reference Format: generation begins. The second stage is the monitoring of state space
Bentley James Oakes, Clark Verbrugge, Levi Lucio, and Hans Vangheluwe. generation (Section 4), where rules are examined to ensure they
2018. Debugging of Model Transformations and Contracts in SyVOLT. In
symbolically execute. Finally, the reporting stage (Section 5) offers
Proceedings of Debugging in Model-Driven Engineering (MDEbug). ACM, New
York, NY, USA, 6 pages.
an explanation for why contracts have failed to be satisfied.
1 INTRODUCTION 2 BACKGROUND
Our verification research concerns the creation of a symbolic execu-
As the adoption of model-driven engineering increases in both
tion state-space for transformations, and verification of structural
academia and industry, the verification of model-to-model or model-
contracts over that representation of the state-space. These opera-
to-text transformations becomes a critical part of software devel-
tions are performed by the SyVOLT contract verifier1 , which has
opment. Our verification research [9, 10] focuses on the proving
been employed in transformation verification research [1].
of structural contracts, which represent patterns on the input and
output models of a transformation written in the DSLTrans model
transformation language. If a contract is said to hold by our tech-
2.1 DSLTrans Transformation Language
nique, then whenever a transformation’s input model contains the Our symbolic execution technique requires that the transformation
pattern specified in the pre-condition of the contract, the output language being verified has reduced expressiveness, as in work by
model produced by that transformation will contain the pattern Varró et al. [18]. Our verification research operates on the model
specified in the contract’s post-condition (including traceability transformation language DSLTrans [2], which has the properties
constraints). of termination and confluence. A full treatment of the semantics of
The SyVOLT tool [8] verifies a set of contracts on a transforma- DSLTrans is found in the thesis of Oakes [10].
tion by generating a symbolic state-space for the transformation The essential unit of a DSLTrans transformation is the rule. Rules
through the combination of rule applications. The contracts are contain matching and production elements and links in the Match-
Model and the ApplyModel. In Figure 1 on the following page, the
MDEbug, October 2018, Copenhagen, Denmark
2018. 1 Available at https://github.com/levilucio/SyVOLT.
MatchModel is the white box in the top half of the rule, while least) these upper elements were present in the input model, and
the ApplyModel is the yellow box in the bottom of the rule. Rule these lower elements are present in the output model.”
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 ap-
plication. This traceability information for the transformation is Figure 2: A path condition which represents the application
stored as traceability links, which are built between a newly gen- of four transformation rules.
erated 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 2.3 Contracts
over these traceability links. Figure 1 depicts a rule containing
two backward links. The backward links are denoted as dotted The structural contracts used in our verification research represent
lines, connecting the Country and Community elements and the patterns on the input and output models of a transformation.
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.
Figure 1: A DSLTrans rule with backward links.
Figure 3: Pos_FourMembers contract, representing the infor-
Rules are placed into layers in the transformation. The semantics
mal statement “A Family with a father, mother, son and
of DSLTrans specify that all rules in a layer fully apply before the
daughter should always produce two Man and two Woman
next layer is executed. Note that rules in a layer cannot match on
elements connected to a Community”
the output produced by another rule in the same layer.
2.2 Path Conditions For example, the input graph of the contract in the upper-half
of Figure 3 contains a Family element and four connected Member
Our contract verification technique builds structures called path
elements. The output graph of the contract in the lower-half of
conditions, which represent the symbolic application of rules in
the figure contains a Community element, two Man elements, and
the transformation by explicitly including the input and output
two Woman elements. The dashed lines represent the restriction
elements and links matched over or created by those rules.
that the output elements must have been produced by a rule that
An example path condition is shown in Figure 2, which repre-
matched over the connected input element.
sents the application of four rules in the transformation. These
rules are bounded in dashed boxes and contain elements and links 2.3.1 Contract Verification. Once the set of path conditions has
which are typed from the input and output meta-models for the been created for a transformation, then the pre-condition and post-
transformation. condition for each contract are matched over these path conditions.
The white top-half of the path condition is the input graph, while In Figure 3, the pre-condition of the contract is composed of the
the grey bottom-half is the output graph. Lines between the input elements in the upper half of the contract. The post-condition of
graph and output graph are traceability links, which record how this contract is all elements and links as shown in Figure 3.
the output elements were created during the execution of the trans- If a contract is said to be satisfied by our technique, then when-
formation. This path condition can therefore be read as: “If only ever a transformation’s input model contains the pattern specified
these four rules apply during a transformation execution, then (at in the pre-condition of the contract, the output model produced
by that transformation will contain the pattern specified in the a) Error: Elements in contract ErrFourMembers link are missing:
Community - directLink_T - Female
contract’s post-condition (including traceability constraints). Oth- b) Error: Backward link might be missing in contract ErrFourMembers:
erwise, if the post-condition does not hold on a path condition, then Member - trace - Female
c) Looking for meta-model element: `Member'
we have found a counter-example to the contract, and those rule Rule Daughter2Woman contains meta-model element:
combinations represented by the path condition do not satisfy the `Member' as `Child'
contract. Rule Father2Man contains meta-model element:
`Member' as `Parent'
The present paper focuses on how to assist the user in under- ...
standing the result of contract satisfaction through a number of d) Looking for meta-model element: `Female'
debugging techniques. Error: Meta-model element `Female' not found in any rule!
3 DEBUGGING STAGE 1: ANALYSIS Figure 4: Dependency analysis presented for the erroneous
ErrFourMembers contract.
The main operation of the SyVOLT tool is the generation of the
state-space of rule execution. However, first an analysis stage oc-
curs, where the transformation and contract are examined to detect where the contract’s post-condition can be satisfied, and thus the
dependencies between the contract and rules in the transformation, contract will never hold.
as well as inter-rule dependencies. The output marked b) states that there is also a backward link
This dependency analysis has three primary objectives in a de- in the contract which cannot be satisfied by the transformation.
bugging context. The first objective is a sanity check to ensure that That is, there is no rule that matches over a Member element and
all rules can symbolically execute and all contract elements can be produces a Female element. To assist the user, the rules where these
produced, such that the user is alerted to an invalid transformation elements are presented are indicated in sections c) and d).
or a contract which cannot be verified. The second objective is to The c) section displays the transformation rules that contain a
record which elements of the contract and transformation depend Member element. Note that these rules may contain the element
on which rules in the transformation, as this information will be as a sub-class instead. For example, the Father2Man rule contains a
used when presenting the results of verification (Section 5). Parent element which is a sub-class of the Member element. This
Finally, the last objective is to support a slicing optimization [10, allows the user to focus on the rules which are likely candidates
11], which restricts the symbolic execution of the transformation for errors.
to only those rules needed to verify a contract. This optimization Finally, the section marked d) informs the user of the error that
therefore improves the debugging process for the user by winnow- no rule contains a Female element. All elements of the contract
ing away all rules that can not change the satisfaction of a contract, must be present in the transformation for successful verification,
and allowing the user to concentrate on the essential rules. otherwise the user must modify the contract or transformation
such that the element exists.
3.1 Procedure
The analysis process begins by examining all rules in the transfor- 3.3 Fixing Input Errors
mation to determine if any rule produces the elements and links During our verification research, we noticed that our case studies
in a particular contract. As well, we ensure that all backward links suffered from typos/inconsistencies, which meant that a number
between input and output elements (denoting dependencies) in the of contracts could never be satisfied. For example, a contract for
transformation’s rules can be satisfied by earlier rules. the mbeddr case study (presented in the thesis of Oakes [10]) con-
This element-matching allows our analysis to check if there tained ReferenceExpression and GlobalRefExpr elements instead of
exists an element or link in a contract or a rule that cannot be the correct ReferenceExpr and GlobalVarRef elements.
satisfied in the transformation. In this case, even before the contract In this section, we wish to emphasize how crucial it is to detect
prover executes we know that there is an error with the contract or or prevent these simple errors as early as possible in the verification
the transformation such that the validation process will fail. When process. These errors can potentially consume a large portion of
this occurs, the user is alerted to the precise missing element or debugging time, while not addressing the “interesting” reasons for
link in the rule or contract so that it may be fixed. verification failure.
The source of these errors was the manual nature of the Eclipse-
3.2 Example based editing environment used to initially create the transforma-
Consider an intentional error in the FourMembers contract pre- tions and contracts [8]. In the current version of the visual editor,
sented in Figure 3. Instead of having Woman elements in the Output the user is able to type in any name for rule elements without any
graph (lower half) of this contract, assume that these are Female validation against the transformation meta-models.
elements in the erroneous version. This represents the contract More recently, we have developed an editor plugin2 for the Meta
builder unintentionally using an old meta-model or making a typo. Programming System (MPS) editor 3 . MPS is a language workbench
When the contract prover is determining which rules the con- for the rapid creation and use of domain-specific languages (DSLs),
tract depends on, the output in Figure 4 will be produced. In the which can ease the development of software [17].
section marked a), the analysis indicates that the link from the 2 The plugin is available from within the MPS plugin repository under the name
Community element to the Female element cannot be found in the DSLTrans, or at the repository site https://github.com/mbeddr/language_verification.
transformation. This indicates that no path condition will exist 3 https://www.jetbrains.com/MPS
As part of our verification research, we created the language con- caused our pruning technique to remove all path conditions con-
structs necessary to build DSLTrans transformations and contracts. taining that particular rule. This technique removes path conditions
The explicit modelling of languages in MPS allows for desirable if they violate the output meta-model with respect to containment
features during modelling activities, such as auto-completion and links. For example, a path condition containing Female elements in
type checking in the projectional editor [5]. the output model not properly contained by a Community element
For example, when creating DSLTrans rules or contracts, ele- would be removed. Careful use of this technique is required, as it
ments and their attributes in the rule must be typed by the input may remove counter-examples to contracts [10].
or output meta-models of the transformation. We (and others [19]) The current implementation for the rule reachability analysis in-
note that this deep integration of languages allows for quick and volves checking all path conditions periodically to determine which
accurate creation of code/transformations, with fewer errors than rules they abstract. If a rule appears in no path condition, then it
a manual method. 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) informa-
tion allows the user to debug and understand the execution of the
rule, before further layers in the transformation are symbolically
executed.
5 DEBUGGING STAGE 3: REPORTING
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
Figure 5: Auto-complete during rule construction in the intention for the contract matches the verification result, and if not,
Meta-Programming System (MPS) editor. 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
Figure 5 demonstrates the creation of the Father2Man rule in where the contract is satisfied, and the second set (fail) is where the
the textual editor, where the rule’s MatchModel includes a Parent contract is not satisfied. The tool examines these sets and provides
element and a Family element. Note that the user is in the process the following information:
of adding an attribute to the Family, and the auto-complete pop-up
• rulessuccess - Rules found in all successful path conditions
indicates that the Family concept includes the name and lastName
• rulesfail - Rules found in all failed path conditions, and not
as valid attributes, as is specified in the input meta-model. Thus,
present in rulessuccess
all elements and attributes in the transformation and the contracts
• The precise elements and links that the contract requires
are typed according to the input and output languages, prevent-
from the set of rules rulessuccess
ing typos or inconsistencies before they can affect the verification
• The contract is also tested against a failed path condition
process.
– The elements and links that could not be found on this
path condition are reported
4 DEBUGGING STAGE 2: MONITORING – The user can use this information and a visualization of
The second stage of fault detection and localization in the SyVOLT the path condition to better understand the failure of the
is performed during the path condition generation process itself. contract, as in Figure 8 on the facing page
As the state-space for rule execution is constructed, the user is This comprehensive information allows the user to precisely
informed if a rule has not been symbolically executed4 . determine how the contract is succeeding or failing, and have as-
A rule not symbolically executing may indicate one of three surance that the result is as intended.
issues with the transformation which should be reported to the
user to investigate. The first case is where the required dependencies 5.1 Example
for the rule were not present in the transformation. This may occur
if a backward link specifies a dependency not satisfied by any other We will present the Neg_SchoolOrdFac contract in Figure 6a as an
rules. The second case is where the user has not indicated that a example for the information reported when a contract has counter-
rule should symbolically execute enough times, as specified by a example path conditions.
dependency analysis [10]. Note that for this contract we expect counter-examples to be
Finally, the third case is that there may be an undesired inter- found. This contract represents the statement ‘Every School in the
action between the transformation and its meta-model that has input model will produce an Ordinary Facility’. The rule dfacilities-
...OrdinaryFacility which performs this production is displayed in
4 Note that the work of Selim [12] defined this check as a series of rule reachability Figure 6b. However, the transformation also contains the dfacilities-
contracts. ...SpecialFacility rule, which matches over a School element with
successful path conditions. This is correct, as this rule must symbol-
ically 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
(a) An example contract for analysing success/failure results. 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 OrdinaryFa-
cility 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 Match10
Daughter2
Woman
Neighborhood2
Family3 Family14
District
(b) Rule needed for contract success. Apply1
daughters Match19 registeredIn
Figure 6: Contract and rule examples for result analysis.
Apply11
Child Neighborhood
a special Service to produce a Special Facility element. Thus, the
family goesTo schools
contract is expected to fail on path conditions that include the
d...SpecFacPerson
dfacilities...SpecialFacility rule.
School
For the Neg_SchoolOrdFac contract, as seen in Figure 7 on the
line marked a), the contract prover indicates that there are six path
students special
conditions where this contract holds, and three path conditions
where it does not.
Service Apply20
a) Name: Neg_SchoolOrdFac
Num Succeeded Path Conditions: 6 District
Num Failed Path Conditions: 3
b) Explaining contract result:
Good rules: (Rules in success set and not failure set) facilities
dfacilities...OrdinaryFacilityPerson
Bad rules: (Rules common to all in failure set)
dfacilities...SpecialFacilityPerson SpecialFacility
c) Contract requires elements from successful rules of type:
School members
OrdinaryFacility
d) Examining failed path condition: Woman
Daughter2Woman-Neigh2District-dfacilities...SpecialFacilityPerson
e) Elements of contract that fail on this path condition:
Could not find links of type: Figure 8: An unintuitive visualization of a path condition
OrdinaryFacility - trace_link - School that fails to satisfy the SchoolOrdFac contract.
Figure 7: Result analysis for the Neg_SchoolOrdFac contract.
5.1.1 Visualization. Figure 8 shows a visualization for the failed
path condition mentioned in part d) from Figure 7. This information
The contract result analysis indicates in the section marked is presented for the user to understand how the contract fails to
b) that the dfacilities...OrdinaryFacility rule is common to all the match on the path condition. However, it is difficult to comprehend
as it presents a technical, graph-based representation. In compar- lack sufficiently powerful debugging mechanisms, hindering de-
ison, Figure 2 on page 2 shows a hand-made (but more natural) velopment. For future work, we are interested in developing and
visualization for a different path condition. promoting reusable libraries for graph-matching visualization and
Another critique of this visualization is the inability to see the debugging in concert with the ModelVerse [16] and AToMPM [13]
structure which would allow the contract to be satisfied. For ex- projects.
ample, the Neg_SchoolOrdFac requires a School element connected Developing a systematic approach to developing contracts is also
to a Service element through an ordinary link, not the special link a goal of our research, requiring user experiments to determine how
shown in a pale yellow oval in the middle of Figure 8. users build contracts and what debugging information they require.
In future work, we intend to improve our visualization tech- As well, an important task is to transfer our contract verification and
niques by creating MPS plugins for visual viewers and editors of debugging techniques from the DSLTrans model transformation
transformations, contracts, and path conditions. language to others with more expressiveness.
6 RELATED WORK REFERENCES
[1] Banafsheh Azizi, Bahman Zamani, and Shekoufeh Kolahdouz-Rahimi. 2017. Con-
There is significant previous work in the general field of model tract verification of ETL transformations. In International Conference on Computer
transformation verification [6, 12]. Our present work focuses on and Knowledge Engineering. IEEE, 154–160.
[2] Bruno Barroca, Levi Lúcio, Vasco Amaral, Roberto Félix, and Vasco Sousa. 2011.
how to relate the result of contract verification to the transforma- DSLTrans: A Turing Incomplete Transformation Language. In International Con-
tion. ference on Software Language Engineering. Springer Berlin Heidelberg, 296–305.
The work of Burgueneo et al. [3] compares the elements in Tracts [3] Loli Burgueno, Javier Troya, Manuel Wimmer, and Antonio Vallecillo. 2015. Static
Fault Localization in Model Transformations. IEEE Transactions on Software
to the rules in the transformation. These tracts define a set of Engineering 41, 5 (2015), 490–506.
constraints on the source and target meta-models, a set of source- [4] Jesús Sánchez Cuadrado, Esther Guerra, and Juan de Lara. 2017. Static analysis
target constraints, and a tract test suite. The intention is to suggest of model transformations. IEEE Transactions on Software Engineering 43, 9 (2017),
868–897.
to the user which rules are causing constraints to fail by matching [5] Martin Fowler. 2008. Projectional Editing. https://martinfowler.com/bliki/
the classes and associations in the rules and constraints. ProjectionalEditing.html.
[6] Esther Guerra, Juan De Lara, Manuel Wimmer, Gerti Kappel, Angelika Kusel,
Cuadrado et al. [4] discuss a technique for statically analyzing Werner Retschitzegger, Johannes Schönböck, and Wieland. Schwinger. 2013.
ATL transformations. Their technique uses type inference and other Automated Verification of Model Transformations based on Visual Contracts.
analyses to determine potential problems in the transformation. Automated Software Engineering 20, 1 (2013), 5–46.
[7] Maris Jukšs, Clark Verbrugge, and Hans Vangheluwe. 2017. Transformations
From this, OCL constraints are generated and used to produce Debugging Transformations. In MDEbug: Debugging in Model-Driven Engineering
“witness” input models which precisely target the error. at International Conference on Model Driven Engineering Languages and Systems.
The thesis of Amstel [14] tackles the issue of evaluating the qual- [8] Levi Lúcio, Bentley Oakes, Cláudio Gomes, Gehan Selim, Juergen Dingel, James
Cordy, and Hans Vangheluwe. 2015. SyVOLT: Full Model Transformation Verifi-
ity of a model transformation. User studies are performed to rate cation Using Contracts.. In International Conference on Model Driven Engineering
transformations based on qualities such as re-usability, complete- Languages and Systems. 24–27.
[9] Levi Lúcio, Bentley Oakes, and Hans Vangheluwe. 2014. A technique for symboli-
ness, and conciseness. These qualitative facets of the transformation cally verifying properties of graph-based model transformations. Technical Report
are then correlated with quantitative metrics, such as the number SOCS-TR-2014.1. McGill University.
of rules or variables in the transformation, to provide a guide for [10] Bentley Oakes. 2018. A Symbolic Execution-Based Approach to Model Transforma-
tion Verification Using Structural Contracts. Ph.D. Dissertation. McGill University.
the transformation designer to build intuitive transformations. [11] Bentley Oakes, Javier Troya, Levi Lúcio, and Manuel Wimmer. 2016. Full contract
verification for ATL using symbolic execution. Software and Systems Modeling
(2016), 1–35.
7 CONCLUSION [12] Gehan Selim. 2015. Formal Verification of Graph-Based Model Transformations.
In this paper, we have discussed three analyses implemented in the Ph.D. Dissertation. Queen’s University.
[13] Eugene Syriani, Hans Vangheluwe, Raphael Mannadiar, Conner Hansen, Simon
SyVOLT tool to detect and report errors in the input transforma- Van Mierlo, and Huseyin Ergin. 2013. AToMPM: A web-based modeling environ-
tion and contract to the user so that these errors can be fixed and ment. In International Conference on Model Driven Engineering Languages and
Systems. 21–25.
successful verification can be achieved. [14] Marinus Franciscus van Amstel. 2012. Assessing and improving the quality of
The checks and analyses detailed in this paper arose organically model transformations. Ph.D. Dissertation. Technische Universiteit Eindhoven.
out of the development of the contract verification tool, and have [15] Simon Van Mierlo. 2015. Explicitly Modelling Model Debugging Environments..
In ACM Student Research Competition at the International Conference on Model
been quite successful in detecting errors as well as giving insight Driven Engineering Languages and Systems. 24–29.
into the behaviour of the contracts and transformations [10]. In [16] Simon Van Mierlo, Bruno Barroca, Hans Vangheluwe, Eugene Syriani, and
the future, we aim to improve these techniques to allow for more Thomas Kühne. 2014. Multi-level modelling in the Modelverse.. In International
Conference on Model Driven Engineering Languages and Systems. 83–92.
precise detection, visualization, and correction of errors. [17] Simon Van Mierlo, Yentl Van Tendeloo, Bart Meyers, and Hans Vangheluwe. 2017.
An especially crucial feature which is lacking in SyVOLT is the Domain-specific Modelling For Human–computer Interaction. In The Hand-
book of Formal Methods in Human-Computer Interaction. Springer International
visualization of transformation execution, both before and after the Publishing, 435–463.
application of rules as well as the actual matching and rewriting [18] Daniel Varró, Szilvia Varró-Gyapai, Hartmut Ehrig, Ulrike Prange, and Gabriele
steps of each rule [7, 15]. Implementing these techniques would Taentzer. 2006. Termination Analysis Of Model Transformations By Petri Nets.
In International Conference on Graph Transformation (2006), Vol. 4178. Springer,
assist with two key questions we encountered during the develop- 260–274.
ment of SyVOLT: why is this rule/contract not matching, when it [19] Markus Voelter, Arie van Deursen, Bernd Kolb, and Stephan Eberle. 2015. Using
should? and why is this rule/contract matching, when it shouldn’t? C language extensions for developing embedded software: A case study. In ACM
SIGPLAN Notices, Vol. 50. ACM, 655–674.
We note that these debugging questions are relatively simple,
and yet the igraph and T-Core libraries used in the SyVOLT tool