Mathias Hülsbusch and Barbara König and Arend Rensink and Maria Semenyak and Christian Soltenborn and Heike Wehrheim: Full Semantics Preservation in Model Transformation - A Comparison of Proof Techniques. In Proceedings of the 8th International Conference on Integrated Formal Methods (IFM 2010). Springer (Berlin/Heidelberg), LNCS, vol. 6396, pp. 183--198 (2010)
Show Bibtex | Show Abstract | DOI

@inproceedings{HKRSSW2010, author = {Mathias Hülsbusch and Barbara König and Arend Rensink and Maria Semenyak and Christian Soltenborn and Heike Wehrheim}, title = {Full Semantics Preservation in Model Transformation - A Comparison of Proof Techniques}, booktitle = {Proceedings of the 8th International Conference on Integrated Formal Methods (IFM 2010)}, year = {2010}, volume = {6396}, series = {LNCS}, pages = {183--198}, address = {Berlin/Heidelberg}, publisher = {Springer} }

Model transformation is a prime technique in modern, model-driven software design. One of the most challenging issues is to show that the semantics of the models is not affected by the transformation. So far, there is hardly any research into this issue, in particular in those cases where the source and target languages are different. In this paper, we are using two different state-of-the-art proof techniques (explicit bisimulation construction versus borrowed contexts) to show bisimilarity preservation of a given model transformation between two simple (self-defined) languages, both of which are equipped with a graph transformation-based operational semantics. The contrast between these proof techniques is interesting because they are based on different model transformation strategies: triple graph grammars versus in situ transformation. We proceed to compare the proofs and discuss scalability to a more realistic setting.

Gregor Engels and Anneke Kleppe and Arend Rensink and Maria Semenyak and Christian Soltenborn and Heike Wehrheim: From UML Activities to TAAL - Towards Behaviour-Preserving Model Transformations. In Proceedings of the 4th European Conference on Model Driven Architecture - Foundations and Applications (ECMDA-FA 2008), Berlin (Germany). Springer (Berlin/Heidelberg), LNCS, vol. 5095, pp. 95--109 (2008)
Show Bibtex | Show Abstract | DOI

@inproceedings{Engels08-2, author = {Gregor Engels and Anneke Kleppe and Arend Rensink and Maria Semenyak and Christian Soltenborn and Heike Wehrheim}, title = {From UML Activities to TAAL - Towards Behaviour-Preserving Model Transformations}, booktitle = {Proceedings of the 4th European Conference on Model Driven Architecture - Foundations and Applications (ECMDA-FA 2008), Berlin (Germany)}, year = {2008}, volume = {5095}, series = {LNCS}, pages = {95--109}, address = {Berlin/Heidelberg}, month = {July}, publisher = {Springer} }

Model transformations support a model-driven design by providing an automatic translation of abstract models into more concrete ones, and eventually program code. Crucial to a successful application of model transformations is their correctness, in the sense that the meaning (semantics) of the models is preserved. This is especially important if the models not only describe the structure but also the intended behaviour of the systems. Reasoning about and showing correctness is, however, often impossible as the source and target models typically lack a precise definition of their semantics. In this paper, we take a first step towards provably correct behavioural model transformations. In particular, we develop transformations from UML Activities (which are visual models) to programs in TAAL, which is a textual Java-like programming language. Both languages come equipped with formal behavioural semantics, which, moreover, have the same semantic domain. This sets the stage for showing correctness, which in this case comes down to showing that the behaviour of every (well-formed) UML Activity coincides with that of the corresponding TAAL program, in a well-defined sense.

Mathias Hülsbusch and Barbara König and Arend Rensink and Maria Semenyak and Christian Soltenborn and Heike Wehrheim: Full Semantics Preservation in Model Transformation - A Comparison of Proof Techniques. techreportCentre for Telematics and Information Technology of the University of Twente (Enschede, The Netherlands) (2010)
Show Bibtex | Show Abstract

@techreport{HKRSSW2010TR, author = {Mathias Hülsbusch and Barbara König and Arend Rensink and Maria Semenyak and Christian Soltenborn and Heike Wehrheim}, title = {Full Semantics Preservation in Model Transformation - A Comparison of Proof Techniques}, institution = {Centre for Telematics and Information Technology of the University of Twente}, year = {2010}, type = {techreport}, address = {Enschede, The Netherlands} }

Model transformation is a prime technique in modern, model-driven software design. One of the most challenging issues is to show that the semantics of the models is not affected by the transformation. So far, there is hardly any research into this issue, in particular in those cases where the source and target languages are different. In this paper, we are using two different state-of-the-art proof techniques (explicit bisimulation construction versus borrowed contexts) to show bisimilarity preservation of a given model transformation between two simple (self-defined) languages, both of which are equipped with a graph transformation-based operational semantics. The contrast between these proof techniques is interesting because they are based on different model transformation strategies: triple graph grammars versus in situ transformation. We proceed to compare the proofs and discuss scalability to a more realistic setting.