{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,24]],"date-time":"2025-04-24T04:32:21Z","timestamp":1745469141492,"version":"3.40.4"},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642357428"},{"type":"electronic","value":"9783642357435"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-35743-5_14","type":"book-chapter","created":{"date-parts":[[2012,12,14]],"date-time":"2012-12-14T01:40:42Z","timestamp":1355449242000},"page":"223-240","source":"Crossref","is-referenced-by-count":3,"title":["A Proof Assistant Based Formalization of MDE Components"],"prefix":"10.1007","author":[{"given":"Mounira","family":"Kezadri","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Beno\u00eet","family":"Combemale","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marc","family":"Pantel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xavier","family":"Thirioux","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"14_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":"14_CR2","unstructured":"Azurat, A.: Mechanization of invasive software composition in F-logic. In: Proceedings of the 2007 Annual Conference on International Conference on Computer Engineering and Applications, pp. 89\u201394. World Scientific and Engineering Academy and Society, WSEAS (2007)"},{"key":"14_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"},{"issue":"3","key":"14_CR4","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. IET Software\u00a04(3), 181\u2013193 (2010)","journal-title":"IET Software"},{"issue":"4","key":"14_CR5","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":"3-4","key":"14_CR6","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 Asp. Comput.\u00a022(3-4), 269\u2013296 (2010)","journal-title":"Formal Asp. Comput."},{"issue":"1","key":"14_CR7","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":"14_CR8","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":"14_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1007\/978-3-642-19811-3_9","volume-title":"Fundamental Approaches to Software Engineering","author":"P. Crouzen","year":"2011","unstructured":"Crouzen, P., Lang, F.: Smart Reduction. In: Giannakopoulou, D., Orejas, F. (eds.) FASE 2011. LNCS, vol.\u00a06603, pp. 111\u2013126. Springer, Heidelberg (2011)"},{"issue":"3","key":"14_CR10","doi-asserted-by":"publisher","first-page":"305","DOI":"10.1007\/s10270-008-0094-z","volume":"8","author":"M.D.D. Fabro","year":"2009","unstructured":"Fabro, M.D.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":"14_CR11","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":"14_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/978-3-642-03764-1_2","volume-title":"Transactions on Aspect-Oriented Software Development VI","author":"F. Heidenreich","year":"2009","unstructured":"Heidenreich, F., Henriksson, J., Johannes, J., Zschaler, S.: On Language-Independent Model Modularisation. In: Katz, S., Ossher, H., France, R., J\u00e9z\u00e9quel, J.-M. (eds.) Transactions on Aspect-Oriented Software Development VI. LNCS, vol.\u00a05560, pp. 39\u201382. Springer, Heidelberg (2009)"},{"key":"14_CR13","unstructured":"Henriksson, J.: A Lightweight Framework for Universal Fragment Composition with an application in the Semantic Web, PhD thesis. TU Dresden (January 2009)"},{"key":"14_CR14","unstructured":"Jeanneret, C.: An Analysis of Model Composition Approaches. Master\u2019s thesis. Ecole Polytechnique F\u00e9d\u00e9rale de Lausanne (2007-2008)"},{"key":"14_CR15","unstructured":"Johannes, J.: Component-Based Model-Driven Software Development. Ph.D. thesis, vorgelegt an der Technischen Universit\u00e4t Dresden Fakult\u00e4t Informatik (2011)"},{"key":"14_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"220","DOI":"10.1007\/BFb0053381","volume-title":"ECOOP \u201997 - Object-Oriented Programming","author":"G. Kiczales","year":"1997","unstructured":"Kiczales, G., Lamping, J., Menhdhekar, A., Maeda, C., Lopes, C., Loingtier, J.M., Irwin, J.: Aspect-Oriented Programming. In: Aksit, M., Auletta, V. (eds.) ECOOP 1997. LNCS, vol.\u00a01241, pp. 220\u2013242. Springer, Heidelberg (1997)"},{"issue":"4","key":"14_CR17","doi-asserted-by":"publisher","first-page":"741","DOI":"10.1145\/210332.210335","volume":"42","author":"M. Kifer","year":"1995","unstructured":"Kifer, M., Lausen, G., Wu, J.: Logical foundations of object-oriented and frame-based languages. Journal of the ACM\u00a042(4), 741\u2013843 (1995)","journal-title":"Journal of the ACM"},{"issue":"1-2","key":"14_CR18","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1016\/j.scico.2004.11.005","volume":"56","author":"M. Lumpe","year":"2005","unstructured":"Lumpe, M., Schneider, J.: A form-based meta-model for software composition. Science of Computer Programming\u00a056(1-2), 59\u201378 (2005)","journal-title":"Science of Computer Programming"},{"key":"14_CR19","unstructured":"Object Management Group, Inc.: Meta Object Facility (MOF) 2.0 Core Specification (January 2006), http:\/\/www.omg.org\/docs\/formal\/06-01-01.pdf (final Adopted Specification)"},{"key":"14_CR20","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":"14_CR21","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":"14_CR22","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":"14_CR23","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":"14_CR24","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":"14_CR25","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":"14_CR26","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)"},{"issue":"5","key":"14_CR27","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"}],"container-title":["Lecture Notes in Computer Science","Formal Aspects of Component Software"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-35743-5_14.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,23]],"date-time":"2025-04-23T17:54:17Z","timestamp":1745430857000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-35743-5_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642357428","9783642357435"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-35743-5_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}