The general problem of maintaining consistency between two related sources of information is recurrent across computer science, surfacing in communities as diverse as database management (e.g. the construction of updatable views for relational databases), programming languages (e.g. invertible computations), and model-driven engineering (e.g. synchronising views of software models). The various mechanisms constructed for solving these problems and maintaining consistency have, collectively, become known as bidirectional transformations (BX), and the last decade has seen several cross-discipline initiatives to study the common challenges and underpinnings; most notably the GRACE-BX meeting in 2008 and the BX wiki and workshop series.
Some months ago (and almost certainly in one of York’s fine pubs), Richard Paige, Mike Dodds, Arend Rensink and I turned our attention to the buzz surrounding BX in one particular subcommunity: that of model transformations. This is a community concerned with making models first-class engineering artefacts, manipulated by automatic consistency-preserving translations (i.e. model transformations). Intuitively, these models could be system views at different levels of abstraction (perhaps all the way down to code), with model transformations the means of linking them, and consistency a property satisfied if all the models actually are views of the same system. These transformations are typically unidirectional, in the sense that they can translate a source model S into a target model T – but not a T into an S. It’s often quite fine that a transformation cannot do this; the reverse direction is not necessarily interesting or useful (who modifies compiled code and expects the source files to be updated?). But often it is: for example, in integrating separately-modelled systems that must be consistent; or in the database view problem, where low-level users are modifying restricted views of a database, while administrators are concurrently querying and modifying a model of the entire thing.
Bidirectional model transformations (BX) that solve such problems simultaneously describe transformations in both directions – from S to T and T to S – and are consistency-preserving by construction. This property makes BX scientifically fascinating (for myself and many others), but whether they are a productive means of solving problems in model-driven engineering is quite another issue. The inherent complexity that BX must encode make them very difficult to implement; so much so, that many transformation languages do not support them at all, or do so with strings attached and severe restrictions (e.g. bijective transformations only). Perhaps worse, while the QVT-R language (part of an OMG standard) does support them, it does so with an ambiguous semantics and limited tool support.
At some point, one starts to ask: does the difficulty in expressing and executing BX actually outweigh the practical benefits arising from their consistency guarantees? And if engineers aren’t writing BX to solve the problems that they are intended to solve… what are they writing instead? For the latter question, the answer is typically “pairs of unidirectional transformations”. These are certainly easier to write than BX, and a pair of transformations could still maintain consistency; but the emphasis here is on could – we lack the guarantee. Arend, Mike, Richard and I, however, began to wonder whether this could be automatically checked. And we were not alone:
“If a framework existed in which it were possible to write the directions of a transformation separately and then check, easily, that they were coherent, we might be able to have the best of both worlds.” — Perdita Stevens
We have come to believe that the Epsilon family of model management languages has all of the ingredients necessary to facilitate such checks. BX can be “faked” in Epsilon as pairs of update-in-place transformations that separately manipulate the source and target models, with an inter-model constraint expressing precisely what it means for the two models to be consistent. The idea is that immediately after an update of the source (resp. target) model, the constraint is violated, and the corresponding update of the target (resp. source) model is triggered. We claim that a fake BX in this sense is indistinguishable from a true BX, if it can be proven that the constraint is invariant under executions of the transformations in both directions. Furthermore, we conjecture that we will be able to check this, automatically, using rigorous proof techniques adapted from graph rewriting.
We explored these ideas further in our short paper, Towards Rigorously Faking Bidirectional Model Transformations, presented by Richard on our behalf at AMT 2014. We applied them successfully to a small conceptual example, but whether they work more generally, and prove to be a practical alternative to true BX, remains to be evaluated. We are certainly on the case, but would appreciate your thoughts, suggestions, and criticisms in the meantime.