{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T00:52:41Z","timestamp":1740099161106,"version":"3.37.3"},"publisher-location":"Cham","reference-count":28,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030021450"},{"type":"electronic","value":"9783030021467"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-030-02146-7_3","type":"book-chapter","created":{"date-parts":[[2018,10,5]],"date-time":"2018-10-05T21:44:02Z","timestamp":1538775842000},"page":"54-74","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Event-B Formalization of a Variability-Aware Component Model Patterns Framework"],"prefix":"10.1007","author":[{"given":"Jean-Paul","family":"Bodeveix","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Arnaud","family":"Dieumegard","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mamoun","family":"Filali","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,10,5]]},"reference":[{"key":"3_CR1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511624162","volume-title":"The B-book: Assigning Programs to Meanings","author":"J-R Abrial","year":"1996","unstructured":"Abrial, J.-R.: The B-book: Assigning Programs to Meanings. Cambridge University Press, New York (1996)"},{"key":"3_CR2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139195881","volume-title":"Modeling in Event-B: System and Software Engineering","author":"J-R Abrial","year":"2010","unstructured":"Abrial, J.-R.: Modeling in Event-B: System and Software Engineering, 1st edn. Cambridge University Press, New York (2010)","edition":"1"},{"key":"3_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1007\/3-540-60973-3_108","volume-title":"FME\u201996: Industrial Benefit and Advances in Formal Methods","author":"PSC Alencar","year":"1996","unstructured":"Alencar, P.S.C., Cowan, D.D., Lucena, C.J.P.: A formal approach to architectural design patterns. In: Gaudel, M.-C., Woodcock, J. (eds.) FME 1996. LNCS, vol. 1051, pp. 576\u2013594. Springer, Heidelberg (1996). https:\/\/doi.org\/10.1007\/3-540-60973-3_108"},{"key":"3_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1007\/11925040_8","volume-title":"Leveraging Applications of Formal Methods","author":"PA Abdulla","year":"2006","unstructured":"Abdulla, P.A., Deneux, J., St\u00e5lmarck, G., \u00c5gren, H., \u00c5kerlund, O.: Designing safe, reliable systems using scade. In: Margaria, T., Steffen, B. (eds.) ISoLA 2004. LNCS, vol. 4313, pp. 115\u2013129. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11925040_8"},{"issue":"3","key":"3_CR5","doi-asserted-by":"publisher","first-page":"329","DOI":"10.1017\/S0960129504004153","volume":"14","author":"F Arbab","year":"2004","unstructured":"Arbab, F.: Reo: a channel-based coordination model for component composition. Math. Struct. Comput. Sci. 14(3), 329\u2013366 (2004)","journal-title":"Math. Struct. Comput. Sci."},{"issue":"3","key":"3_CR6","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1109\/MS.2011.27","volume":"28","author":"A Basu","year":"2011","unstructured":"Basu, A., Bensalem, S., Bozga, M., Combaz, J., Jaber, M., Nguyen, T.-H., Sifakis, J.: Rigorous component-based system design using the BIP framework. IEEE Softw. 28(3), 41\u201348 (2011)","journal-title":"IEEE Softw."},{"issue":"3","key":"3_CR7","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/s10817-009-9148-3","volume":"43","author":"S Blazy","year":"2009","unstructured":"Blazy, S., Leroy, X.: Mechanized semantics for the clight subset of the C language. J. Autom. Reason. 43(3), 263\u2013288 (2009)","journal-title":"J. Autom. Reason."},{"issue":"1","key":"3_CR8","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1002\/j.2334-5837.2015.00048.x","volume":"25","author":"Ronald S. Carson","year":"2015","unstructured":"Carson, R.S.: Implementing structured requirements to improve requirements quality. In: INCOSE International Symposium, vol. 25, pp. 54\u201367. Wiley Online Library (2015)","journal-title":"INCOSE International Symposium"},{"key":"3_CR9","series-title":"SIGS Management Briefings","volume-title":"Software Patterns","author":"JO Coplien","year":"1996","unstructured":"Coplien, J.O.: Software Patterns. SIGS Management Briefings. SIGS books & multimedia, New York (1996)"},{"key":"3_CR10","doi-asserted-by":"crossref","unstructured":"Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Patterns in property specifications for finite-state verification. In: Proceedings of the ICSE\u2019 99, Los Angeles, CA, USA, May 16\u201322, pp. 411\u2013420 (1999)","DOI":"10.1145\/302405.302672"},{"issue":"11","key":"3_CR11","doi-asserted-by":"publisher","first-page":"1755","DOI":"10.1016\/j.jss.2007.03.005","volume":"80","author":"J Dong","year":"2007","unstructured":"Dong, J., Alencar, P.S.C., Cowan, D.D., Yang, S.: Composing pattern-based components and verifying correctness. J. Syst. Softw. 80(11), 1755\u20131769 (2007)","journal-title":"J. Syst. Softw."},{"key":"3_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1007\/978-3-540-88194-0_5","volume-title":"Formal Methods and Software Engineering","author":"K Damchoom","year":"2008","unstructured":"Damchoom, K., Butler, M., Abrial, J.-R.: Modelling and proof of a tree-structured file system in event-b and rodin. In: Liu, S., Maibaum, T., Araki, K. (eds.) ICFEM 2008. LNCS, vol. 5256, pp. 25\u201344. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-88194-0_5"},{"key":"3_CR13","doi-asserted-by":"crossref","unstructured":"Denney, E., Pai, G., Whiteside, I.: Model-driven development of safety architectures. In: 20th ACM\/IEEE International Conference on Model Driven Engineering Languages and Systems, MODELS 2017, Austin, TX, USA, September 17\u201322, 2017, pp. 156\u2013166. IEEE Computer Society (2017)","DOI":"10.1109\/MODELS.2017.27"},{"key":"3_CR14","series-title":"SEI Series in Software Engineering","volume-title":"Model-Based Engineering with AADL - An Introduction to the SAE Architecture Analysis and Design Language","author":"PH Feiler","year":"2012","unstructured":"Feiler, P.H., Gluch, D.P.: Model-Based Engineering with AADL - An Introduction to the SAE Architecture Analysis and Design Language. SEI Series in Software Engineering. Addison-Wesley, Upper Saddle River (2012)"},{"issue":"2","key":"3_CR15","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1007\/s10270-010-0183-7","volume":"12","author":"TS Hoang","year":"2013","unstructured":"Hoang, T.S., F\u00fcrst, A., Abrial, J.-R.: Event-B patterns and their tool support. Softw. Syst. Model. 12(2), 229\u2013244 (2013)","journal-title":"Softw. Syst. Model."},{"key":"3_CR16","volume-title":"The VHDL Reference: A Practical Guide to Computer-Aided Integrated Circuit Design (Including VHDL-AMS) with Other","author":"U Heinkel","year":"2000","unstructured":"Heinkel, U., Glauert, W., Wahl, M.: The VHDL Reference: A Practical Guide to Computer-Aided Integrated Circuit Design (Including VHDL-AMS) with Other. Wiley, New York (2000)"},{"key":"3_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1007\/978-3-642-17071-3_4","volume-title":"Formal Methods for Components and Objects","author":"A Iliasov","year":"2010","unstructured":"Iliasov, A., Troubitsyna, E., Laibinis, L., Romanovsky, A.: Patterns for refinement automation. In: de Boer, F.S., Bonsangue, M.M., Hallerstede, S., Leuschel, M. (eds.) FMCO 2009. LNCS, vol. 6286, pp. 70\u201388. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-17071-3_4"},{"key":"3_CR18","doi-asserted-by":"crossref","unstructured":"Kang, K., Cohen, S., Hess, J., Novak, W., Peterson, A.: Feature-oriented domain analysis (foda) feasibility study. Technical Report CMU\/SEI-90-TR-021, Software Engineering Institute, Carnegie Mellon University, Pittsburgh, PA (1990)","DOI":"10.21236\/ADA235785"},{"key":"3_CR19","volume-title":"Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers","author":"L Lamport","year":"2002","unstructured":"Lamport, L.: Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley, Boston (2002)"},{"key":"3_CR20","doi-asserted-by":"publisher","first-page":"16","DOI":"10.4204\/EPTCS.245.2","volume":"245","author":"Diego Marmsoler","year":"2017","unstructured":"Marmsoler, D., Degenhardt, S.: Verifying patterns of dynamic architectures using model checking. In: Kofron, J., Tumova, J. (eds.) Proceedings International Workshop on Formal Engineering approaches to Software Components and Architectures, FESCA@ETAPS 2017, Uppsala, Sweden, 22nd April 2017, vol. 245 of EPTCS, pp. 16\u201330 (2017)","journal-title":"Electronic Proceedings in Theoretical Computer Science"},{"key":"3_CR21","unstructured":"OMG. OMG Systems Modeling Language (OMG SysML), Version 1.3 (2012)"},{"key":"3_CR22","doi-asserted-by":"crossref","unstructured":"Preschern, C., Kajtazovic, N., Kreiner, C.: Building a safety architecture pattern system. In: Proceedings of the 18th European Conference on Pattern Languages of Program, EuroPLoP \u201913, pp. 17:1\u201317:55, ACM, New York, NY, USA (2015)","DOI":"10.1145\/2739011.2739028"},{"key":"3_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/BFb0054170","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Pnueli","year":"1998","unstructured":"Pnueli, A., Siegel, M., Singerman, E.: Translation validation. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol. 1384, pp. 151\u2013166. Springer, Heidelberg (1998). https:\/\/doi.org\/10.1007\/BFb0054170"},{"key":"3_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"345","DOI":"10.1007\/978-3-540-87603-8_33","volume-title":"Abstract State Machines, B and Z","author":"A Requet","year":"2008","unstructured":"Requet, A.: BART: a tool for automatic refinement. In: B\u00f6rger, E., Butler, M., Bowen, J.P., Boca, P. (eds.) ABZ 2008. LNCS, vol. 5238, pp. 345\u2013345. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-87603-8_33"},{"key":"3_CR25","unstructured":"Rumbaugh, J., Jacobson, I., Booch, G.: Unified Modeling Language Reference Manual, 2nd edn. Pearson Higher Education (2004)"},{"key":"3_CR26","unstructured":"http:\/\/www.event-b.org\/"},{"key":"3_CR27","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1007\/978-3-319-49103-5_22","volume-title":"Complex Systems Design & Management","author":"M Sango","year":"2016","unstructured":"Sango, M., Vall\u00e9e, F., Vi\u00e9, A.-C., Voirin, J.-L., Leroux, X., Normand, V.: MBSE and MBSA with Capella and safety architect tools. In: Fanmuy, G., Goubault, E., Krob, D., Stephan, F. (eds.) CSDM 2016, p. 239. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-49103-5_22"},{"key":"3_CR28","unstructured":"Voirin, J.L.: Model-based System and Architecture Engineering with the Arcadia Method. Elsevier Science (2017)"}],"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-030-02146-7_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,25]],"date-time":"2019-10-25T11:40:27Z","timestamp":1572003627000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-02146-7_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783030021450","9783030021467"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-02146-7_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]},"assertion":[{"value":"FACS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Formal Aspects of Component Software","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Pohang","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Korea (Republic of)","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2018","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10 October 2018","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12 October 2018","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"facs2018","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/sevlab.postech.ac.kr\/facs18","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}