{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,11]],"date-time":"2026-02-11T18:15:30Z","timestamp":1770833730608,"version":"3.50.1"},"publisher-location":"Cham","reference-count":48,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319117362","type":"print"},{"value":"9783319117379","type":"electronic"}],"license":[{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-11737-9_16","type":"book-chapter","created":{"date-parts":[[2014,10,15]],"date-time":"2014-10-15T00:52:14Z","timestamp":1413334334000},"page":"235-250","source":"Crossref","is-referenced-by-count":4,"title":["A Formal Framework to Prove the Correctness of Model Driven Engineering Composition Operators"],"prefix":"10.1007","author":[{"given":"Mounira","family":"Kezadri Hamiaz","sequence":"first","affiliation":[]},{"given":"Marc","family":"Pantel","sequence":"additional","affiliation":[]},{"given":"Benoit","family":"Combemale","sequence":"additional","affiliation":[]},{"given":"Xavier","family":"Thirioux","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"16_CR1","doi-asserted-by":"crossref","unstructured":"A\u00dfmann, U.: Invasive software composition. Springer-Verlag New York Inc. (2003)","DOI":"10.1007\/978-3-662-05082-8"},{"key":"16_CR2","doi-asserted-by":"crossref","unstructured":"Barbier, F., Cast\u00e9ran, 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\u2013325 (2013)","DOI":"10.4018\/978-1-4666-4217-1.ch013"},{"key":"16_CR3","doi-asserted-by":"crossref","unstructured":"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\u201312. IEEE (2006)","DOI":"10.1109\/SEFM.2006.27"},{"key":"16_CR4","first-page":"844","volume":"10","author":"A. Baya","year":"2013","unstructured":"Baya, A., Asri, B.E.: Composing specific domains for large scale systems. Journal of Communication and Computer\u00a010, 844\u2013856 (2013)","journal-title":"Journal of Communication and Computer"},{"issue":"3","key":"16_CR5","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1049\/iet-sen.2009.0011","volume":"4","author":"S. Bensalem","year":"2010","unstructured":"Bensalem, S., Bozga, M., Nguyen, T., Sifakis, J.: Compositional verification for component-based systems and application. Software, IET\u00a04(3), 181\u2013193 (2010)","journal-title":"Software, IET"},{"issue":"4","key":"16_CR6","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1145\/369275.369289","volume":"29","author":"P. Bernstein","year":"2000","unstructured":"Bernstein, P., Halevy, A., Pottinger, R.: A vision for management of complex models. ACM Sigmod Record\u00a029(4), 55\u201363 (2000)","journal-title":"ACM Sigmod Record"},{"issue":"2","key":"16_CR7","first-page":"21","volume":"5","author":"J. B\u00e9zivin","year":"2004","unstructured":"B\u00e9zivin, J.: In search of a basic principle for model driven engineering. Novatica Journal, Special Issue\u00a05(2), 21\u201324 (2004)","journal-title":"Novatica Journal, Special Issue"},{"issue":"3-4","key":"16_CR8","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1007\/s00165-009-0140-9","volume":"22","author":"A. Boronat","year":"2010","unstructured":"Boronat, A., Meseguer, J.: An algebraic semantics for MOF. Formal Aspects of Computing\u00a022(3-4), 269\u2013296 (2010)","journal-title":"Formal Aspects of Computing"},{"key":"16_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1007\/3-540-45685-6_8","volume-title":"Theorem Proving in Higher Order Logics","author":"A.D. Brucker","year":"2002","unstructured":"Brucker, A.D., Wolff, B.: A proposal for a formal OCL semantics in isabelle\/HOL. In: Carre\u00f1o, V.A., Mu\u00f1oz, C.A., Tahar, S. (eds.) TPHOLs 2002. LNCS, vol.\u00a02410, pp. 99\u2013114. Springer, Heidelberg (2002)"},{"key":"16_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/978-3-540-78743-3_8","volume-title":"Fundamental Approaches to Software Engineering","author":"A.D. Brucker","year":"2008","unstructured":"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.\u00a04961, pp. 97\u2013100. Springer, Heidelberg (2008)"},{"key":"16_CR11","doi-asserted-by":"crossref","unstructured":"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\u201312. ACM (2006)","DOI":"10.1145\/1138304.1138307"},{"key":"16_CR12","unstructured":"Cengarle, M.V., Gr\u00f6nniger, H., Rumpe, B., Schindler, M.: System model semantics of class diagrams. Technische Universitat Braunschweig (2008)"},{"issue":"1","key":"16_CR13","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1016\/S0167-6423(02)00030-8","volume":"44","author":"S. Clarke","year":"2002","unstructured":"Clarke, S.: Extending standard UML with model composition semantics. Science of Computer Programming\u00a044(1), 71\u2013100 (2002)","journal-title":"Science of Computer Programming"},{"issue":"2","key":"16_CR14","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1016\/S0304-3975(01)00359-0","volume":"285","author":"M. Clavel","year":"2002","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Lincoln, P., Mart\u00ed-Oliet, N., Meseguer, J., Quesada, J.: Maude: specification and programming in rewriting logic. Theoretical Computer Science\u00a0285(2), 187\u2013243 (2002)","journal-title":"Theoretical Computer Science"},{"key":"16_CR15","unstructured":"Coquand, T., Huet, G., et al.: The calculus of constructions (1986)"},{"issue":"3","key":"16_CR16","doi-asserted-by":"publisher","first-page":"305","DOI":"10.1007\/s10270-008-0094-z","volume":"8","author":"M.D. Fabro Del","year":"2009","unstructured":"Del Fabro, M.D., Valduriez, P.: Towards the efficient development of model transformations using model weaving and matching transformations. Software and System Modeling\u00a08(3), 305\u2013324 (2009)","journal-title":"Software and System Modeling"},{"key":"16_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"106","DOI":"10.1007\/978-3-642-40229-6_8","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"M. Garnacho","year":"2013","unstructured":"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.\u00a08053, pp. 106\u2013120. Springer, Heidelberg (2013)"},{"key":"16_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1007\/978-3-642-20551-4_5","volume-title":"Logic-Based Program Synthesis and Transformation","author":"M. Giorgino","year":"2011","unstructured":"Giorgino, M., Strecker, M., Matthes, R., Pantel, M.: Verification of the schorr-waite algorithm \u2013 from trees to graphs. In: Alpuente, M. (ed.) LOPSTR 2010. LNCS, vol.\u00a06564, pp. 67\u201383. Springer, Heidelberg (2011)"},{"key":"16_CR19","doi-asserted-by":"crossref","unstructured":"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\u2013122 (2014)","DOI":"10.4204\/EPTCS.147.8"},{"issue":"3","key":"16_CR20","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1049\/iet-sen:20070060","volume":"2","author":"J. Henriksson","year":"2008","unstructured":"Henriksson, J., Heidenreich, F., Johannes, J., Zschaler, S., A\u00dfmann, U.: Extending grammars and metamodels for reuse: the Reuseware approach. Software, IET\u00a02(3), 165\u2013184 (2008)","journal-title":"Software, IET"},{"key":"16_CR21","doi-asserted-by":"crossref","unstructured":"Holt, J., Perry, S.: SysML for systems engineering, vol.\u00a07. IET (2008)","DOI":"10.1049\/PBPC007E"},{"key":"16_CR22","unstructured":"Jackson, D.: Software abstractions-logic, language, and analysis, revised edition (2012)"},{"key":"16_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/11768869_14","volume-title":"Formal Methods for Open Object-Based Distributed Systems","author":"F. Jouault","year":"2006","unstructured":"Jouault, F., B\u00e9zivin, J.: Km3: A dsl for metamodel specification. In: Gorrieri, R., Wehrheim, H. (eds.) FMOODS 2006. LNCS, vol.\u00a04037, pp. 171\u2013185. Springer, Heidelberg (2006)"},{"key":"16_CR24","unstructured":"Kezadri, M.: Assistance \u00e0 la validation et v\u00e9rification de syst\u00e8mes critiques: ontologies et int\u00e9gration de composants. PhD thesis (2013)"},{"key":"16_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/978-3-642-35743-5_14","volume-title":"Formal Aspects of Component Software","author":"M. Kezadri","year":"2012","unstructured":"Kezadri, M., Combemale, B., Pantel, M., Thirioux, X.: A proof assistant based formalization of MDE components. In: Arbab, F., \u00d6lveczky, P.C. (eds.) FACS 2011. LNCS, vol.\u00a07253, pp. 223\u2013240. Springer, Heidelberg (2012)"},{"issue":"4","key":"16_CR26","doi-asserted-by":"publisher","first-page":"369","DOI":"10.1007\/s10270-006-0017-9","volume":"5","author":"T. K\u00fchne","year":"2006","unstructured":"K\u00fchne, T.: Matters of (meta-) modeling. Software & Systems Modeling\u00a05(4), 369\u2013385 (2006)","journal-title":"Software & Systems Modeling"},{"issue":"3","key":"16_CR27","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1007\/s10270-011-0221-0","volume":"12","author":"J. Lara","year":"2013","unstructured":"Lara, J., Guerra, E.: From types to type requirements: genericity for model-driven engineering. Software and Systems Modeling\u00a012(3), 453\u2013474 (2013)","journal-title":"Software and Systems Modeling"},{"key":"16_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1007\/978-3-642-24485-8_12","volume-title":"Model Driven Engineering Languages and Systems","author":"S. Maoz","year":"2011","unstructured":"Maoz, S., Ringert, J.O., Rumpe, B.: Semantically configurable consistency analysis for class and object diagrams. In: Whittle, J., Clark, T., K\u00fchne, T. (eds.) MODELS 2011. LNCS, vol.\u00a06981, pp. 153\u2013167. Springer, Heidelberg (2011)"},{"key":"16_CR29","doi-asserted-by":"crossref","unstructured":"Morin, B., Klein, J., Barais, O., J\u00e9z\u00e9quel, J.-M.: A generic weaver for supporting product lines. In: Proceedings of the 13th International Workshop on Early Aspects, pp. 11\u201318. ACM (2008)","DOI":"10.1145\/1370828.1370832"},{"key":"16_CR30","doi-asserted-by":"crossref","unstructured":"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\u201364. IEEE Computer Society (2007)","DOI":"10.1109\/ICSE.2007.50"},{"key":"16_CR31","unstructured":"Object Management Group, Inc. Meta Object Facility (MOF) 2.0 Core Specification (January 2006); Final Adopted Specification."},{"key":"16_CR32","unstructured":"Object Management Group, Inc. Meta Object Facility (MOF) 2.4.2 Core Specification (January 2014)"},{"key":"16_CR33","unstructured":"O.\u00a0OMG. Unified modeling language (omg uml)-infrastructure(v2.4.1) (2011), http:\/\/www.omg.org\/spec\/UML\/2.4.1"},{"key":"16_CR34","unstructured":"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)"},{"key":"16_CR35","doi-asserted-by":"crossref","unstructured":"Poernomo, I.: The meta-object facility typed. In: Haddad, H. (ed.) SAC, pp. 1845\u20131849. ACM (2006)","DOI":"10.1145\/1141277.1141710"},{"key":"16_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"214","DOI":"10.1007\/978-3-540-69927-9_15","volume-title":"Theory and Practice of Model Transformations","author":"I. Poernomo","year":"2008","unstructured":"Poernomo, I.: Proofs-as-model-transformations. In: Vallecillo, A., Gray, J., Pierantonio, A. (eds.) ICMT 2008. LNCS, vol.\u00a05063, pp. 214\u2013228. Springer, Heidelberg (2008)"},{"key":"16_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"56","DOI":"10.1007\/978-3-642-16901-4_6","volume-title":"Formal Methods and Software Engineering","author":"I. Poernomo","year":"2010","unstructured":"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.\u00a06447, pp. 56\u201373. Springer, Heidelberg (2010)"},{"issue":"9","key":"16_CR38","doi-asserted-by":"publisher","first-page":"187","DOI":"10.5381\/jot.2007.6.9.a10","volume":"6","author":"J.R. Romero","year":"2007","unstructured":"Romero, J.R., Rivera, J.E., Dur\u00e1n, F., Vallecillo, A.: Formal and tool support for Model Driven Engineering with Maude. Journal of Object Technology\u00a06(9), 187\u2013207 (2007)","journal-title":"Journal of Object Technology"},{"key":"16_CR39","unstructured":"RTCA \/ EUROCAE. \u201cFormal Methods Supplement to DO-178C [ED-12C]\u201d, DO-333\/ED-218 (2011)"},{"key":"16_CR40","unstructured":"RTCA \/ EUROCAE. \u201cModel-Based Development and Verification Supplement to DO-178C [ED-12C]\u201d, DO-331\/ED-216 (2011)"},{"key":"16_CR41","unstructured":"RTCA \/ EUROCAE. \u201cSoftware Considerations in Airborne Systems and Equipment Certification\u201d, DO-178C\/ED-12C (2011)"},{"key":"16_CR42","unstructured":"RTCA \/ EUROCAE. \u201cDO-330\/ED-215: Software Tool Qualification Considerations\u201d - clarifying software tools and avionics tool qualification (2012)"},{"key":"16_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/978-3-642-02414-6_11","volume-title":"Component-Based Software Engineering","author":"S. Sentilles","year":"2009","unstructured":"Sentilles, S., \u0160t\u011bp\u00e1n, P., Carlson, J., Crnkovi\u0107, I.: Integration of extra-functional properties in component models. In: Lewis, G.A., Poernomo, I., Hofmeister, C. (eds.) CBSE 2009. LNCS, vol.\u00a05582, pp. 173\u2013190. Springer, Heidelberg (2009)"},{"key":"16_CR44","unstructured":"Thirioux, X., Combemale, B., Cr\u00e9gut, X., Garoche, P.-L.: A Framework to Formalise the MDE Foundations. In: Paige, R., B\u00e9zivin, J. (eds.) International Workshop on Towers of Models (TOWERS), Zurich, pp. 14\u201330 (June 2007)"},{"key":"16_CR45","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"230","DOI":"10.1007\/978-3-642-13688-7_16","volume-title":"Theory and Practice of Model Transformations","author":"J. Troya","year":"2010","unstructured":"Troya, J., Vallecillo, A.: Towards a rewriting logic semantics for ATL. In: Tratt, L., Gogolla, M. (eds.) ICMT 2010. LNCS, vol.\u00a06142, pp. 230\u2013244. Springer, Heidelberg (2010)"},{"key":"16_CR46","unstructured":"Warmer, J.B., Kleppe, A.G.: The object constraint language: getting your models ready for MDA. Addison-Wesley Professional (2003)"},{"issue":"5","key":"16_CR47","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1145\/949952.940109","volume":"28","author":"F. Xie","year":"2003","unstructured":"Xie, F., Browne, J.: Verified systems by composition from verified components. ACM SIGSOFT Software Engineering Notes\u00a028(5), 277\u2013286 (2003)","journal-title":"ACM SIGSOFT Software Engineering Notes"},{"key":"16_CR48","unstructured":"Zito, A.: UML\u2019s Package Extension Mechanism: Taking a Closer Look at Package Merge. Queen\u2019s University (2006)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-11737-9_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,5]],"date-time":"2025-05-05T04:24:58Z","timestamp":1746419098000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-11737-9_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319117362","9783319117379"],"references-count":48,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-11737-9_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014]]}}}