{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T13:30:31Z","timestamp":1742995831653,"version":"3.40.3"},"publisher-location":"Cham","reference-count":33,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031712609"},{"type":"electronic","value":"9783031712616"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"DOI":"10.1007\/978-3-031-71261-6_4","type":"book-chapter","created":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T19:02:03Z","timestamp":1725735723000},"page":"59-78","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Correct Pattern-Based Development Through Refinements and\u00a0Weakest Preconditions Calculus"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-9277-4024","authenticated-orcid":false,"given":"Elie","family":"Fares","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4179-6063","authenticated-orcid":false,"given":"Jean-Paul","family":"Bodeveix","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5387-6805","authenticated-orcid":false,"given":"Mamoun","family":"Filali","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,9,8]]},"reference":[{"key":"4_CR1","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, Cambridge (2010)","edition":"1"},{"issue":"6","key":"4_CR2","doi-asserted-by":"publisher","first-page":"447","DOI":"10.1007\/s10009-010-0145-y","volume":"12","author":"J-R Abrial","year":"2010","unstructured":"Abrial, J.-R., Butler, M., Hallerstede, S., Hoang, T.S., Mehta, F., Voisin, L.: Rodin: an open toolset for modelling and reasoning in Event-B. Int. J. Software Tools Technol. Transfer 12(6), 447\u2013466 (2010)","journal-title":"Int. J. Software Tools Technol. Transfer"},{"key":"4_CR3","doi-asserted-by":"crossref","unstructured":"Alkhammash, E., Butler, M., Fathabadi, A.S., C\u00eerstea, C.: Building traceable Event-B models from requirements. Sci. Comput. Programm. 111, 318\u2013338 (2015). Special Issue on Automated Verification of Critical Systems (AVoCS 2013)","DOI":"10.1016\/j.scico.2015.06.002"},{"key":"4_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"104","DOI":"10.1007\/978-3-642-00867-2_6","volume-title":"Methods, Models and Tools for Fault Tolerance","author":"E Ball","year":"2009","unstructured":"Ball, E., Butler, M.: Event-B patterns for specifying fault-tolerance in multi-agent interaction. In: Butler, M., Jones, C., Romanovsky, A., Troubitsyna, E. (eds.) Methods, Models and Tools for Fault Tolerance. LNCS, vol. 5454, pp. 104\u2013129. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-00867-2_6"},{"key":"4_CR5","unstructured":"Bettini, L.: Implementing Domain Specific Languages with Xtext and Xtend - Second Edition, 2nd edn. Packt Publishing (2016)"},{"key":"4_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1007\/978-3-030-77543-8_5","volume-title":"Rigorous State-Based Methods","author":"J-P Bodeveix","year":"2021","unstructured":"Bodeveix, J.-P., Filali, M.: Event-B formalization of event-B contexts. In: Raschke, A., M\u00e9ry, D. (eds.) ABZ 2021. LNCS, vol. 12709, pp. 66\u201380. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-77543-8_5"},{"key":"4_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"432","DOI":"10.1007\/11590156_35","volume-title":"FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science","author":"P Bouyer","year":"2005","unstructured":"Bouyer, P., Chevalier, F., Markey, N.: On the expressiveness of TPTL and MTL. In: Sarukkai, S., Sen, S. (eds.) FSTTCS 2005. LNCS, vol. 3821, pp. 432\u2013443. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11590156_35"},{"key":"4_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1007\/978-3-642-15898-8_3","volume-title":"Formal Methods for Industrial Critical Systems","author":"JW Bryans","year":"2010","unstructured":"Bryans, J.W., Wei, W.: Formal analysis of BPMN models using event-B. In: Kowalewski, S., Roveri, M. (eds.) FMICS 2010. LNCS, vol. 6371, pp. 33\u201349. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-15898-8_3"},{"key":"4_CR9","doi-asserted-by":"publisher","first-page":"130","DOI":"10.1016\/j.scico.2014.04.012","volume":"94","author":"D D\u00e9harbe","year":"2014","unstructured":"D\u00e9harbe, D., Fontaine, P., Guyot, Y., Voisin, L.: Integrating SMT solvers in Rodin. Sci. Comput. Program. 94, 130\u2013143 (2014)","journal-title":"Sci. Comput. Program."},{"issue":"5","key":"4_CR10","doi-asserted-by":"publisher","first-page":"861","DOI":"10.1145\/365151.365169","volume":"22","author":"A Dovier","year":"2000","unstructured":"Dovier, A., Piazza, C., Pontelli, E., Rossi, G.: Sets and constraint logic programming. ACM Trans. Program. Lang. Syst. 22(5), 861\u2013931 (2000)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"4_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1007\/978-3-031-33163-3_3","volume-title":"Rigorous State-Based Methods","author":"E Fares","year":"2023","unstructured":"Fares, E., Bodeveix, P.J., Filali, M.: Pattern-based refinement generation through domain specific languages. In: Gl\u00e4sser, U., Creissac Campos, J., M\u00e9ry, D., Palanque, P. (eds.) ABZ 2023. Pattern-based refinement generation through domain specific languages, vol. 14010, pp. 35\u201342. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-33163-3_3"},{"key":"4_CR12","unstructured":"Farrell, M.: Event-B in the institutional framework: defining a semantics, modularisation constructs and interoperability for a specification language (2017)"},{"key":"4_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1007\/978-3-031-33163-3_19","volume-title":"Rigorous State-Based Methods","author":"M Farrell","year":"2023","unstructured":"Farrell, M., Monahan, R., Power, J.F.: Building specifications in\u00a0the\u00a0Event-B institution: a summary. In: Gl\u00e4sser, U., Creissac Campos, J., M\u00e9ry, D., Palanque, P. (eds.) ABZ 2023. LNCS, vol. 14010, pp. 245\u2013253. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-33163-3_19"},{"key":"4_CR14","volume-title":"Domain-Specific Languages","author":"M Fowler","year":"2010","unstructured":"Fowler, M.: Domain-Specific Languages. Addison-Wesley, Upper Saddle River (2010)"},{"key":"4_CR15","unstructured":"Gamma, E., Helm, R., Johnson, R., Vlissides, J.M.: Design Patterns: Elements of Reusable Object-Oriented Software, 1st edn. Addison-Wesley Professional (1994)"},{"key":"4_CR16","unstructured":"Guillaume\u00a0Verdier, L.V.: Context instantiation plug-in: a new approach to genericity in Rodin. In: Proceedings of the 9th Rodin User and Developer Workshop (2021)"},{"key":"4_CR17","unstructured":"Hoang, T.S.: An introduction to the Event-B modelling method. In: Romanovsky, A., Thomas, M. (eds.) Industrial Deployment of System Engineering Methods, pp. 211\u2013236. Springer, Cham (2013). http:\/\/www.springer.com\/computer\/swe\/book\/978-3-642-33169-5"},{"key":"4_CR18","doi-asserted-by":"crossref","unstructured":"Hoang, T.S., F\u00fcrst, A., Abrial, J.-R.: Event-B patterns and their tool support. In: Hung, D.V., Krishnan, P. (eds.) Seventh IEEE International Conference on Software Engineering and Formal Methods, SEFM 2009, Hanoi, Vietnam, 23\u201327 November 2009, pp. 210\u2013219. IEEE Computer Society (2009)","DOI":"10.1109\/SEFM.2009.17"},{"key":"4_CR19","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. Software Syst. Model. 12, 229\u2013244 (2013)","journal-title":"Software Syst. Model."},{"key":"4_CR20","doi-asserted-by":"publisher","unstructured":"Hoang, T.S., Snook, C., Dghaym, D., Fathabadi, A.S., Butler, M.: Building an extensible textual framework for the Rodin platform. In: Masci, P., Bernardeschi, C., Graziani, P., Koddenbrock, M., Palmieri, M. (eds.) SEFM 2022. LNCS, vol. 13765, pp. 132\u2013147. Springer, Heidelberg (2023). https:\/\/doi.org\/10.1007\/978-3-031-26236-4_11","DOI":"10.1007\/978-3-031-26236-4_11"},{"key":"4_CR21","unstructured":"Hoang, T.S., Voisin, L., Salehi,A., Butler, M.J., Wilkinson, T., Beauger, N.: Theory plug-in for rodin 3.x. CoRR, abs\/1701.08625 (2017)"},{"key":"4_CR22","unstructured":"Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall International Series in Computer Science. Prentice Hall (1985)"},{"key":"4_CR23","doi-asserted-by":"crossref","unstructured":"Iliasov, A., Troubitsyna, E., Laibinis, L., Romanovsky, A.B.: Patterns for refinement automation. 6286, 70\u201388 (2009)","DOI":"10.1007\/978-3-642-17071-3_4"},{"key":"4_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"357","DOI":"10.1007\/978-3-030-02450-5_21","volume-title":"Formal Methods and Software Engineering","author":"T Kobayashi","year":"2018","unstructured":"Kobayashi, T., Ishikawa, F.: Analysis on strategies of superposition refinement of event-B specifications. In: Sun, J., Sun, M. (eds.) ICFEM 2018. LNCS, vol. 11232, pp. 357\u2013372. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-02450-5_21"},{"key":"4_CR25","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1007\/11916246_13","volume-title":"Rigorous Development of Fault-Tolerant Agent Systems","author":"L Laibinis","year":"2006","unstructured":"Laibinis, L., Troubitsyna, E., Iliasov, A., Romanovsky, A.: Rigorous Development of Fault-Tolerant Agent Systems, pp. 241\u2013260. Springer, Heidelberg (2006)"},{"key":"4_CR26","doi-asserted-by":"crossref","unstructured":"\u00d6lveczky, P.C., Meseguer, J.: Specifying real-time systems in rewriting logic. In: Meseguer, J. (ed.) Electronic Notes in Theoretical Computer Science, volume\u00a04. Elsevier Science Publishers (2000)","DOI":"10.1016\/S1571-0661(04)00044-1"},{"key":"4_CR27","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":"4_CR28","unstructured":"http:\/\/www.event-b.org\/"},{"key":"4_CR29","unstructured":"https:\/\/wiki.event-b.org\/index.php\/Set_Rewrite_Rules"},{"key":"4_CR30","doi-asserted-by":"publisher","unstructured":"Siala, B., Bhiri, M.T.: An automatic refinement for event-B through annotated temporal logic patterns. In: Nguyen, N.T., Manolopoulos, Y., Chbeir, R., Kozierkiewicz, A., Trawinski, B. (eds.) ICCCI 2022. LNCS, vol. 13501, pp. 624\u2013637. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-16014-1_49","DOI":"10.1007\/978-3-031-16014-1_49"},{"key":"4_CR31","doi-asserted-by":"crossref","unstructured":"Siala, B., Bodeveix, J.-P., Filali, M., Bhiri, M.T.: Automatic refinement for Event-B through annotated patterns. In: Kotenko, I.V., Cotronis, Y., Daneshtalab, M. (eds.) 25th Euromicro International Conference on Parallel, Distributed and Network-based Processing, PDP 2017, St. Petersburg, Russia, March 6\u20138, 2017, pp. 287\u2013290. IEEE Computer Society (2017)","DOI":"10.1109\/PDP.2017.72"},{"key":"4_CR32","doi-asserted-by":"crossref","unstructured":"Silva, R.: Towards the composition of specifications in Event-B. In: Proceedings of the B 2011 Workshop, a satellite event of the 17th International Symposium on Formal Methods (FM 2011), Electronic Notes in Theoretical Computer Science, vol. 280, pp. 81\u201393 (2011)","DOI":"10.1016\/j.entcs.2011.11.020"},{"key":"4_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"122","DOI":"10.1007\/978-3-642-25271-6_7","volume-title":"Formal Methods for Components and Objects","author":"R Silva","year":"2011","unstructured":"Silva, R., Butler, M.: Shared event composition\/decomposition in event-B. In: Aichernig, B.K., de Boer, F.S., Bonsangue, M.M. (eds.) FMCO 2010. LNCS, vol. 6957, pp. 122\u2013141. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-25271-6_7"}],"container-title":["Lecture Notes in Computer Science","Formal Aspects of Component Software"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-71261-6_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T19:02:41Z","timestamp":1725735761000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-71261-6_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031712609","9783031712616"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-71261-6_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"8 September 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"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":"Milan","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9 September 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10 September 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"facs2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/facs-conference.github.io\/2024\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}