{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,30]],"date-time":"2026-07-30T18:04:38Z","timestamp":1785434678871,"version":"3.56.0"},"reference-count":41,"publisher":"Elsevier BV","license":[{"start":{"date-parts":[[2027,1,1]],"date-time":"2027-01-01T00:00:00Z","timestamp":1798761600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2027,1,1]],"date-time":"2027-01-01T00:00:00Z","timestamp":1798761600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/legal\/tdmrep-license"},{"start":{"date-parts":[[2027,1,1]],"date-time":"2027-01-01T00:00:00Z","timestamp":1798761600000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-017"},{"start":{"date-parts":[[2027,1,1]],"date-time":"2027-01-01T00:00:00Z","timestamp":1798761600000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-037"},{"start":{"date-parts":[[2027,1,1]],"date-time":"2027-01-01T00:00:00Z","timestamp":1798761600000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-012"},{"start":{"date-parts":[[2027,1,1]],"date-time":"2027-01-01T00:00:00Z","timestamp":1798761600000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2027,1,1]],"date-time":"2027-01-01T00:00:00Z","timestamp":1798761600000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-004"}],"content-domain":{"domain":["elsevier.com","sciencedirect.com"],"crossmark-restriction":true},"short-container-title":["Science of Computer Programming"],"published-print":{"date-parts":[[2027,1]]},"DOI":"10.1016\/j.scico.2026.103550","type":"journal-article","created":{"date-parts":[[2026,7,27]],"date-time":"2026-07-27T06:10:46Z","timestamp":1785132646000},"page":"103550","update-policy":"https:\/\/doi.org\/10.1016\/elsevier_cm_policy","source":"Crossref","is-referenced-by-count":0,"special_numbering":"C","title":["Correct pattern-based development through refinements and predicate transformers"],"prefix":"10.1016","volume":"255","author":[{"given":"Elie","family":"Fares","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jean-Paul","family":"Bodeveix","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Mamoun","family":"Filali","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"78","reference":[{"key":"10.1016\/j.scico.2026.103550_bib0001","series-title":"Modeling in Event-B: System and Software Engineering","author":"Abrial","year":"2010"},{"key":"10.1016\/j.scico.2026.103550_bib0002","unstructured":"Rodin, http:\/\/www.event-b.org\/."},{"key":"10.1016\/j.scico.2026.103550_bib0003","unstructured":"T.S. Hoang, CamilleX user guide, https:\/\/wiki.event-b.org\/index.php\/CamilleX_User_Guide."},{"key":"10.1016\/j.scico.2026.103550_bib0004","series-title":"Rigorous State-Based Methods - 9th International Conference, ABZ 2023, Nancy, France, May 30- June 2, 2023, Proceedings","first-page":"35","article-title":"Pattern-based refinement generation through domain specific languages","volume":"14010","author":"Fares","year":"2023"},{"key":"10.1016\/j.scico.2026.103550_bib0005","series-title":"Formal Aspects of Component Software - 20th International Conference, FACS 2024, Milan, Italy, September 9-10, 2024, Proceedings","first-page":"59","article-title":"Correct pattern-based development through refinements and weakest preconditions calculus","volume":"15189","author":"Fares","year":"2024"},{"issue":"6","key":"10.1016\/j.scico.2026.103550_bib0006","doi-asserted-by":"crossref","first-page":"447","DOI":"10.1007\/s10009-010-0145-y","article-title":"Rodin: an open toolset for modelling and reasoning in Event-B","volume":"12","author":"Abrial","year":"2010","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"10.1016\/j.scico.2026.103550_bib0007","series-title":"Formal Methods and Software Engineering","first-page":"357","article-title":"Analysis on strategies of superposition refinement of Event-B specifications","author":"Kobayashi","year":"2018"},{"key":"10.1016\/j.scico.2026.103550_bib0008","series-title":"Industrial Deployment of System Engineering Methods","first-page":"211","article-title":"An introduction to the Event-B modelling method","author":"Hoang","year":"2013"},{"key":"10.1016\/j.scico.2026.103550_bib0009","doi-asserted-by":"crossref","first-page":"130","DOI":"10.1016\/j.scico.2014.04.012","article-title":"Integrating SMT solvers in Rodin","volume":"94","author":"D\u00e9harbe","year":"2014","journal-title":"Sci. Comput. Program."},{"key":"10.1016\/j.scico.2026.103550_bib0010","doi-asserted-by":"crossref","first-page":"81","DOI":"10.1016\/j.entcs.2011.11.020","article-title":"Towards the composition of specifications in Event-B","volume":"280","author":"Silva","year":"2011","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"10.1016\/j.scico.2026.103550_bib0011","series-title":"Formal Methods for Components and Objects","first-page":"122","article-title":"Shared event composition\/decomposition in Event-B","author":"Silva","year":"2012"},{"key":"10.1016\/j.scico.2026.103550_bib0012","article-title":"Communicating Sequential Processes","author":"Hoare","year":"1985"},{"key":"10.1016\/j.scico.2026.103550_bib0013","series-title":"Software Engineering and Formal Methods. SEFM 2022 Collocated Workshops: AI4EA, F-IDE, CoSim-CPS, CIFMA, Berlin, Germany, September 26\u201330, 2022, Revised Selected Papers","first-page":"132","article-title":"Building an extensible textual framework for the Rodin platform","author":"Hoang","year":"2023"},{"key":"10.1016\/j.scico.2026.103550_bib0014","series-title":"Implementing Domain Specific Languages with Xtext and Xtend - Second Edition","author":"Bettini","year":"2016"},{"key":"10.1016\/j.scico.2026.103550_bib0015","unstructured":"Rodin rewrite rules, https:\/\/wiki.event-b.org\/index.php\/Set_Rewrite_Rules."},{"key":"10.1016\/j.scico.2026.103550_bib0016","unstructured":"T.S. Hoang, L. Voisin, A. Salehi, M.J. Butler, T. Wilkinson, N. Beauger, Theory plug-in for Rodin 3.x, (2017). arXiv: 1701.08625."},{"key":"10.1016\/j.scico.2026.103550_bib0017","unstructured":"Rodin proof tactics, https:\/\/wiki.event-b.org\/index.php\/Rodin_Proof_Tactics."},{"issue":"10","key":"10.1016\/j.scico.2026.103550_bib0018","doi-asserted-by":"crossref","first-page":"1315","DOI":"10.1109\/TC.2008.26","article-title":"The algebra of connectors-structuring interaction in BIP","volume":"57","author":"Bliudze","year":"2008","journal-title":"IEEE Trans. Comput."},{"key":"10.1016\/j.scico.2026.103550_bib0019","unstructured":"CaseStudies, https:\/\/github.com\/efares1\/EventB."},{"key":"10.1016\/j.scico.2026.103550_bib0020","series-title":"Seventh IEEE International Conference on Software Engineering and Formal Methods, SEFM 2009, Hanoi, Vietnam, 23-27 November 2009","first-page":"210","article-title":"Event-B patterns and their tool support","author":"Hoang","year":"2009"},{"key":"10.1016\/j.scico.2026.103550_bib0021","unstructured":"A. F\u00fcrst, T.S. Hoang, J.-R. Abrial, Pattern, 2012, Event-B Wiki, ETH Zurich. Last modified 24 January 2012. https:\/\/wiki.event-b.org\/index.php\/Pattern."},{"key":"10.1016\/j.scico.2026.103550_bib0022","series-title":"Formal Methods for Components and Objects","first-page":"70","article-title":"Patterns for refinement automation","author":"Iliasov","year":"2010"},{"key":"10.1016\/j.scico.2026.103550_bib0023","series-title":"Rigorous Development of Fault-Tolerant Agent Systems","first-page":"241","author":"Laibinis","year":"2006"},{"key":"10.1016\/j.scico.2026.103550_bib0024","series-title":"Abstract State Machines, B and Z: First International Conference, ABZ 2008, London, UK","first-page":"345","article-title":"BART: a tool for automatic refinement","author":"Requet","year":"2008"},{"key":"10.1016\/j.scico.2026.103550_bib0025","doi-asserted-by":"crossref","first-page":"229","DOI":"10.1007\/s10270-010-0183-7","article-title":"Event-B patterns and their tool support","volume":"12","author":"Hoang","year":"2013","journal-title":"Softw. Syst. Model."},{"key":"10.1016\/j.scico.2026.103550_bib0026","doi-asserted-by":"crossref","first-page":"318","DOI":"10.1016\/j.scico.2015.06.002","article-title":"Building traceable Event-B models from requirements","volume":"111","author":"Alkhammash","year":"2015","journal-title":"Sci. Comput. Program."},{"key":"10.1016\/j.scico.2026.103550_bib0027","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"33","DOI":"10.1007\/978-3-642-15898-8_3","article-title":"Formal analysis of BPMN models using Event-B","volume":"6371","author":"Bryans","year":"2010"},{"key":"10.1016\/j.scico.2026.103550_bib0028","series-title":"Methods, Models and Tools for Fault Tolerance","first-page":"104","article-title":"Event-B patterns for specifying fault-tolerance in multi-agent interaction","volume":"5454","author":"Ball","year":"2009"},{"key":"10.1016\/j.scico.2026.103550_bib0029","series-title":"Electronic Notes in Theoretical Computer Science","article-title":"Specifying real-time systems in rewriting logic","volume":"4","author":"\u00d6lveczky","year":"2000"},{"issue":"5","key":"10.1016\/j.scico.2026.103550_bib0030","doi-asserted-by":"crossref","first-page":"861","DOI":"10.1145\/365151.365169","article-title":"Sets and constraint logic programming","volume":"22","author":"Dovier","year":"2000","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"10.1016\/j.scico.2026.103550_bib0031","series-title":"Proceedings of the 9th Rodin User and Developer Workshop","article-title":"Context instantiation plug-in: a new approach to genericity in Rodin","author":"Guillaume Verdier","year":"2021"},{"key":"10.1016\/j.scico.2026.103550_bib0032","series-title":"Rigorous State-Based Methods - 8th International Conference, ABZ 2021, Ulm, Germany, June 9-11, 2021, Proceedings","first-page":"66","article-title":"Event-B formalization of Event-B contexts","volume":"12709","author":"Bodeveix","year":"2021"},{"key":"10.1016\/j.scico.2026.103550_sbref0033","series-title":"Event-B in the Institutional Framework: Defining a Semantics, Modularisation Constructs and Interoperability for a Specification Language","author":"Farrell","year":"2017"},{"key":"10.1016\/j.scico.2026.103550_bib0034","series-title":"Rigorous State-Based Methods - 9th International Conference, ABZ 2023, Nancy, France, May 30-June 2, 2023, Proceedings","first-page":"245","article-title":"Building specifications in the Event-B institution: a summary","volume":"14010","author":"Farrell","year":"2023"},{"key":"10.1016\/j.scico.2026.103550_bib0035","unstructured":"T.R.D. Team, Rocq prover reference manual, 2025. https:\/\/rocq-prover.org\/doc\/master\/refman\/index.html."},{"key":"10.1016\/j.scico.2026.103550_bib0036","series-title":"Isabelle\/HOL: A Proof Assistant for Higher-Order Logic","volume":"2283","author":"Nipkow","year":"2002"},{"key":"10.1016\/j.scico.2026.103550_bib0037","series-title":"Rigorous State-Based Methods","first-page":"241","article-title":"Event-B as DSL in Isabelle and HOL experiences from a prototype","author":"Ballenghien","year":"2024"},{"key":"10.1016\/j.scico.2026.103550_bib0038","unstructured":"T. Rowney, R. Ahuja, J. Avigad, S. Welleck, DSLean: a framework for type-correct interoperability between Lean 4 and external DSLS, 2026. https:\/\/arxiv.org\/abs\/2602.18657. arXiv: 2602.18657 [cs.LO]."},{"key":"10.1016\/j.scico.2026.103550_bib0039","series-title":"Leveraging Applications of Formal Methods, Verification and Validation. Modeling","first-page":"399","article-title":"Modelling by Patterns for Correct-by-Construction Process","author":"M\u00e9ry","year":"2018"},{"key":"10.1016\/j.scico.2026.103550_bib0040","series-title":"Generating Simulink Models from Hybridised Event-B Models","first-page":"189","author":"Singh","year":"2025"},{"issue":"2","key":"10.1016\/j.scico.2026.103550_bib0041","doi-asserted-by":"crossref","first-page":"835","DOI":"10.1109\/TR.2022.3219649","article-title":"Reflexive Event-B: Semantics and Correctness of the EB4EB Framework","volume":"73","author":"Rivi\u00e8re","year":"2024","journal-title":"IEEE Transactions on Reliability"}],"container-title":["Science of Computer Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0167642326001164?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0167642326001164?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2026,7,30]],"date-time":"2026-07-30T17:26:39Z","timestamp":1785432399000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0167642326001164"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2027,1]]},"references-count":41,"alternative-id":["S0167642326001164"],"URL":"https:\/\/doi.org\/10.1016\/j.scico.2026.103550","relation":{},"ISSN":["0167-6423"],"issn-type":[{"value":"0167-6423","type":"print"}],"subject":[],"published":{"date-parts":[[2027,1]]},"assertion":[{"value":"Elsevier","name":"publisher","label":"This article is maintained by"},{"value":"Correct pattern-based development through refinements and predicate transformers","name":"articletitle","label":"Article Title"},{"value":"Science of Computer Programming","name":"journaltitle","label":"Journal Title"},{"value":"https:\/\/doi.org\/10.1016\/j.scico.2026.103550","name":"articlelink","label":"CrossRef DOI link to publisher maintained version"},{"value":"article","name":"content_type","label":"Content Type"},{"value":"\u00a9 2026 Elsevier B.V. All rights are reserved, including those for text and data mining, AI training, and similar technologies.","name":"copyright","label":"Copyright"}],"article-number":"103550"}}