{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,26]],"date-time":"2026-08-26T01:15:58Z","timestamp":1787706958109,"version":"build-2784847793"},"reference-count":37,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2014,3,1]],"date-time":"2014-03-01T00:00:00Z","timestamp":1393632000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2014,3]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    Event-B provides a flexible framework for stepwise system development via refinement. The framework supports steps for (a) refining events (one-by-one), (b) splitting events (one-by-many), and (c) introducing new events. In each of the steps events can be indicated as\n                    <jats:italic>convergent<\/jats:italic>\n                    (to be made internal) or\n                    <jats:italic>anticipated<\/jats:italic>\n                    (treatment deferred to a later refinement step). All such steps are accompanied with precise proof obligations. However, no behavioural semantics has been provided to validate the proof obligations, and no formal justification has previously been given for the application of these rules in a refinement chain. Behavioural semantics expresses a clear relationship between the first and last machines in a refinement chain. The framework we present provides a coherent justification for Abrial\u2019s approach to refinement in Event-B, and its generalisation to interface extension: adding events to the interface. In this paper, we give a behavioural semantics for Event-B refinement, with a treatment for the first time of splitting events and of anticipated events, adding to the well-understood treatment of convergent events. To this end, we define a CSP semantics for Event-B and show how the different forms of Event-B refinement can be captured as CSP refinement. It turns out that the appropriate CSP refinement relationship is influenced by the particular Event-B\n                    <jats:italic>development strategy<\/jats:italic>\n                    taken. We present two such strategies, one allowing, the other disallowing interface extensions.\n                  <\/jats:p>","DOI":"10.1007\/s00165-012-0265-0","type":"journal-article","created":{"date-parts":[[2012,10,22]],"date-time":"2012-10-22T08:23:41Z","timestamp":1350894221000},"page":"251-280","source":"Crossref","is-referenced-by-count":21,"title":["The behavioural semantics of Event-B refinement"],"prefix":"10.1145","volume":"26","author":[{"given":"Steve","family":"Schneider","sequence":"first","affiliation":[{"name":"Department of Computing, University of Surrey, Surrey, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Helen","family":"Treharne","sequence":"additional","affiliation":[{"name":"Department of Computing, University of Surrey, Surrey, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Heike","family":"Wehrheim","sequence":"additional","affiliation":[{"name":"Department of Computer Science, University of Paderborn, Paderborn, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-010-0145-y"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"crossref","unstructured":"Abrial J-R Butler MJ Hallerstede S Voisin L (2008) A roadmap for the Rodin toolset. In: B\u00f6rger E Butler MJ Bowen JP Boca P (eds) ABZ. Lecture notes in computer science vol 5238. Springer Berlin p 347","DOI":"10.1007\/978-3-540-87603-8_35"},{"key":"e_1_2_1_2_3_2","unstructured":"Abrial J-R (2005) The B-book\u2014assigning programs to meanings. Cambridge University Press"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"crossref","unstructured":"Abrial J-R (2010) Modeling in Event-B: system and software engineering. Cambridge University Press","DOI":"10.1017\/CBO9781139195881"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"crossref","unstructured":"Bolton C Davies J (2002) Refinement in object-Z and CSP. In: Butler M Petre L Sere K (eds) IFM 2002: integrated formal methods. LNCS vol 2335 pp 225\u2013244","DOI":"10.1007\/3-540-47884-1_13"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"crossref","unstructured":"Boiten EA Derrick J (2009) Modelling divergence in relational concurrent refinement. In: Leuschel M Wehrheim H (eds) Proceedings of 7th international conference on integrated formal methods IFM 2009 D\u00fcsseldorf Germany February 16\u201319 2009. Lecture notes in computer science vol 5423. Springer Berlin pp 183\u2013199","DOI":"10.1007\/978-3-642-00255-7_13"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"crossref","unstructured":"Butler MJ Hallerstede S (2007) The Rodin formal modelling tool. In: BCS-FACS Christmas 2007 Meeting\u2014formal methods in industry","DOI":"10.14236\/ewic\/FMI2007.2"},{"key":"e_1_2_1_2_8_2","unstructured":"Butler MJ (1992) A CSP approach to action systems. DPhil thesis Oxford University"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"crossref","unstructured":"Butler MJ (2000) csp2B: a practical approach to combining CSP and B. In: FACS pp 182\u2013196","DOI":"10.1007\/PL00003930"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"crossref","unstructured":"Butler MJ (2009) Decomposition structures for Event-B. In: Leuschel M Wehrheim H (eds) Proceedings of 7th international conference on integrated formal methods IFM 2009 D\u00fcsseldorf Germany February 16\u201319 2009. Lecture notes in computer science vol 5423. Springer Berlin pp 20\u201338","DOI":"10.1007\/978-3-642-00255-7_2"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-012-0239-2"},{"key":"e_1_2_1_2_12_2","volume-title":"In: Graduate texts in computer science","author":"Back R-J","year":"1998"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"publisher","DOI":"10.5555\/379171"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-003-0007-4"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-003-0002-9"},{"key":"e_1_2_1_2_16_2","unstructured":"Event-B.org (2011) Rodin platform version 2.2.2. Released 6 Jan 2011. http:\/\/www.event-b.org\/"},{"key":"e_1_2_1_2_17_2","unstructured":"Formal Systems (Europe) Ltd (2011) The FDR model checker. http:\/\/www.fsel.com\/. Accessed 8 Mar 2011"},{"key":"e_1_2_1_2_18_2","unstructured":"Hoang TS Abrial J-R (2010) Event-B decomposition for parallel programs. In: Frappier M Gl\u00e4sser U Khurshid S Laleau R Reeves S (eds) ABZ. Lecture notes in computer science vol 5977. Springer Berlin pp 319\u2013333"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"crossref","unstructured":"Hoang TS Abrial J-R (2011) Reasoning about liveness properties in Event-B. In: Qin S Qiu Z (eds) ICFEM. Lecture notes in computer science vol 6991. Springer Berlin pp 456\u2013471","DOI":"10.1007\/978-3-642-24559-6_31"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-009-0138-3"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"crossref","unstructured":"Hoare CAR (1985) Communicating sequential processes. Prentice-Hall","DOI":"10.1007\/978-3-642-82921-5_4"},{"key":"e_1_2_1_2_22_2","unstructured":"Iliasov A (2009) On Event-B and control flow. Technical report CS-TR-1159 School of Computing Science Newcastle University August 2009"},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"publisher","DOI":"10.1145\/505145.505149"},{"key":"e_1_2_1_2_24_2","unstructured":"M\u00e9tayer C Abrial J-R Voisin L (2010) Event-B language 2005. RODIN Project Deliverable 3.2. http:\/\/rodin.cs.ncl.ac.uk\/deliverables\/D7.pdf. Accessed 25 May 2010"},{"key":"e_1_2_1_2_25_2","doi-asserted-by":"publisher","DOI":"10.1145\/44501.44503"},{"key":"e_1_2_1_2_26_2","doi-asserted-by":"crossref","unstructured":"Morgan CC (1990) Of wp and CSP. Beauty is our business: a birthday salute to E. W. Dijkstra pp 319\u2013326","DOI":"10.1007\/978-1-4612-4476-9_37"},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2004.05.017"},{"key":"e_1_2_1_2_28_2","unstructured":"Roscoe AW (1998) Theory and practice of concurrency. Prentice-Hall"},{"key":"e_1_2_1_2_29_2","doi-asserted-by":"publisher","DOI":"10.5555\/555233"},{"key":"e_1_2_1_2_30_2","unstructured":"Silva RA Hoang TS Wei W Iliasov A (2001) A survey on Event-B decomposition. In: Workshop on automated verification of critical systems (AVOCS 2011)"},{"key":"e_1_2_1_2_31_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-005-0076-7"},{"key":"e_1_2_1_2_32_2","doi-asserted-by":"crossref","unstructured":"Schneider S Treharne H Wehrheim H (2010) A CSP approach to control in Event-B. In: IFM pp 260\u2013274","DOI":"10.1007\/978-3-642-16265-7_19"},{"key":"e_1_2_1_2_33_2","doi-asserted-by":"crossref","unstructured":"Schneider S Treharne H Wehrheim H (2011) Bounded retransmission in Event-B CSP: a case study. In: Workshop B 2011 ENTCS","DOI":"10.1016\/j.entcs.2011.11.019"},{"key":"e_1_2_1_2_34_2","doi-asserted-by":"crossref","unstructured":"Schneider S Treharne H Wehrheim H (2011) A CSP account of Event-B refinement. In: Derrick J Boiten EA Reeves S (eds) Refine 2011. EPTCS vol 55 pp 139\u2013154","DOI":"10.4204\/EPTCS.55.9"},{"key":"e_1_2_1_2_35_2","unstructured":"Schneider S Treharne H Wehrheim H (2011) Stepwise refinement in Event-B CSP. Technical Report CS-11-03 University of Surrey"},{"key":"e_1_2_1_2_36_2","doi-asserted-by":"crossref","unstructured":"Woodcock J Cavalcanti A (2002) The semantics of circus. In: Bert D Bowen JP Henson MC Robinson K (eds) ZB 2002. Lecture notes in computer science vol 2272. Springer Berlin pp 184\u2013203","DOI":"10.1007\/3-540-45648-1_10"},{"key":"e_1_2_1_2_37_2","unstructured":"Woodcock JCP Davies J (1996) Using Z: specification refinement and proof. Prentice Hall"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-012-0265-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-012-0265-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-012-0265-0","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T11:04:16Z","timestamp":1641467056000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-012-0265-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,3]]},"references-count":37,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2014,3]]}},"alternative-id":["10.1007\/s00165-012-0265-0"],"URL":"https:\/\/doi.org\/10.1007\/s00165-012-0265-0","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,3]]}}}