Abstract
To cope with formal verification issues within the Model-Driven Engineering (MDE) paradigm, a separation of duties between software developers is usually proposed: MDE experts define models and transformations, while formal verification experts conduct the verification process. This is often aided by (semi)automatic translations form the MDE elements to their formal representation in the semantic domain used for verification. From a formal perspective, this requires semantic-preserving translations between the MDE elements and the semantic domain. The aim of this paper is to present formal semantics for the MOF and QVT-Relations languages which are standard languages for defining metamodels and model transformations, respectively. The semantics is based on the Theory of Institutions and reflect the conformance relation between models and metamodels, and the satisfaction of transformation rules between pairs of models. The theory assists in the definition of semantic-preserving translations between our institutions and other logics which will be used for verification.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
References
Kent, S.: Model driven engineering. In: Butler, M., Petre, L., Sere, K. (eds.) IFM 2002. LNCS, vol. 2335, pp. 286–298. Springer, Heidelberg (2002)
Object Management Group: Meta Object Facility (MOF) 2.0 Core Specification. Specification Version 2.0 (2003)
Object Management Group: Meta Object Facility (MOF) 2.0 Query/View/Transformation. Final Adopted Specification Version 1.1 (2009)
Kurtev, I., Bezivin, J., Aksit, M.: Technological spaces: An initial appraisal. In: Intl. Symposium on Distributed Objects and Applications (2002)
Cengarle, M.V., Knapp, A., Tarlecki, A., Wirsing, M.: A heterogeneous approach to UML semantics. In: Degano, P., De Nicola, R., Meseguer, J. (eds.) Concurrency, Graphs and Models. LNCS, vol. 5065, pp. 383–402. Springer, Heidelberg (2008)
Mossakowski, T.: Heterogeneous specification and the heterogeneous tool set. Tech. Rep., Universitaet Bremen, Habilitation thesis (2005)
Goguen, J.A., Burstall, R.M.: Institutions: Abstract Model Theory for Specification and Programming. J. ACM 39(1), 95–146 (1992)
Object Management Group: Object Constraint Language. Formal Specification Version 2.2 (2010)
Calegari, D., Szasz, N.: Bridging techological spaces for the verification of model transformations. In: Conf. Iberoamericana de Software Engineering, Uruguay (2013)
Goguen, J.A., Rosu, G.: Institution morphisms. Formal Aspects of Computing 13, 274–307 (2002)
Mossakowski, T., Haxthausen, A.E., Sannella, D., Tarlecki, A.: Casl - the common algebraic specification language: Semantics and proof theory. Computers and Artificial Intelligence 22, 285–321 (2003)
Cengarle, M.V., Knapp, A.: An institution for UML 2.0 static structures. Tech. Rep. TUM-I0807, Institut für Informatik, Technische Universität München (2008)
James, P., Knapp, A., Mossakowski, T., Roggenbach, M.: Designing domain specific languages – A craftsman’s approach for the railway domain using casl. In: Martí-Oliet, N., Palomino, M. (eds.) WADT 2012. LNCS, vol. 7841, pp. 178–194. Springer, Heidelberg (2013)
Sannella, D., Tarlecki, A.: Foundations of Algebraic Specification and Formal Software Development. Springer (2012)
Beckert, B., Keller, U., Schmitt, P.: Translating the Object Constraint Language into first-order predicate logic. In: VERIFY Workshop, Denmark (2002)
Shan, L., Zhu, H.: Semantics of metamodels in UML. In: 3rd IEEE Symposium on Theoretical Aspects of Software Engineering, pp. 55–62. IEEE Computer Society (2009)
Rivera, J., Durán, F., Vallecillo, A.: Formal specification and analysis of domain specific models using Maude. Simulation 85(11-12), 778–792 (2009)
Boronat, A., Knapp, A., Meseguer, J., Wirsing, M.: What is a multi-modeling language? In: Corradini, A., Montanari, U. (eds.) WADT 2008. LNCS, vol. 5486, pp. 71–87. Springer, Heidelberg (2009)
Orejas, F., Wirsing, M.: On the specification and verification of model transformations. In: Palsberg, J. (ed.) Semantics and Algebraic Specification. LNCS, vol. 5700, pp. 140–161. Springer, Heidelberg (2009)
Bidoit, M., Hennicker, R., Tort, F., Wirsing, M.: Correct realizations of interface constraints with OCL. In: France, R.B. (ed.) UML 1999. LNCS, vol. 1723, pp. 399–415. Springer, Heidelberg (1999)
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)
de Lara, J., Guerra, E.: Formal Support for QVT-Relations with Coloured Petri Nets. In: Schürr, A., Selic, B. (eds.) MODELS 2009. LNCS, vol. 5795, pp. 256–270. Springer, Heidelberg (2009)
Anastasakis, K., Bordbar, B., Küster, J.M.: Analysis of model transformations via Alloy. In: 4th MoDeVVa Workshop, pp. 47–56 (2007)
Stenzel, K., Moebius, N., Reif, W.: Formal verification of QVT transformations for code generation. In: Whittle, J., Clark, T., Kühne, T. (eds.) MODELS 2011. LNCS, vol. 6981, pp. 533–547. Springer, Heidelberg (2011)
Guerra, E., de Lara, J.: An algebraic semantics for QVT-relations check-only transformations. Fundamenta Informaticae 114, 73–101 (2012)
Calegari, D., Szasz, N.: Institution-based semantics for MOF and QVT-Relations (extended version). Tech. Rep. 13-06, InCo-PEDECIBA (2013) ISSN 0797-6410, http://www.fing.edu.uy/inco/pedeciba/bibliote/reptec/TR1306.pdf
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Calegari, D., Szasz, N. (2013). Institution-Based Semantics for MOF and QVT-Relations. In: Iyoda, J., de Moura, L. (eds) Formal Methods: Foundations and Applications. SBMF 2013. Lecture Notes in Computer Science, vol 8195. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-41071-0_4
Download citation
DOI: https://doi.org/10.1007/978-3-642-41071-0_4
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-41070-3
Online ISBN: 978-3-642-41071-0
eBook Packages: Computer ScienceComputer Science (R0)