On the Specification and Verification of Model Transformations

  • Fernando Orejas
  • Martin Wirsing
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5700)


Model transformation is one of the key notions in the model-driven engineering approach to software development. Most work in this area concentrates on designing methods and tools for defining or implementing transformations, on defining interesting specific classes of transformations, or on proving properties about given transformations, like confluence or termination. However little attention has been paid to the verification of transformations. In this sense, the aim of this work is, on one hand, to clarify what means to verify a model transformation and, on the other, to propose a specific approach for proving the correctness of transformations. More precisely, we use some general patterns to describe both the transformation and the properties that we may want to verify. Then, we provide a method for proving the correctness of a given transformation.


Model Transformation Class Diagram Target Model Relation Symbol Graph Grammar 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Boronat, A., Heckel, R., Meseguer, J.: Rewriting logic semantics and verification of model transformations. In: Chechik, M., Wirsing, M. (eds.) FASE 2009. LNCS, vol. 5503, pp. 18–33. Springer, Heidelberg (2009)Google Scholar
  2. 2.
    Boronat, A., Knapp, A., Meseguer, J., Wirsing, M.: What is a multi-modelling language? In: WADT 2008 (2008)Google Scholar
  3. 3.
    Boronat, A., Meseguer, J.: An algebraic semantics for MOF. In: Fiadeiro, J.L., Inverardi, P. (eds.) FASE 2008. LNCS, vol. 4961, pp. 377–391. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  4. 4.
    Bouhoula, A., Jouannaud, J.-P., Meseguer, J.: Specification and proof in membership equational logic. Theor. Comput. Sci. 236(1-2), 35–132 (2000)MathSciNetCrossRefzbMATHGoogle Scholar
  5. 5.
    Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C. (eds.): All About Maude - A High-Performance Logical Framework. LNCS, vol. 4350. Springer, Heidelberg (2007)zbMATHGoogle Scholar
  6. 6.
    de Lara, J., Guerra, E.: Pattern-based model-to-model transformation. In: Ehrig, H., Heckel, R., Rozenberg, G., Taentzer, G. (eds.) ICGT 2008. LNCS, vol. 5214, pp. 426–441. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  7. 7.
    Ehrig, H., Baldamus, M., Orejas, F.: Amalgamation and extension in the framework of specification logics and generalized morphisms. Bulletin of the EATCS 44, 129–143 (1991)zbMATHGoogle Scholar
  8. 8.
    Ehrig, H., Ehrig, K., Prange, U., Taentzer, G.: Fundamentals of algebraic graph transformation. Springer, Heidelberg (2006)zbMATHGoogle Scholar
  9. 9.
    Ehrig, H., Habel, A.: Graph grammars with application conditions. In: Rozenberg, G., Salomaa, A. (eds.) The Book of L, pp. 87–100. Springer, Heidelberg (1986)CrossRefGoogle Scholar
  10. 10.
    Goguen, J.A., Burstall, R.M.: Institutions: Abstract model theory for specification and programming. J. ACM 39(1), 95–146 (1992)MathSciNetCrossRefzbMATHGoogle Scholar
  11. 11.
    Goguen, J.A., Jouannaud, J.-P., Meseguer, J.: Operational semantics for order-sorted algebra. In: Brauer, W. (ed.) ICALP 1985. LNCS, vol. 194, pp. 221–231. Springer, Heidelberg (1985)CrossRefGoogle Scholar
  12. 12.
    Guerra, E., de Lara, J., Orejas, F.: Pattern-based model-to-model transformation: Handling attribute conditions. In: ICMT 2009. LNCS. Springer, Heidelberg (accepted, 2009)Google Scholar
  13. 13.
    Habel, A., Heckel, R., Taentzer, G.: Graph grammars with negative application conditions. Fundamenta Informatica 287–313 (1996)Google Scholar
  14. 14.
    Habel, A., Pennemann, K.-H.: Correctness of high-level transformation systems relative to nested conditions. Math. Struct. in Comp. Sc. (to appear)Google Scholar
  15. 15.
    Heckel, R., Wagner, A.: Ensuring consistency of conditional graph rewriting - a constructive approach. ENTCS, 2 (1995)Google Scholar
  16. 16.
    Koch, M., Mancini, L.V., Parisi-Presicce, F.: Graph-based specification of access control policies. J. Comput. Syst. Sci, 1–33 (2005)Google Scholar
  17. 17.
    Mens, T., Gorp, P.V.: A taxonomy of model transformation. Electr. Notes Theor. Comput. Sci. 152, 125–142 (2006)CrossRefGoogle Scholar
  18. 18.
    Mosses, P.D.: Unified algebras. In: ADT (1988)Google Scholar
  19. 19.
    Mosses, P.D.: Unified algebras and institutions. In: LICS 1989, pp. 304–312 (1989)Google Scholar
  20. 20.
    Mosses, P.D.: Unified algebras and modules. In: Sixteenth Annual ACM Symposium on Principles of Programming Languages, POPL 1989, pp. 329–343 (1989)Google Scholar
  21. 21.
    Orejas, F.: Attributed graph constraints. In: Ehrig, H., Heckel, R., Rozenberg, G., Taentzer, G. (eds.) ICGT 2008. LNCS, vol. 5214, pp. 274–288. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  22. 22.
    Orejas, F., Ehrig, H., Prange, U.: A logic of graph constraints. In: Fiadeiro, J.L., Inverardi, P. (eds.) FASE 2008. LNCS, vol. 4961, pp. 179–198. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  23. 23.
    Orejas, F., Guerra, E., de Lara, J., Ehrig, H.: Correctness, completeness and termination of pattern-based model-to-model transformation. In: Kurz, A., Lenisa, M., Tarlecki, A. (eds.) CALCO 2009. LNCS, vol. 5728, pp. 383–397. Springer, Heidelberg (2009)Google Scholar
  24. 24.
    Pennemann, K.-H.: Resolution-like theorem proving for high-level condition. In: Ehrig, H., Heckel, R., Rozenberg, G., Taentzer, G. (eds.) ICGT 2008. LNCS, vol. 5214, pp. 289–304. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  25. 25.
  26. 26.
    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)CrossRefGoogle Scholar
  27. 27.
    Schürr, A.: Specification of graph translators with triple graph grammars. In: Mayr, E.W., Schmidt, G., Tinhofer, G. (eds.) WG 1994. LNCS, vol. 903, pp. 151–163. Springer, Heidelberg (1995)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2009

Authors and Affiliations

  • Fernando Orejas
    • 1
  • Martin Wirsing
    • 2
  1. 1.Universitat Politècnica de CatalunyaBarcelonaSpain
  2. 2.Ludwig-Maximilians UniversitätMunichGermany

Personalised recommendations