A Semantic Framework to Improve Model-to-Model Transformations

  • Mohamed Elkamel HamdaneEmail author
  • Karima Berramla
  • Allaoua Chaoui
  • Abou El Hasan Benyamina
Conference paper
Part of the Smart Innovation, Systems and Technologies book series (SIST, volume 111)


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.


Model Transformation Proof Correctness Coq 


  1. 1.
    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)Google Scholar
  2. 2.
    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)Google Scholar
  3. 3.
    Kleppe, A., Warmer, J., Bas, W.: MDA Explained: The Model Driven Architecture: Practice and Promise. Addison-Wesley Professional, Boston (2003)Google Scholar
  4. 4.
    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)Google Scholar
  5. 5.
    Rahim, L. A., Whittle, J.: A survey of approaches for verifying model transformations. Softw. Syst. Model. 1003–1028 (2015)Google Scholar
  6. 6.
    Cariou, E., Belloir, N., Barbier, F., Djemam, N.: OCL contracts for the verification of model transformations, Electronic Communications of the EASST (2010)Google Scholar
  7. 7.
    Audebaud, P., Paulin-Mohring, C.: Proofs of randomized algorithms in Coq. Sci. Comput. Programm. 74, 568–589 (2009)MathSciNetCrossRefGoogle Scholar
  8. 8.
    Coq development team, coq reference manual, version 8.6, 485, INRIA (2016).
  9. 9.
    Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development: CoqArt: The Calculus of Inductive Constructions. Springer (2013)Google Scholar
  10. 10.
    Calegari, D., Luna, C., Szasz, N., Tasistro, A.: A type-theoretic framework for certified model transformations. In: SBMF, pp. 112–127 (2010)Google Scholar
  11. 11.
    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)Google Scholar
  12. 12.
    Lano, K., Clark, T., Kolahdouz-Rahimi, S.: A framework for model transformation verification. Formal Aspects Comput. 27, 193 (2015)MathSciNetCrossRefGoogle Scholar
  13. 13.
    de Putter, S., Wijs, A.: A formal verification technique for behavioural model-to-model transformations. Formal Aspects Comput., 1–41 (2017)Google Scholar
  14. 14.
    Steinberg, D., Budinsky, F., Paternostro, M., Merks, E.: Eclipse Modelling Framework-Chapter: Ecore Modelling Concepts. Addison-Wesley Professional, Boston (2008)Google Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  • Mohamed Elkamel Hamdane
    • 1
    • 2
    Email author
  • Karima Berramla
    • 3
  • Allaoua Chaoui
    • 1
  • Abou El Hasan Benyamina
    • 3
  1. 1.MISC LaboratoryAbdElhamid Mahri University of Constantine 2ConstantineAlgeria
  2. 2.Department of Mathematics and Computer ScienceTeachers’ Training School of ConstantineConstantineAlgeria
  3. 3.Lapeci LaboratoryUniversity of Ahmed Ben Bella Oran 1OranAlgeria

Personalised recommendations