A Theory of Least Change for Bidirectional Transformations
Lead Research Organisation:
University of Edinburgh
Department Name: Sch of Informatics
Abstract
A bidirectional transformation is a means of maintaining consistency between multiple information sources: when one source is edited, the others may need updating to restore consistency. There are many domains in which bidirectional transformations are needed. Currently, the best-known of these is model-driven development. Model-driven development is the approach to developing software in which models - specialised descriptions of only certain aspects of the software to be built - are important artefacts in the development. Some or all code may be generated from models, rather than written by hand. Different experts work on different models, adapted to their needs, each recording their decisions in their own model. In order to end up with a correct system, the models need to be kept consistent; when one developer changes one model, another model may need to be changed to match, and vice versa. Another current application is the "view update" problem in databases (updating source tables after edits to view tables). Potential applications include integrating different electronic health records, maintaining consistency between a high-level systems biology model and a more detailed model of some aspect, providing user-friendly access to machine-oriented data representation, automating the coevolution of a program with its proof of correctness, etc.
A bidirectional transformation can be implemented in terms of several unidirectional restoring functions, one per source; but this duplicates information (for example, information about the structure of the models being related appears in every function), wasting effort and risking inconsistencies. Bidirectional transformation languages allow one to describe the consistency relationship and the restoring functions with a single declarative specification. A good bidirectional transformation language should support the developer of the transformation by not allowing the developer to write nonsense: when a transformation is considered correct according to the language, it should obey basic sanity properties.
Various natural properties of bidirectional transformations are now well understood; in particular, "correctness" (that the bidirectional transformation does actually restore consistency) and "hippocraticness" (that if an edited source remains consistent, then the bidirectional transformation makes no changes). What is much less well understood, and what we will study in this project, is the "principle of least change" (that a bidirectional transformation should not make unnecessary changes when it enforces consistency).
Our hypotheses are: (i) that this Principle of Least Change can be precisely and productively captured; (ii) that our understanding of the Principle will benefit from work on "provenance" in databases - provenance involves building and using a record of which outputs depend on which inputs, and how they do so; and (iii) that this will lead to a theory of "alignment" - matching of parts - for non-free datatypes such as associative lists and graphs. Graphs are an especially important datatype, because they are ubiquitous in software engineering. In particular, the models in model-driven development are often types of graph, such as class diagrams and statecharts.
This project will work on the mathematical foundations of bidirectional transformations. The reason for doing this is in order that a better understanding of the Principle of Least Change will, in future, contribute to more usable and more reliable model-driven engineering tools, supporting efficient and correct software development, even in the face of continuous change. It will thus enable software developers to combine the advantages of model-driven development with those of agile methods. By enabling better languages and tools to be developed, it will also make practical the use of bidirectional transformations in a wide range of other application areas.
A bidirectional transformation can be implemented in terms of several unidirectional restoring functions, one per source; but this duplicates information (for example, information about the structure of the models being related appears in every function), wasting effort and risking inconsistencies. Bidirectional transformation languages allow one to describe the consistency relationship and the restoring functions with a single declarative specification. A good bidirectional transformation language should support the developer of the transformation by not allowing the developer to write nonsense: when a transformation is considered correct according to the language, it should obey basic sanity properties.
Various natural properties of bidirectional transformations are now well understood; in particular, "correctness" (that the bidirectional transformation does actually restore consistency) and "hippocraticness" (that if an edited source remains consistent, then the bidirectional transformation makes no changes). What is much less well understood, and what we will study in this project, is the "principle of least change" (that a bidirectional transformation should not make unnecessary changes when it enforces consistency).
Our hypotheses are: (i) that this Principle of Least Change can be precisely and productively captured; (ii) that our understanding of the Principle will benefit from work on "provenance" in databases - provenance involves building and using a record of which outputs depend on which inputs, and how they do so; and (iii) that this will lead to a theory of "alignment" - matching of parts - for non-free datatypes such as associative lists and graphs. Graphs are an especially important datatype, because they are ubiquitous in software engineering. In particular, the models in model-driven development are often types of graph, such as class diagrams and statecharts.
This project will work on the mathematical foundations of bidirectional transformations. The reason for doing this is in order that a better understanding of the Principle of Least Change will, in future, contribute to more usable and more reliable model-driven engineering tools, supporting efficient and correct software development, even in the face of continuous change. It will thus enable software developers to combine the advantages of model-driven development with those of agile methods. By enabling better languages and tools to be developed, it will also make practical the use of bidirectional transformations in a wide range of other application areas.
Planned Impact
Outside academia, the most obvious direct beneficiaries will be software engineers and tool developers working within the model-driven development paradigm. They represent many application domains, including embedded systems, automotive and aeronautical engineering, health informatics, public-sector IT, and finance; see http://www.omg.org/mda/products_success.htm for a portfolio of MDD success stories.
Currently model-driven development is hard to reconcile with agile development, the other important trend in modern software engineering. This is because the lack of dependable bidirectional transformation tools makes it impractical to work with several models any of which may need to change; instead, users are forced to finalise one model before using it to generate another model or code which may itself need to be worked on. Our work will enable the development of better tools and languages for bidirectional transformations, which in turn will let changes be made in the most appropriate model and automatically rolled out to other models as necessary. Thus, in addition to benefitting developers already using the MDD paradigm, our research should benefit developers who currently do not use it because of the difficulty of making it sufficiently agile.
These groups will benefit from results leading to more useful and more robust tools for software development, and especially tools that reliably automate the tedious and error-prone tasks that follow as software requirements and design decisions evolve over time. The essence of these tasks is that they restore consistency between different system perspectives when changes are made from one perspective, and our research is about precisely this reconciliation process.
Indirectly, all of society will benefit from more dependable software systems. All of us rely on a daily basis on software infrastructure - for banking, communications, travel, power, shopping, and many other necessities - and we all experience software failures that cause frustration and inconvenience at best, and financial loss and threats to safety at worst. Ultimately, better tools for software development will lead to better quality of life in the digital world.
Currently model-driven development is hard to reconcile with agile development, the other important trend in modern software engineering. This is because the lack of dependable bidirectional transformation tools makes it impractical to work with several models any of which may need to change; instead, users are forced to finalise one model before using it to generate another model or code which may itself need to be worked on. Our work will enable the development of better tools and languages for bidirectional transformations, which in turn will let changes be made in the most appropriate model and automatically rolled out to other models as necessary. Thus, in addition to benefitting developers already using the MDD paradigm, our research should benefit developers who currently do not use it because of the difficulty of making it sufficiently agile.
These groups will benefit from results leading to more useful and more robust tools for software development, and especially tools that reliably automate the tedious and error-prone tasks that follow as software requirements and design decisions evolve over time. The essence of these tasks is that they restore consistency between different system perspectives when changes are made from one perspective, and our research is about precisely this reconciliation process.
Indirectly, all of society will benefit from more dependable software systems. All of us rely on a daily basis on software infrastructure - for banking, communications, travel, power, shopping, and many other necessities - and we all experience software failures that cause frustration and inconvenience at best, and financial loss and threats to safety at worst. Ultimately, better tools for software development will lead to better quality of life in the digital world.
Organisations
Publications
Abou-Saleh F
(2018)
Bidirectional Transformations
Abou-Saleh, F
(2015)
Reflections on monadic lenses
Abou-Saleh, F
(2015)
Coalgebraic Aspects of Bidirectional Computation
Cheney J
(2014)
Database Queries that Explain their Work
Cheney J
(2017)
On principles of Least Change and Least Surprise for bidirectional transformations.
in The Journal of Object Technology
Cheney, J
(2014)
Entangled State Monads
in 2014 workshop on Bidirectional Transformations (BX 2014)
Cheney, J
(2014)
Towards a Repository of Bx Examples
in 2014 workshop on Bidirectional Transformations (BX 2014)
| Description | We have discovered that the technical device called monads can be useful to describe, formally, correctness properties for the type of software artefact we're studying (bidirectional transformations). These are particularly useful in that, we showed, they can be used to reason about situations in which the bidirectional transformation needs to have so-called effects, such as interacting with the user. We have developed several notions of least surprise; that is, properties that can help such bidirectional transformations to have behaviour that will be useful and not disruptive to their users. We showed why the most obvious version of such a property does not always give the bidirectional transformation the best behaviour, and we investigated alternatives deriving from mathematical analysis. We have developed the concept of subspace pairs, which help us to describe situations in which a bidirectional transformation may have very safe, predictable behaviour under some circumstances, so that the user could feel confident in using it without checking under those circumstances, while under other circumstances it may be necessary for the user to check whether the transformation's behaviour is what is wanted. Unexpectedly, we found a close relationship between bidirectional transformations and a well-known relationship between concurrent processes, viz bisimulation. In a nutshell, bidirectional transformations are proof-relevant bisimulations; here proof-relevant means that it does not only matter that things are related, but precisely how they are related. The connections we developed between bidirectional transformations and monads on the one hand, and bisimulations on the other, enabled us to understand better how bidirectional compositions can be composed: this is an important issue for using them in computing contexts, and something that had difficult up till now. We found several areas that need more investigation than we could do on this grant: for example, we found that witness structures, which help to demonstrate whether data sources are consistent, can be described using dependent types; we now hypothesise that it will be important for a bidirectional transformation to explain its actions, and we think an approach via dependent types may help us to do this. |
| Exploitation Route | Our findings will help people who design bidirectional transformation languages (including, we hope, ourselves) to make choices that will make the languages easy to use to write bidirectional transformations that will do what users want without confusing or surprising them. Such languages may be embedded in a general purpose programming language such as Haskell, making use of our monad-based work, or may be free-standing languages. This is one ingredient in an ongoing agenda of helping model-driven development to be more generally applicable in an agile way, thereby making it feasible to develop high quality software faster and more cheaply. |
| Sectors | Digital/Communication/Information Technologies (including Software) |
| URL | http://groups.inf.ed.ac.uk/bx/ |
| Description | This is primarily a theoretical, foundational project. - We have established the Bx Example Repository, http://bx-community.wikidot.com/examples:home , which is a resource for the whole community interested in bidirectional transformations, including both theoreticians and practitioners. It records and discusses interesting examples of bidirectional transformations, some theoretical, some industrial in origin. - We held a Summer School on Bidirectional Transformations in July 2016, which was attended by both academics and practitioners, including several engineers from Google. A book resulting from the summer school is available from Springer. |
| First Year Of Impact | 2016 |
| Sector | Digital/Communication/Information Technologies (including Software) |