Skip to main content
SpringerLink
Log in

A Formal Framework to Prove the Correctness of Model Driven Engineering Composition Operators

  • Conference paper
Formal Methods and Software Engineering (ICFEM 2014)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 8829))

Included in the following conference series:

Abstract

Current trends in system engineering combine modeling, composition and verification technologies in order to harness their ever growing complexity. Each composition operator dedicated to a different modeling concern should be proven to be property preserving at assembly time. These proofs are usually burdensome with repetitive aspects. Our work targets the factorisation of these aspects relying on primitive generic composition operators used to express more sophisticated language specific ones. These operators are defined for languages expressed with OMG MOF metamodeling technologies. The proofs are done with the Coq proof assistant relying on the Coq4MDE framework defined previously. These basic operators, Union and Substitution, are illustrated using the MOF Package Merge as a composition operator and the preservation of model conformance as a verified property.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Aßmann, U.: Invasive software composition. Springer-Verlag New York Inc. (2003)

    Google Scholar 

  2. Barbier, F., Castéran, P., Cariou, E., Le Goaer, O., et al.: Adaptive software based on correct-by-construction metamodels. In: Progressions and Innovations in Model-Driven Software Engineering, pp. 308–325 (2013)

    Google Scholar 

  3. Basu, A., Bozga, M., Sifakis, J.: Modeling heterogeneous real-time components in BIP. In: Fourth IEEE International Conference on Software Engineering and Formal Methods, SEFM 2006, pp. 3–12. IEEE (2006)

    Google Scholar 

  4. Baya, A., Asri, B.E.: Composing specific domains for large scale systems. Journal of Communication and Computer 10, 844–856 (2013)

    Google Scholar 

  5. Bensalem, S., Bozga, M., Nguyen, T., Sifakis, J.: Compositional verification for component-based systems and application. Software, IET 4(3), 181–193 (2010)

    Article  Google Scholar 

  6. Bernstein, P., Halevy, A., Pottinger, R.: A vision for management of complex models. ACM Sigmod Record 29(4), 55–63 (2000)

    Article  Google Scholar 

  7. Bézivin, J.: In search of a basic principle for model driven engineering. Novatica Journal, Special Issue 5(2), 21–24 (2004)

    Google Scholar 

  8. Boronat, A., Meseguer, J.: An algebraic semantics for MOF. Formal Aspects of Computing 22(3-4), 269–296 (2010)

    Article  MATH  Google Scholar 

  9. Brucker, A.D., Wolff, B.: A proposal for a formal OCL semantics in isabelle/HOL. In: Carreño, V.A., Muñoz, C.A., Tahar, S. (eds.) TPHOLs 2002. LNCS, vol. 2410, pp. 99–114. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  10. Brucker, A.D., Wolff, B.: HOL-OCL: A formal proof environment for uml/ocl. In: Fiadeiro, J.L., Inverardi, P. (eds.) FASE 2008. LNCS, vol. 4961, pp. 97–100. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  11. Brunet, G., Chechik, M., Easterbrook, S., Nejati, S., Niu, N., Sabetzadeh, M.: A manifesto for model merging. In: Proceedings of the 2006 International Workshop on Global Integrated Model Management, pp. 5–12. ACM (2006)

    Google Scholar 

  12. Cengarle, M.V., Grönniger, H., Rumpe, B., Schindler, M.: System model semantics of class diagrams. Technische Universitat Braunschweig (2008)

    Google Scholar 

  13. Clarke, S.: Extending standard UML with model composition semantics. Science of Computer Programming 44(1), 71–100 (2002)

    Article  MATH  Google Scholar 

  14. Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Quesada, J.: Maude: specification and programming in rewriting logic. Theoretical Computer Science 285(2), 187–243 (2002)

    Article  MathSciNet  MATH  Google Scholar 

  15. Coquand, T., Huet, G., et al.: The calculus of constructions (1986)

    Google Scholar 

  16. Del Fabro, M.D., Valduriez, P.: Towards the efficient development of model transformations using model weaving and matching transformations. Software and System Modeling 8(3), 305–324 (2009)

    Article  Google Scholar 

  17. Garnacho, M., Bodeveix, J.-P., Filali-Amine, M.: A mechanized semantic framework for real-time systems. In: Braberman, V., Fribourg, L. (eds.) FORMATS 2013. LNCS, vol. 8053, pp. 106–120. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  18. Giorgino, M., Strecker, M., Matthes, R., Pantel, M.: Verification of the schorr-waite algorithm – from trees to graphs. In: Alpuente, M. (ed.) LOPSTR 2010. LNCS, vol. 6564, pp. 67–83. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  19. Hamiaz, M.K., Pantel, M., Combemale, B., Thirioux, X.: Correct-by-construction model composition: Application to the invasive software composition method. In: FESCA, pp. 108–122 (2014)

    Google Scholar 

  20. Henriksson, J., Heidenreich, F., Johannes, J., Zschaler, S., Aßmann, U.: Extending grammars and metamodels for reuse: the Reuseware approach. Software, IET 2(3), 165–184 (2008)

    Article  Google Scholar 

  21. Holt, J., Perry, S.: SysML for systems engineering, vol. 7. IET (2008)

    Google Scholar 

  22. Jackson, D.: Software abstractions-logic, language, and analysis, revised edition (2012)

    Google Scholar 

  23. Jouault, F., Bézivin, J.: Km3: A dsl for metamodel specification. In: Gorrieri, R., Wehrheim, H. (eds.) FMOODS 2006. LNCS, vol. 4037, pp. 171–185. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  24. Kezadri, M.: Assistance à la validation et vérification de systèmes critiques: ontologies et intégration de composants. PhD thesis (2013)

    Google Scholar 

  25. Kezadri, M., Combemale, B., Pantel, M., Thirioux, X.: A proof assistant based formalization of MDE components. In: Arbab, F., Ölveczky, P.C. (eds.) FACS 2011. LNCS, vol. 7253, pp. 223–240. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  26. Kühne, T.: Matters of (meta-) modeling. Software & Systems Modeling 5(4), 369–385 (2006)

    Article  Google Scholar 

  27. Lara, J., Guerra, E.: From types to type requirements: genericity for model-driven engineering. Software and Systems Modeling 12(3), 453–474 (2013)

    Article  Google Scholar 

  28. Maoz, S., Ringert, J.O., Rumpe, B.: Semantically configurable consistency analysis for class and object diagrams. In: Whittle, J., Clark, T., Kühne, T. (eds.) MODELS 2011. LNCS, vol. 6981, pp. 153–167. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  29. Morin, B., Klein, J., Barais, O., Jézéquel, J.-M.: A generic weaver for supporting product lines. In: Proceedings of the 13th International Workshop on Early Aspects, pp. 11–18. ACM (2008)

    Google Scholar 

  30. Nejati, S., Sabetzadeh, M., Chechik, M., Easterbrook, S., Zave, P.: Matching and merging of statecharts specifications. In: Proceedings of the 29th international conference on Software Engineering, pp. 54–64. IEEE Computer Society (2007)

    Google Scholar 

  31. Object Management Group, Inc. Meta Object Facility (MOF) 2.0 Core Specification (January 2006); Final Adopted Specification.

    Google Scholar 

  32. Object Management Group, Inc. Meta Object Facility (MOF) 2.4.2 Core Specification (January 2014)

    Google Scholar 

  33. O. OMG. Unified modeling language (omg uml)-infrastructure(v2.4.1) (2011), http://www.omg.org/spec/UML/2.4.1

  34. Picard, C., Matthes, R.: Coinductive graph representation: the problem of embedded lists. In: Electronic Communications of the EASST, Special issue Graph Computation Models, GCM 2010 (2011)

    Google Scholar 

  35. Poernomo, I.: The meta-object facility typed. In: Haddad, H. (ed.) SAC, pp. 1845–1849. ACM (2006)

    Google Scholar 

  36. Poernomo, I.: Proofs-as-model-transformations. In: Vallecillo, A., Gray, J., Pierantonio, A. (eds.) ICMT 2008. LNCS, vol. 5063, pp. 214–228. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  37. Poernomo, I., Terrell, J.: Correct-by-construction model transformations from partially ordered specifications in coq. In: Dong, J.S., Zhu, H. (eds.) ICFEM 2010. LNCS, vol. 6447, pp. 56–73. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  38. Romero, J.R., Rivera, J.E., Durán, F., Vallecillo, A.: Formal and tool support for Model Driven Engineering with Maude. Journal of Object Technology 6(9), 187–207 (2007)

    Article  Google Scholar 

  39. RTCA / EUROCAE. “Formal Methods Supplement to DO-178C [ED-12C]”, DO-333/ED-218 (2011)

    Google Scholar 

  40. RTCA / EUROCAE. “Model-Based Development and Verification Supplement to DO-178C [ED-12C]”, DO-331/ED-216 (2011)

    Google Scholar 

  41. RTCA / EUROCAE. “Software Considerations in Airborne Systems and Equipment Certification”, DO-178C/ED-12C (2011)

    Google Scholar 

  42. RTCA / EUROCAE. “DO-330/ED-215: Software Tool Qualification Considerations” - clarifying software tools and avionics tool qualification (2012)

    Google Scholar 

  43. Sentilles, S., Štěpán, P., Carlson, J., Crnković, I.: Integration of extra-functional properties in component models. In: Lewis, G.A., Poernomo, I., Hofmeister, C. (eds.) CBSE 2009. LNCS, vol. 5582, pp. 173–190. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  44. Thirioux, X., Combemale, B., Crégut, X., Garoche, P.-L.: A Framework to Formalise the MDE Foundations. In: Paige, R., Bézivin, J. (eds.) International Workshop on Towers of Models (TOWERS), Zurich, pp. 14–30 (June 2007)

    Google Scholar 

  45. Troya, J., Vallecillo, A.: Towards a rewriting logic semantics for ATL. In: Tratt, L., Gogolla, M. (eds.) ICMT 2010. LNCS, vol. 6142, pp. 230–244. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  46. Warmer, J.B., Kleppe, A.G.: The object constraint language: getting your models ready for MDA. Addison-Wesley Professional (2003)

    Google Scholar 

  47. Xie, F., Browne, J.: Verified systems by composition from verified components. ACM SIGSOFT Software Engineering Notes 28(5), 277–286 (2003)

    Article  Google Scholar 

  48. Zito, A.: UML’s Package Extension Mechanism: Taking a Closer Look at Package Merge. Queen’s University (2006)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Université de Toulouse, IRIT, France

    Mounira Kezadri Hamiaz, Marc Pantel & Xavier Thirioux

  2. Université de Rennes 1, IRISA, France

    Benoit Combemale

Authors
  1. Mounira Kezadri Hamiaz
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Marc Pantel
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Benoit Combemale
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Xavier Thirioux
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Inria Nancy - Grand Est, 615 rue du Jardin Botanique, 54602, Villers-lès-Nancy, France

    Stephan Merz

  2. Université du Luxembourg, 6 rue Richard Coudenhove-Kalergi, 1359, Luxembourg, Luxembourg

    Jun Pang

Rights and permissions

Reprints and permissions

Copyright information

© 2014 Springer International Publishing Switzerland

About this paper

Cite this paper

Kezadri Hamiaz, M., Pantel, M., Combemale, B., Thirioux, X. (2014). A Formal Framework to Prove the Correctness of Model Driven Engineering Composition Operators. In: Merz, S., Pang, J. (eds) Formal Methods and Software Engineering. ICFEM 2014. Lecture Notes in Computer Science, vol 8829. Springer, Cham. https://doi.org/10.1007/978-3-319-11737-9_16

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-11737-9_16

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-11736-2

  • Online ISBN: 978-3-319-11737-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation