{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,15]],"date-time":"2025-12-15T14:02:22Z","timestamp":1765807342864,"version":"3.37.3"},"reference-count":53,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2016,5,1]],"date-time":"2016-05-01T00:00:00Z","timestamp":1462060800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"name":"Midi Pyr\u00e9n\u00e9es, French DGCIS and FUI"},{"DOI":"10.13039\/501100002403","name":"Taibah University","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100002403","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2016,5]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>Model composition is a crucial activity in Model Driven Engineering both to reuse validated and verified model elements and to handle separately the various aspects in a complex system and then weave them while preserving their properties. Many research activities target this compositional validation and verification (V &amp; V) strategy: allow the independent assessment of components and minimize the residual V &amp; V activities at assembly time. However, there is a continuous and increasing need for the definition of new composition operators that allow the reconciliation of existing models to build new systems according to various requirements. These ones are usually built from scratch and must be systematically verified to assess that they preserve the properties of the assembled elements. This verification is usually tedious but is mandatory to avoid verifying the composite system for each use of the operators. Our work addresses these issues, we first target the use of proof assistants for specifying and verifying compositional verification frameworks relying on formal verification techniques instead of testing and proofreading. Then, using a divide and conquer approach, we focus on the development of elementary composition operators that are easy to verify and can be used to further define complex composition operators. In our approach, proofs for the complex operators are then obtained by assembling the proofs of the basic operators. To illustrate our proposal, we use the Coq proof assistant to formalize the language-independent elementary composition operators Union and Substitution and the proof that the conformance of models with respect to metamodels is preserved during composition. We show that more sophisticated composition operators that share parts of the implementation and have several properties in common (especially: aspect oriented modeling composition approach, invasive software composition, and package merge) can then be built from the basic ones, and that the proof of conformance preservation can also be built from the proofs of basic operators.<\/jats:p>","DOI":"10.1007\/s00165-016-0354-6","type":"journal-article","created":{"date-parts":[[2016,1,27]],"date-time":"2016-01-27T14:41:02Z","timestamp":1453905662000},"page":"409-440","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Correct-by-construction model driven engineering composition operators"],"prefix":"10.1145","volume":"28","author":[{"given":"Mounira","family":"Kezadri Hamiaz","sequence":"first","affiliation":[{"name":"College of Computer Science and Engineering (CCSE), Taibah University, Al Madinah, Saudi Arabia"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marc","family":"Pantel","sequence":"additional","affiliation":[{"name":"IRIT, Universit\u00e9 de Toulouse, Toulouse, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xavier","family":"Thirioux","sequence":"additional","affiliation":[{"name":"IRIT, Universit\u00e9 de Toulouse, Toulouse, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Benoit","family":"Combemale","sequence":"additional","affiliation":[{"name":"IRISA, Universit\u00e9 de Rennes 1, Rennes, France"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"crossref","unstructured":"Apel S Lengauer C M\u00f6ller B K\u00e4stner C (2008) An algebra for features and feature composition. In: Algebraic methodology and software technology Springer New York pp 36\u201350","DOI":"10.1007\/978-3-540-79980-1_4"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"publisher","DOI":"10.5555\/778164"},{"key":"e_1_2_1_2_3_2","unstructured":"Basu A Bozga M Sifakis J (2006) Modeling heterogeneous real-time components in BIP. In: Software engineering and formal methods 2006. SEFM 2006. 4th IEEE international conference on pp 3\u201312"},{"issue":"2","key":"e_1_2_1_2_4_2","first-page":"21","article-title":"In search of a basic principle for model driven engineering","volume":"5","author":"B\u00e9zivin J","year":"2004","journal-title":"Novat J Special Issue"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"publisher","DOI":"10.1145\/369275.369289"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-009-0140-9"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(01)00359-0"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"crossref","unstructured":"Chrz\u0105szcz J (2003) Implementing modules in the Coq system: theorem proving in higher order logics pp 270\u2013286","DOI":"10.1007\/10930755_18"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0167-6423(02)00030-8"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"crossref","unstructured":"Vin\u00edcius Carvalho M Lopes D Abdelouahab Z (2015) A framework based on model driven engineering to support schema merging in database systems. In: New trends in networking computing e-learning systems sciences and engineering Springer New York pp 397\u2013405","DOI":"10.1007\/978-3-319-06764-3_49"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"crossref","unstructured":"Calegari D Luna C Szasz N Tasistro \u00c1 (2011) A type-theoretic framework for certified model transformations. In: Formal methods: foundations and applications Springer New York pp 112\u2013127","DOI":"10.1007\/978-3-642-19829-8_8"},{"key":"e_1_2_1_2_12_2","unstructured":"Didonet Del Fabro M B\u00e9zivin J Jouault F Breton E Gueltas G (2005) AMW: a generic model weaver. In: Proceedings of the 1\u00e8res Journ\u00e9es sur l\u2019Ing\u00e9nierie Dirig\u00e9e par les Mod\u00e8les"},{"key":"e_1_2_1_2_13_2","unstructured":"Dijkstra EW (1976) A discipline of programming volume 1. Prentice-Hall Englewood Cliffs"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"crossref","unstructured":"France R Fleurey F Reddy R Baudry B Ghosh S (2007) Providing support for model composition in metamodels. In: Enterprise distributed object computing conference 2007. EDOC 2007. 11th IEEE international pp 253\u2013253","DOI":"10.1109\/EDOC.2007.55"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"crossref","unstructured":"France R Rumpe B (2007) Model-driven development of complex software: a research roadmap. In: 2007 Future of software engineering IEEE Computer Society pp 37\u201354","DOI":"10.1109\/FOSE.2007.14"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"publisher","DOI":"10.1049\/ip-sen:20040920"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"crossref","unstructured":"Giorgino M Strecker M Matthes R Pantel M (2011) Verification of the schorr-waite algorithm\u2013from trees to graphs. Logic-based program synthesis and transformation pp 67\u201383","DOI":"10.1007\/978-3-642-20551-4_5"},{"key":"e_1_2_1_2_18_2","unstructured":"Henriksson J (2009) A lightweight framework for universal fragment composition with an application in the semantic web. PhD thesis TU Dresden"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"publisher","DOI":"10.1049\/iet-sen:20070060"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"crossref","unstructured":"Heidenreich F Henriksson J Johannes J Zschaler S (2009) On language-independent model modularisation. In: Transactions on aspect-oriented software development VI pp 39\u201382","DOI":"10.1007\/978-3-642-03764-1_2"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"crossref","unstructured":"Holt J Perry S (2008) SysML for systems engineering volume 7. IET","DOI":"10.1049\/PBPC007E"},{"key":"e_1_2_1_2_22_2","unstructured":"Jeanneret C (2007\u20132008) An analysis of model composition approaches. Master\u2019s thesis Ecole Polytechnique F\u00e9d\u00e9rale de Lausanne"},{"key":"e_1_2_1_2_23_2","unstructured":"Jendrik J (2011) Component-based model-driven software development. PhD thesis vorgelegt an der Technischen Universit\u00e4t Dresden Fakult\u00e4t Informatik"},{"key":"e_1_2_1_2_24_2","doi-asserted-by":"publisher","DOI":"10.5381\/jot.2007.6.9.a10"},{"key":"e_1_2_1_2_25_2","doi-asserted-by":"crossref","unstructured":"Jayaraman P Whittle J Elkhodary AM Gomaa H (2007) Model composition in product lines and feature interaction detection using critical pair analysis. In: Model driven engineering languages and systems pp 151\u2013165","DOI":"10.1007\/978-3-540-75209-7_11"},{"key":"e_1_2_1_2_26_2","doi-asserted-by":"crossref","unstructured":"Kienzle J Al Abed W Klein J (2009) Aspect-oriented multi-view modeling. In: Proceedings of the 8th ACM international conference on aspect-oriented software development pp 87\u201398 ACM","DOI":"10.1145\/1509239.1509252"},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"crossref","unstructured":"Kezadri Hamiaz M Pantel M Combemale B Thirioux X (2014) Correct-by-construction model composition: application to the invasive software composition method. In: FESCA pp 108\u2013122","DOI":"10.4204\/EPTCS.147.8"},{"key":"e_1_2_1_2_28_2","doi-asserted-by":"crossref","unstructured":"Kezadri Hamiaz M Pantel M Combemale B Thirioux X (2014) A formal framework to prove the correctness of model driven engineering composition operators. In: ICFEM\u201914\u201316th international conference on formal engineering methods Springer New York pp 235\u2013250","DOI":"10.1007\/978-3-319-11737-9_16"},{"key":"e_1_2_1_2_29_2","doi-asserted-by":"crossref","unstructured":"Klein J Lo\u00efc H Jean-Marc J (2006) Semantic-based weaving of scenarios. In: Proceedings of the 5th international conference on aspect-oriented software development ACM pp 27\u201338","DOI":"10.1145\/1119655.1119662"},{"key":"e_1_2_1_2_30_2","doi-asserted-by":"crossref","unstructured":"Kezadri M Pantel M Combemale B Thirioux X (2011) A proof assistant based formalization of components in MDE. In: 8th international symposium on formal aspects of component software (FACS 2011) Springer Berlin pp 223\u2013240","DOI":"10.1007\/978-3-642-35743-5_14"},{"key":"e_1_2_1_2_31_2","unstructured":"Letkeman K (2005) Comparing and merging UML models in IBM rational software architect. IBM Rational"},{"key":"e_1_2_1_2_32_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10270-011-0221-0"},{"key":"e_1_2_1_2_33_2","doi-asserted-by":"crossref","unstructured":"Manuel G Jean-Paul B Mamoun F-A (2013) A mechanized semantic framework for real-time systems. In: Formal modeling and analysis of timed systems Springer New York pp 106\u2013120","DOI":"10.1007\/978-3-642-40229-6_8"},{"key":"e_1_2_1_2_34_2","unstructured":"Noy NF Musen MA (2000) Algorithm and tool for automated ontology merging and alignment. In: Proceedings of the 17th national conference on artificial intelligence (AAAI-00). Available as SMI technical report SMI-2000-0831"},{"key":"e_1_2_1_2_35_2","doi-asserted-by":"crossref","unstructured":"Nejati S Sabetzadeh M Chechik M Easterbrook S Zave P (2007) Matching and merging of statecharts specifications. In: Proceedings of the 29th international conference on software engineering IEEE Computer Society pp 54\u201364","DOI":"10.1109\/ICSE.2007.50"},{"key":"e_1_2_1_2_36_2","unstructured":"Object Management Group Inc. (2006) Meta object facility (MOF) 2.0 Core Specification"},{"key":"e_1_2_1_2_37_2","unstructured":"Object Management Group (2013) OMG meta object facility (MOF) Core Specification Version 2.4.1"},{"key":"e_1_2_1_2_38_2","unstructured":"Object Management Group (2013) OMG unified modeling language TM (OMG UML) Version 2.5 38."},{"key":"e_1_2_1_2_39_2","unstructured":"Object Management Group (2014) Object constraint language Version 2.4"},{"key":"e_1_2_1_2_40_2","doi-asserted-by":"publisher","DOI":"10.1145\/361598.361623"},{"key":"e_1_2_1_2_41_2","doi-asserted-by":"crossref","unstructured":"Pham T-K-Z Dubois C L\u00e9vy N (2015) Towards correct-by-construction product variants of a software product line: Gfml a formal language for feature modules. In: Proceedings 6th workshop on formal methods and analysis in SPL engineering FMSPLE 2015 London 11 April 2015 pp 44\u201355","DOI":"10.4204\/EPTCS.182.4"},{"key":"e_1_2_1_2_42_2","unstructured":"Picard C Matthes R (2011) Coinductive graph representation : the problem of embedded lists. In: Electronic communications of the EASST special issue graph computation models GCM\u201910"},{"key":"e_1_2_1_2_43_2","doi-asserted-by":"crossref","unstructured":"Poernomo I (2006) The meta-object facility typed. In Hisham H (ed) SAC ACM pp 1845\u20131849","DOI":"10.1145\/1141277.1141710"},{"key":"e_1_2_1_2_44_2","doi-asserted-by":"crossref","unstructured":"Poernomo I (2008) Proofs-as-model-transformations. In: Antonio V Jeff G Alfonso P (eds)ICMT volume 5063 of Lecture Notes in Computer Science Springer New York pp 214\u2013228","DOI":"10.1007\/978-3-540-69927-9_15"},{"key":"e_1_2_1_2_45_2","doi-asserted-by":"crossref","unstructured":"Poernomo I Terrell J (2010) Correct-by-construction model transformations from partially ordered specifications in Coq. In: Dong JS Zhu H (eds) ICFEM volume 6447 of Lecture Notes in Computer Science Springer New York pp 56\u201373","DOI":"10.1007\/978-3-642-16901-4_6"},{"key":"e_1_2_1_2_46_2","unstructured":"Reddy R France R Ghosh S Fleurey F Baudry B (2005) Model composition: a signature-based approach. In: Aspect oriented modeling (AOM) Workshop"},{"key":"e_1_2_1_2_47_2","doi-asserted-by":"crossref","unstructured":"Reddy R Ghosh S France R Straw G Bieman J McEachen N Song E Georg G (2006) Directives for composing aspect-oriented design class models. In: Transactions on aspect-oriented software development I Springer New York pp 75\u2013105","DOI":"10.1007\/11687061_3"},{"key":"e_1_2_1_2_48_2","unstructured":"Schirmeier H Spinczyk O (2009) Challenges in software product line composition. In: 42nd Hawaii international conference on system sciences IEEE pp 1\u20137"},{"volume-title":"A survey on aspect-oriented modeling approaches","year":"2007","author":"Schauerhuber A","key":"e_1_2_1_2_49_2"},{"key":"e_1_2_1_2_50_2","unstructured":"Thirioux X Combemale B Cr\u00e9gut X Garoche P-L (2007) A framework to formalise the MDE foundations. In Richard P Jean B (eds) International Workshop on Towers of Models (TOWERS) Zurich pp 14\u201330"},{"key":"e_1_2_1_2_51_2","doi-asserted-by":"crossref","unstructured":"Troya J Vallecillo A (2010) Towards a rewriting logic semantics for ATL. In: Tratt L Gogolla M (eds) ICMT volume 6142 of Lecture Notes in Computer Science Springer New York pp 230\u2013244","DOI":"10.1007\/978-3-642-13688-7_16"},{"key":"e_1_2_1_2_52_2","doi-asserted-by":"publisher","DOI":"10.1109\/MS.2013.65"},{"key":"e_1_2_1_2_53_2","unstructured":"Zito A (2006) UML\u2019s package extension mechanism: taking a closer look at package merge. PhD thesis Queen\u2019s University"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-016-0354-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-016-0354-6\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-016-0354-6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T16:12:34Z","timestamp":1641485554000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-016-0354-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,5]]},"references-count":53,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2016,5]]}},"alternative-id":["10.1007\/s00165-016-0354-6"],"URL":"https:\/\/doi.org\/10.1007\/s00165-016-0354-6","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"type":"print","value":"0934-5043"},{"type":"electronic","value":"1433-299X"}],"subject":[],"published":{"date-parts":[[2016,5]]}}}