Abstract
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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
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)
Boronat, A., Knapp, A., Meseguer, J., Wirsing, M.: What is a multi-modelling language? In: WADT 2008 (2008)
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)
Bouhoula, A., Jouannaud, J.-P., Meseguer, J.: Specification and proof in membership equational logic. Theor. Comput. Sci. 236(1-2), 35–132 (2000)
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)
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)
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)
Ehrig, H., Ehrig, K., Prange, U., Taentzer, G.: Fundamentals of algebraic graph transformation. Springer, Heidelberg (2006)
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)
Goguen, J.A., Burstall, R.M.: Institutions: Abstract model theory for specification and programming. J. ACM 39(1), 95–146 (1992)
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)
Guerra, E., de Lara, J., Orejas, F.: Pattern-based model-to-model transformation: Handling attribute conditions. In: ICMT 2009. LNCS. Springer, Heidelberg (accepted, 2009)
Habel, A., Heckel, R., Taentzer, G.: Graph grammars with negative application conditions. Fundamenta Informatica 287–313 (1996)
Habel, A., Pennemann, K.-H.: Correctness of high-level transformation systems relative to nested conditions. Math. Struct. in Comp. Sc. (to appear)
Heckel, R., Wagner, A.: Ensuring consistency of conditional graph rewriting - a constructive approach. ENTCS, 2 (1995)
Koch, M., Mancini, L.V., Parisi-Presicce, F.: Graph-based specification of access control policies. J. Comput. Syst. Sci, 1–33 (2005)
Mens, T., Gorp, P.V.: A taxonomy of model transformation. Electr. Notes Theor. Comput. Sci. 152, 125–142 (2006)
Mosses, P.D.: Unified algebras. In: ADT (1988)
Mosses, P.D.: Unified algebras and institutions. In: LICS 1989, pp. 304–312 (1989)
Mosses, P.D.: Unified algebras and modules. In: Sixteenth Annual ACM Symposium on Principles of Programming Languages, POPL 1989, pp. 329–343 (1989)
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)
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)
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)
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)
QVT (2005), http://www.omg.org/docs/ptc/05-11-01.pdf
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)
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)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Orejas, F., Wirsing, M. (2009). On the Specification and Verification of Model Transformations. In: Palsberg, J. (eds) Semantics and Algebraic Specification. Lecture Notes in Computer Science, vol 5700. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-04164-8_8
Download citation
DOI: https://doi.org/10.1007/978-3-642-04164-8_8
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-04163-1
Online ISBN: 978-3-642-04164-8
eBook Packages: Computer ScienceComputer Science (R0)