Abstract
The Model Driven Engineering approach is an important contribution in Software Engineering. The strength of this approach is related to its model transformation process. However, ensuring that the output model is semantically equivalent to the input model is in itself a challenge. This paper introduces a semantic framework based on the theorem proving method in order to rise this challenge. The framework allows facilitating any proof of model-to-model transformations. We explain how to apply this framework using the Coq tool that’s to prove the correctness of a standard case study.
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
References
Benzmuller, C., Paleo, B.W.: Interacting with modal logics in the coq proof assistant. In: International Computer Science Symposium in Russia, pp. 398–411. Springer (2015)
Buttner, F., Egea, M., Cabot, J.: On verifying ATL transformations using ‘o-the-shelf’ SMT solvers. In: MoDELS, vol. 12, pp. 432–448. Springer (2012)
Kleppe, A., Warmer, J., Bas, W.: MDA Explained: The Model Driven Architecture: Practice and Promise. Addison-Wesley Professional, Boston (2003)
Hamdane, M.E., Berramla, K., Chaoui, A.: Using MDA with model checking to ensure the development of consistent AADL models. In: The First International Conference on Embedded and Distributed Systems (EDiS 2017), Algeria, pp. 135–140 (2017)
Rahim, L. A., Whittle, J.: A survey of approaches for verifying model transformations. Softw. Syst. Model. 1003–1028 (2015)
Cariou, E., Belloir, N., Barbier, F., Djemam, N.: OCL contracts for the verification of model transformations, Electronic Communications of the EASST (2010)
Audebaud, P., Paulin-Mohring, C.: Proofs of randomized algorithms in Coq. Sci. Comput. Programm. 74, 568–589 (2009)
Coq development team, coq reference manual, version 8.6, 485, INRIA (2016). https://coq.inria.fr/distrib/V8.6/refman/
Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development: CoqArt: The Calculus of Inductive Constructions. Springer (2013)
Calegari, D., Luna, C., Szasz, N., Tasistro, A.: A type-theoretic framework for certified model transformations. In: SBMF, pp. 112–127 (2010)
Berramla, K., Deba, E.A., Senouci, M.: Formal validation of model transformation with coq proof assistant. In: First IEEE International Conference on New Technologies of Information and Communication, Algeria (2015)
Lano, K., Clark, T., Kolahdouz-Rahimi, S.: A framework for model transformation verification. Formal Aspects Comput. 27, 193 (2015)
de Putter, S., Wijs, A.: A formal verification technique for behavioural model-to-model transformations. Formal Aspects Comput., 1–41 (2017)
Steinberg, D., Budinsky, F., Paternostro, M., Merks, E.: Eclipse Modelling Framework-Chapter: Ecore Modelling Concepts. Addison-Wesley Professional, Boston (2008)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2019 Springer Nature Switzerland AG
About this paper
Cite this paper
Hamdane, M.E., Berramla, K., Chaoui, A., Benyamina, A.E.H. (2019). A Semantic Framework to Improve Model-to-Model Transformations. In: Rocha, Á., Serrhini, M. (eds) Information Systems and Technologies to Support Learning. EMENA-ISTL 2018. Smart Innovation, Systems and Technologies, vol 111. Springer, Cham. https://doi.org/10.1007/978-3-030-03577-8_32
Download citation
DOI: https://doi.org/10.1007/978-3-030-03577-8_32
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-03576-1
Online ISBN: 978-3-030-03577-8
eBook Packages: Intelligent Technologies and RoboticsIntelligent Technologies and Robotics (R0)