×

zbMATH — the first resource for mathematics

On the specification and verification of model transformations. (English) Zbl 1253.68232
Palsberg, Jens (ed.), Semantics and algebraic specification. Essays dedicated to Peter D. Mosses on the occasion of his 60th birthday. Berlin: Springer (ISBN 978-3-642-04163-1/pbk). Lecture Notes in Computer Science 5700, 140-161 (2009).
Summary: 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.
For the entire collection see [Zbl 1173.68014].

MSC:
68Q65 Abstract data types; algebraic specification
Software:
Maude
PDF BibTeX XML Cite
Full Text: DOI
References:
[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) · Zbl 05535521 · doi:10.1007/978-3-642-00593-0_2
[2] Boronat, A., Knapp, A., Meseguer, J., Wirsing, M.: What is a multi-modelling language? In: WADT 2008 (2008) · Zbl 1253.68225
[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) · Zbl 05270517 · doi:10.1007/978-3-540-78743-3_28
[4] Bouhoula, A., Jouannaud, J.-P., Meseguer, J.: Specification and proof in membership equational logic. Theor. Comput. Sci. 236(1-2), 35–132 (2000) · Zbl 0938.68057 · doi:10.1016/S0304-3975(99)00206-6
[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) · Zbl 1115.68046
[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) · Zbl 1175.68114 · doi:10.1007/978-3-540-87405-8_29
[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) · Zbl 0744.68099
[8] Ehrig, H., Ehrig, K., Prange, U., Taentzer, G.: Fundamentals of algebraic graph transformation. Springer, Heidelberg (2006) · Zbl 1095.68047
[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) · Zbl 0611.68045 · doi:10.1007/978-3-642-95486-3_7
[10] Goguen, J.A., Burstall, R.M.: Institutions: Abstract model theory for specification and programming. J. ACM 39(1), 95–146 (1992) · Zbl 0799.68134 · doi:10.1145/147508.147524
[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) · Zbl 0591.68041 · doi:10.1007/BFb0015747
[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) · Zbl 1251.68019 · doi:10.1007/978-3-642-05118-0
[13] Habel, A., Heckel, R., Taentzer, G.: Graph grammars with negative application conditions. Fundamenta Informatica 287–313 (1996) · Zbl 0854.68055
[14] Habel, A., Pennemann, K.-H.: Correctness of high-level transformation systems relative to nested conditions. Math. Struct. in Comp. Sc. (to appear) · Zbl 1168.68022
[15] Heckel, R., Wagner, A.: Ensuring consistency of conditional graph rewriting - a constructive approach. ENTCS, 2 (1995) · Zbl 0910.68154
[16] Koch, M., Mancini, L.V., Parisi-Presicce, F.: Graph-based specification of access control policies. J. Comput. Syst. Sci, 1–33 (2005) · Zbl 1081.68072 · doi:10.1016/j.jcss.2004.11.002
[17] Mens, T., Gorp, P.V.: A taxonomy of model transformation. Electr. Notes Theor. Comput. Sci. 152, 125–142 (2006) · doi:10.1016/j.entcs.2005.10.021
[18] Mosses, P.D.: Unified algebras. In: ADT (1988) · Zbl 0716.68066
[19] Mosses, P.D.: Unified algebras and institutions. In: LICS 1989, pp. 304–312 (1989) · Zbl 0716.68066 · doi:10.1109/LICS.1989.39185
[20] Mosses, P.D.: Unified algebras and modules. In: Sixteenth Annual ACM Symposium on Principles of Programming Languages, POPL 1989, pp. 329–343 (1989) · doi:10.1145/75277.75306
[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) · Zbl 1175.68229 · doi:10.1007/978-3-540-87405-8_19
[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) · Zbl 1171.68516 · doi:10.1007/978-3-540-78743-3_14
[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) · Zbl 1239.68026 · doi:10.1007/978-3-642-03741-2_26
[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) · Zbl 1175.03008 · doi:10.1007/978-3-540-87405-8_20
[25] QVT (2005), http://www.omg.org/docs/ptc/05-11-01.pdf
[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) · Zbl 1175.68231 · doi:10.1007/978-3-540-87405-8_17
[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) · doi:10.1007/3-540-59071-4_45
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.