Skip to main content
SpringerLink
Log in

Showing Full Semantics Preservation in Model Transformation - A Comparison of Techniques

  • Conference paper
Integrated Formal Methods (IFM 2010)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 6396))

Included in the following conference series:

Abstract

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.

Partially supported by DFG project Behaviour-GT.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Barbosa, P.E.S., Ramalho, F., de Figueiredo, J.C.A., dos, S., Junior, A.D., Costa, A., Gomes, L.: Checking semantics equivalence of MDA transformations in concurrent systems. The Journal of Universal Computer Science 11, 2196–2224 (2009)

    Google Scholar 

  2. Baresi, L., Ehrig, K., Heckel, R.: Verification of model transformations: A case study with BPEL. In: Montanari, U., Sannella, D., Bruni, R. (eds.) TGC 2006. LNCS, vol. 4661, pp. 183–199. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  3. Bisztray, D., Heckel, R., Ehrig, H.: Verification of architectural refactorings by rule extraction. In: Fiadeiro, J.L., Inverardi, P. (eds.) FASE 2008. LNCS, vol. 4961, pp. 347–361. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  4. Ehrig, H., König, B.: Deriving bisimulation congruences in the DPO approach to graph rewriting with borrowed contexts. MSCS 16(6), 1133–1163 (2006)

    MathSciNet  MATH  Google Scholar 

  5. Engels, G., Kleppe, A., Rensink, A., Semenyak, M., Soltenborn, C., Wehrheim, H.: From UML Activities to TAAL - Towards Behaviour-Preserving Model Transformations. In: Schieferdecker, I., Hartman, A. (eds.) ECMDA-FA 2008. LNCS, vol. 5095, pp. 94–109. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  6. Giese, H., Glesner, S., Leitner, J., Schäfer, W., Wagner, R.: Towards verified model transformations. In: Workshop on Model Development, Validation and Verification, pp. 78–93 (2006)

    Google Scholar 

  7. Gorp, P.V., Stenten, H., Mens, T., Demeyer, S.: Towards automating source-consistent UML refactorings. In: Stevens, P., Whittle, J., Booch, G. (eds.) UML 2003. LNCS, vol. 2863, pp. 144–158. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  8. Hausmann, J.: Dynamic Meta Modeling: A Semantics Description Technique for Visual Modeling Languages. PhD thesis, University of Paderborn (2005)

    Google Scholar 

  9. Hirschkoff, D.: On the benefits of using the up-to techniques for bisimulation verification. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 285–299. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  10. Hülsbusch, M., König, B., Rensink, A., Semenyak, M., Soltenborn, C., Wehrheim, H.: Full semantics preservation in model transformation – a comparison of proof techniques. Technical Report TR-CTIT-10-09, CTIT, University of Twente (2010)

    Google Scholar 

  11. Kastenberg, H., Kleppe, A., Rensink, A.: Defining object-oriented execution semantics using graph transformations. In: Gorrieri, R., Wehrheim, H. (eds.) FMOODS 2006. LNCS, vol. 4037, pp. 186–201. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  12. Königs, A.: Model transformation with triple graph grammars. In: Workshop on Model Transformations in Practice (2005)

    Google Scholar 

  13. Küster, J., Gschwind, T., Zimmermann, O.: Incremental development of model transformation chains using automated testing. In: Schürr, A., Selic, B. (eds.) MODELS 2009. LNCS, vol. 5795, pp. 733–747. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  14. Leifer, J., Milner, R.: Deriving bisimulation congruences for reactive systems. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, pp. 243–258. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  15. McComb, T., Smith, G.: Architectural Design in Object-Z. In: ASWEC 2004, pp. 77–86. IEEE, Los Alamitos (2004)

    Google Scholar 

  16. Mens, T., Tourwé, T.: A survey of software refactoring. IEEE Trans. Software Eng. 30(2), 126–139 (2004)

    Article  Google Scholar 

  17. Narayanan, A., Karsai, G.: Towards verifying model transformations. In: GT-VMT 2006. ENTCS, vol. 211, pp. 185–194 (2006)

    Google Scholar 

  18. Necula, G.: Translation validation for an optimizing compiler. In: PLDI 2000. SIGPlan Notices, vol. 35, pp. 83–95. ACM, New York (2000)

    Google Scholar 

  19. Object Management Group: OMG Unified Modeling Language (OMG UML) – Superstructure, Version 2.2 (2009), http://www.omg.org/docs/formal/09-02-02.pdf

  20. Pérez, J., Crespo, Y.: Exploring a method to detect behaviour-preserving evolution using graph transformation. In: Third International ERCIM Workshop on Software Evolution, pp. 114–122 (2007)

    Google Scholar 

  21. Rangel, G., König, B., Ehrig, H.: Deriving bisimulation congruences in the presence of negative application conditions. In: Amadio, R.M. (ed.) FOSSACS 2008. LNCS, vol. 4962, pp. 413–427. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  22. Rangel, G., Lambers, L., König, B., Ehrig, H., Baldan, P.: Behavior preservation in model refactoring using DPO transformations with borrowed contexts. In: Ehrig, H., Heckel, R., Rozenberg, G., Taentzer, G. (eds.) ICGT 2008. LNCS, vol. 5214, pp. 242–256. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  23. Ruhroth, T., Wehrheim, H.: Refactoring object-oriented specifications with data and processes. In: Bonsangue, M.M., Johnsen, E.B. (eds.) FMOODS 2007. LNCS, vol. 4468, pp. 236–251. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  24. Schürr, A., Klar, F.: 15 years of triple graph grammars. In: Ehrig, H., Heckel, R., Rozenberg, G., Taentzer, G. (eds.) ICGT 2008. LNCS, vol. 5214, pp. 411–425. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  25. van Glabbeek, R.: The linear time - branching time spectrum II. In: Best, E. (ed.) CONCUR 1993. LNCS, vol. 715, pp. 66–81. Springer, Heidelberg (1993)

    Google Scholar 

  26. van Kempen, M., Chaudron, M., Kourie, D., Boake, A.: Towards proving preservation of behaviour of refactoring of UML models. In: SAICSIT 2005, pp. 252–259 (2005)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Abteilung für Informatik und Angewandte Kognitionswissenschaft, Universität Duisburg-Essen, Germany

    Mathias Hülsbusch & Barbara König

  2. Department of Computer Science, University of Twente, The Netherlands

    Arend Rensink

  3. Institut für Informatik, Universität Paderborn, Germany

    Maria Semenyak, Christian Soltenborn & Heike Wehrheim

Authors
  1. Mathias Hülsbusch
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Barbara König
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Arend Rensink
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Maria Semenyak
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Christian Soltenborn
    View author publications

    You can also search for this author in PubMed Google Scholar

  6. Heike Wehrheim
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. INRIA Nancy-Grand Est & LORIA, Bâtiment B, équipe MOSEL, 615 rue du Jardin Botanique, 54602, Villers-lès-Nancy cédex, France

    Dominique Méry  & Stephan Merz  & 

Rights and permissions

Reprints and permissions

Copyright information

© 2010 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Hülsbusch, M., König, B., Rensink, A., Semenyak, M., Soltenborn, C., Wehrheim, H. (2010). Showing Full Semantics Preservation in Model Transformation - A Comparison of Techniques. In: Méry, D., Merz, S. (eds) Integrated Formal Methods. IFM 2010. Lecture Notes in Computer Science, vol 6396. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-16265-7_14

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-16265-7_14

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-16264-0

  • Online ISBN: 978-3-642-16265-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation