-We introduce SyVOLT, a plugin for the Eclipse development environment for the verification of structural pre/post-condition contracts on model transformations. The plugin allows the user to build transformations in our transformation language DSLTrans using a visual editor. The pre-/post-condition contracts to be proved on the transformation can also be built in a similar interface. Our contract proving process is exhaustive, meaning that if a contract is said to hold, then the contract will hold for all input models of a transformation. If the contract does not hold, then the counter-examples (i.e., input models) where the contract fails will be presented. Demo: https://www.youtube.com/watch?v=8PrR5RhPptY
Model transformations are at the center of model-driven
development, making pragmatic and usable tools for their
verification indispensable. In this paper we introduce SyVOLT
(Symbolic Verifier of mOdeL Transformations) [
Extensive work exists on the verification of different aspects
of model transformations [
The tool described in [
The distinguishing feature of SyVOLT is that, unlike the methods described above, our tool allows for contracts to be proved for all possible transformation executions, i.e., for all possible input models. However, we share with most tools described above the same implication idea: the pre-condition of a contract sets constraints on the input models to the transformation, and the post-condition defines constraints on the output model.
SyVOLT proves that pre-/post-condition contracts hold for
a model transformation. Such contracts establish relations
between patterns occurring in input and output models of a
model transformation. If a contract holds, a formal guarantee
exists that whenever a transformation’s input model contains
the pattern specified in the pre-condition of the contract,
the transformation’s output model will contain the pattern
specified in the contract’s post-condition. Contracts can
optionally include traceability relations between input and output
patterns. Our technique is exhaustive and input-independent,
in the sense that whenever a contract holds, it will hold for all
possible input models for that transformation. This is possible
because SyVOLT operates on specifications of out-place model
transformations, where unbounded loops and model element
deletions are not allowed. A discussion on the soundness and
completeness of our approach is provided in [
Eclipse is a popular development environment, as many
model transformation tools such as ATL, DSLTrans [
The proving process for a SyVOLT contract is fully automatic and all of the approach’s formal details are completely hidden from the user. Once the transformation and the contracts of interest are created, one command will start the property proving process. This process will automatically create all required artifacts (as detailed in Section III), run the process, and provide the results to the user within the Eclipse environment. This allows the user to continually stay within the Eclipse environment, where he or she develops the contracts and the model transformations.
When a contract does not hold for a model transformation, SyVOLT produces additional information for the user to pinpoint where the contract’s violation occurs. This information is in the form of the set of model transformation rules used to build a particular path condition for which the contract fails. A counter-example is any input model on which this set of rules would execute: e.g. the sample output in Figure 1 alerts the user that the contract motherFather fails when only the transformation’s mother and father rules execute.
Our technique shares its principles with symbolic
execution, a classically used technique for code verification. The
underlying idea entails building a finite representation of the
(infinite) set of computations that can be expressed by a model
transformation specification. In this context, each symbolic
execution – which in the context of our work we call a
path condition – is an overlapping combination of a subset
of the transformation’s rules. A path condition represents the
execution of the model transformation over any input model
those rules match on. Contracts of interest are proved on the
set of path conditions built for a model transformation, and are
extrapolated to the infinite set of the model transformation’s
computations through an abstraction relation [
The Atlas Transformation Language (ATL) [
We have some evidence that SyVOLT scales to
transformations of practical interest. In particular we have verified
contracts on DSLTrans transformations with up to over 60
rules, and ATL transformations with up to 13 rules [
The guiding principle of the Modelling, Design, and Simulation Lab is that all tools and processes should be explicitly modelled at an appropriate abstraction level. This practice ensures that software development effort is targeted at the problem’s essential complexity, while alleviating complexity induced by the computational platforms used.
SyVOLT’s codebase has been developed by applying these
principles. We have used available model-driven development
technology as much as possible, both to develop and as a part
of SyVOLT itself. In particular, we have made it such that the
DSLTrans transformations, the SyVOLT contracts, and path
conditions are all represented and treated as models by the
proof engine. Moreover, we have operationally encoded the
operations required by the algorithm for building a contract
proof as model transformations [
The following model-driven development tools have been used in SyVOLT’s development:
Himesis [
T-Core [
Eclipse Modelling Framework (EMF): SyVOLT makes use of EMF’s Ecore format for the XMI representation of DSLTrans transformations and SyVOLT’s contracts within the Eclipse editors.
Epsilon Generation Language (EGL): Converting Ecore models into Himesis models is achieved using EGL, a model-to-text transformation language.
Figure 2 shows the architecture of our tool, where squares containing gears (and annotated with number identifiers) represent computations and squares containing no gears (and annotated with letter identifiers) represent produced and consumed data. Two essential blocks are depicted: the graphical Eclipse front-end for user interaction and the proof engine back-end which implements the proving algorithm. The frontend and the back-end communicate in the following way: in the left-to-right direction, a number of artifacts (models and model transformations) are synthesized from the graphical representations of the DSLTrans transformations and of the SyVOLT contracts, and passed to the back-end. In the reverse direction, the proof result and counter-examples, if any, are passed from the proof engine to the front-end.
In what follows, we will briefly visit each computational component of SyVOLT to describe its function and the technologies employed in its development.
SyVOLT’s architectural components described in Figure 2 are orchestrated by an ANT script from within Eclipse. This script makes sure all components communicate and execute in the right order, and allows contract proof to run fully automatically at the push of a button.
The SyVolt contract editor, shown in Figure 3, is realized
by a set of Eclipse Graphical Modeling Framework (GMF) [
Internally, the graphical editor reads and write two models: the domain model and the graphical model. The graphical model can be seen as the realization of the concrete syntax by storing the coordinates and other visual information about the shapes that are shown in the graphical editor (Figure 3). In contrast, the Ecore domain model contains the abstract syntax: the essence of the elements that form the contracts and the propositional properties. The domain model is the artifact used when generating the models for the construction of the proof.
The translation of DSLTrans transformations and SyVOLT contracts into Himesis models and model transformation rules was achieved using the EGL. Specifically, two EGL model-totext transformations were used: one to generate the Himesis models representing a DSLTrans transformation (marked (a) in Figure 2); and another one to generate the T-Core model transformation rules necessary to prove SyVOLT contracts (marked (b) in Figure 2).
From the Ecore models of the DSLTrans model transformation and contracts of interest, the EGL transformations produce a number of Python classes that inherit from the Himesis library and that represent models and T-Core transformation rules. These classes will be subsequently loaded in memory and manipulated by the proof engine back-end.
Additional artifacts need to be generated for the property
proof algorithm to execute. These are the path condition
generation T-Core model transformations (marked (c) in Figure 2)
that are needed to perform the model manipulations for a set
of path conditions. These model transformation blocks allow
combining the rules of a DSLTrans model transformation into
a set of path conditions, as per the algorithm described in [
This additional model transformation generation step is achieved by the PyRamify component. PyRamify is a Python script that takes as input Himesis graphs representing the rules in the transformation. It produces T-Core matchers and rewriters for each rule. While matchers allow the contract prover to determine if and how rules might combine with a path condition under construction, rewriters combine the righthand side of a DSLTrans rule with that same path condition.
Currently, PyRamify is implemented as a Python script, as we were unable to implement automatic creation of higherorder artifacts (in our case, T-Core transformations) using graph-based model transformations. This indicates a need to further develop model-driven engineering tools that allow for the explicit manipulation of model transformations as models.
Once the required artifacts have been produced, the prover moves onto the path condition generation step. The path condition generation algorithm starts from the empty path condition, representing the case where no rules in the transformation have executed. Then, each rule in the DSLTrans model transformation under analysis is combined with the path conditions generated thus far, the using path condition generation T-Core matchers and rewriters (marked (c) in Figure 2). As each rule is considered, in the same order it would occur during the transformation’s execution, the set of path conditions will grow to represent all allowed rules combinations.
The contract prover component requires two inputs: the path conditions set, built by the path condition generator (marked (d) in Figure 2); the contract proof T-Core transformations (marked (b) in Figure 2). Pre/post condition contracts form an implication, which needs to be checked for each path condition. For a contract to hold on a DSLTrans model transformation, the contract’s implication should hold for every path condition generated for that model transformation. Thus, for each submodel of the path condition that is isomorphic to the pre-condition’s model, the algorithm will try to find a submodel of the path condition that is isomorphic to the postcondition’s model. T-Core matchers from the contract proof T-Core transformations allow checking the existence of these relations between the contract and the post-condition.
The authors are researchers working for the NECSIS project, funded by the Automotive Partnership Canada.