Bidirectional model transformations (bx) are mechanisms for automatically restoring consistency between multiple concurrently modified models. They are, however, challenging to implement; many model transformation languages not supporting them at all. In this paper, we propose an approach for automatically obtaining the consistency guarantees of bx without the complexities of a bx language. First, we show how to “fake” true bidirectionality using pairs of unidirectional transformations and inter-model consistency constraints in Epsilon. Then, we propose to automatically verify that these transformations are consistency preserving-thus indistinguishable from true bx-by defining translations to graph rewrite rules and nested conditions, and leveraging recent proof calculi for graph transformation verification.
Model transformations are operations for automatically translating models conforming to one language (i.e. a metamodel) into models conforming to another, in a way that maintains some sense of consistency between them. At their most basic, model transformations are unidirectional: given a source model (e.g. some high-level yet usermodifiable view of a system), they generate a target model (perhaps a lower-level view, such as code) whose data is “consistent” with the source, in a sense that is either left implicit, or captured by textual constraints or an inter-model consistency relation.
Many situations arise where the source and target models may both be modified by
users in concurrent engineering activities, e.g. when integrating parts of systems that
are modelled separately but must remain consistent. Bidirectional model
transformations (bx) [
While this advantage is certainly an attractive one, bx are challenging to implement
on account of the inherent complexity that they must encode. Model transformation
languages supporting them often do so with conditions: some require that bx are bijective
(e.g. BOTL [
A trade-off between the benefits (but complexity) of bx and the practicality (but
possible incoherence) of unidirectional transformations can be achieved in Epsilon, a
platform of interoperable model management languages. Epsilon has languages
supporting the specification of unidirectional transformations in either a rule-based (ETL),
update-in-place (EWL), or operational (EOL) [
Although this process gives us a means of checking consistency and automatically triggering a transformation to restore it, we lack the important guarantee that bx give us: the compatibility of the transformations. It might be the case that after the execution of one transformation, the other does not actually restore consistency, leading to further EVL violations. How do we check for, and maintain, compatibility?
We aim to address this shortcoming and obtain the guarantees of bx without the need
for bx languages. Instead, we will use rigorous proof techniques to verify that faked bx
are consistency preserving, and thus indistinguishable to users from true bx. To this end,
we propose to apply techniques from graph transformation verification. Given a faked
bx in Epsilon, we will model the unidirectional transformations as graph transformation
rules, and EVL constraints as nested graph conditions [
The overarching goal of our work is to achieve the ideal that Stevens [
Example bx in Epsilon: Class Diagrams to Databases To illustrate the ideas of our proposal, we recall a common model transformation problem that concerns the consistency of class diagram and relational database models (CD2RDBM). Class diagram models conform to a simple language describing familgg gg iar object-oriented concepts (e.g. classes, attributes, relationships), whereas relational database models conform to a language describing how databases are constructed (e.g. tables, columns, primary keys). Here, consistency is defined in terms of a correspondence between the data in the models, e.g. every table n corresponds to a class n, and every column m corresponds to an attribute m. Figure 1 contains two simple models that are consistent in this sense (we omit the metamodels for lack of space). tbmaeboaldeUbeslls)eecwrtosohncoislrfisestttaehmtneeacnimyne.twoaAdinceblilasnxsgsswheinsootuu(eollrdd-r fneaatmu:reCe=la"sussers" feature npakemy:eTa=b"ulesers" column be well suited for this: upon the :Attribute :Attribute :Column :Column cbrleea),tiaontaobflea (nreewsp.clcalsasss()resshpo.utlad- npakemye==T"riude" nampeke=y"=usFearnlsaeme" name = "id" name = "username" be created with the same name Fig. 1. Two consistent CD and RDB models to restore consistency. We can fake this simple bx in Epsilon with a pair of unidirectional transformations (one for updating the class diagram model, one for updating the relational database) and a set of EVL constraints. For the former, we can use the Epsilon Wizard Language (EWL) to define a pair of update-in-place transformations, AddClass and AddTable (for simplicity, here we assume the new class/table name newName to be pre-determined and unique, but Epsilon does support the capturing and sharing of such data between wizards). wizard AddClass f do f var c : new Class ; c . name = newName ; self . Class . all . first ( ) . contents . add ( c ) ; wizard AddTable f do f var table : new Table ; table . name = newName ; self . Table . all . first ( ) . contents . add ( table ) ; Using the Epsilon Validation Language (EVL), we express the relevant notion of intermodel consistency: that for every class n, there exists a table named n (and vice versa). If one of the constraints is violated, Epsilon can automatically trigger the relevant transformation to attempt to restore consistency. For example, after executing the transformation AddClass, the constraint TableExists will be violated, indicating that the transformation AddTable should be executed to restore consistency. context OO ! Class f constraint TableExists f check : DB ! Table . all . select ( t j t . name = self . name ) . size ( ) > 0 context DB ! Table f constraint ClassExists f check : OO ! Class . all . select ( c j c . name
= self . name ) . size ( ) > 0 gg gg This example of a bx, “faked” in Epsilon, is a deliberately simple one chosen to illustrate the concepts. Note even that the CD2RDBM problem can lead to more interesting (i.e. less symmetric) bx, e.g. manipulating inheritance in the class model. 3
Checking Compatibility of the Transformations The critical difference between the “faked” bx in the previous section and a true bx is the absence of guarantees about the compatibility of the transformations: upon the violation of TableExists, for example, does the execution of AddTable actually restore consistency? For this simple example, a manual inspection will quickly confirm that the transformations are indeed compatible in this sense. But what about more intricate bx? And what about bx that evolve and change over time? For the Epsilon-based approach to be a convincing alternative to a bx language, it is imperative that the compatibility (or not) of the transformations can be checked, and—crucially—that this can be done in a simple and automatic way. To this end, we propose to leverage and adapt some recent developments in the verification of graph transformations.
Graph transformation is a computation abstraction: the state of a computation is
represented as a graph, and the computational steps as applications of rules (i.e. akin to
string rewriting in Chomsky grammars, but lifted to graphs). Modelling a problem using
graph transformation brings an immediate benefit in visualisation, but also an important
one in terms of semantics: the abstraction has a well-developed algebraic theory that
can be used for formal reasoning. This has been exploited to facilitate the verification
of graph transformation systems, i.e. calculi for systematically proving specifications
about graph properties before and after any execution of some given rules.
Furthermore, such calculi have been generalised to graph programs [
Habel et al. [
We aim to exploit this work to check the compatibility of transformations in the Epsilon approach to bx. In particular, we are developing automatic translations of EWL transformations to graph programs (denoted PS ; PT for the source and target updates respectively), and translations from EVL constraints to nested conditions (denoted evl). Then, the task of checking compatibility of the transformations, as shown in Figure 2, reduces to proving the specifications fevlg PS ; PT fevlg and fevlg PT ; PS fevlg (here we assume the input graphs to be disjoint unions of the two models). Intuitively: if the models are consistent to start with, and executing the transformations in either order maintains consistency, then the transformations are compatible.
The technical challenges of the process fall into two main parts: computing the
abstractions, and checking validity. Defining translations for the former requires care:
we need to determine how much of the EWL language can be handled, we need to
ensure that the graph-based semantics we abstract them to is “correct”, and we need to
adapt the proof technology to our specific needs. The work in [
PS PT evl
WLP construction
evl ) Wlp(PS; PT , evl) FO validity
evl ) Wlp(PT ; PS, evl)
FO validity
no / loop ??
no / loop ??
yes
yes
compatible
metamodels). Similar concerns must be addressed for the translations of EVL to nested
conditions (we can take inspiration from recent work on such translations for core OCL
[
Our example bx for the CD2RDBM problem is easily translated into graph programs and nested conditions, as given in Figure 3. The programs PS ; PT are the individual rules creating respectively a class or table node labelled newName (here, ; denotes the empty graph, indicating that the rules can be applied without first matching any structure, i.e. unconditionally). The nested condition evl, given on the right, expresses that for every class (resp. table) node, there is a table (resp. class) node with the same name (we do not define here a formal interpretation, but note that x; y are variables, and that the numbers indicate when nodes are the same down the nesting of the formula). Were the weakest liberal preconditions to be constructed, we would find:
Wlp(PS ; PT ; evl)
Wlp(PT ; PS ; evl) evl: Since evl ) evl is clearly valid, both fevlg PS ; PT fevlg and fevlg PT ; PS fevlg must hold, and—assuming correctness of the abstractions—the original EWL transformations are therefore compatible with respect to the EVL constraints. ; ; ) )
:Class name = newName
:Table name = newName
:Class :Class 8 ( name = x , 9 ( name = x
1 :Table ^ 8 ( name = y 2
1
:Table
, 9 ( name = y
:Table
name = x
:Class
name = y
After further exploring the CD2RDBM example, we will identify a selection of bx case
studies—from the community repository [