{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,28]],"date-time":"2025-11-28T12:09:36Z","timestamp":1764331776751},"reference-count":30,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"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":[[2011,1]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>Event-B is a formal modelling method which is claimed to be suitable for diverse modelling domains, such as reactive systems and sequential program development. This claim hinges on the fact that any particular model has an appropriate semantics. In Event-B, this semantics is provided implicitly by proof obligations associated with a model. There is no fixed semantics though. In this article we argue that this approach is beneficial to modelling because we can use similar proof obligations across a variety of modelling domains. By way of two examples we show how similar proof obligations are linked to different semantics. A small set of proof obligations is thus suitable for a whole range of modelling problems in diverse modelling domains.<\/jats:p>","DOI":"10.1007\/s00165-009-0138-3","type":"journal-article","created":{"date-parts":[[2009,11,16]],"date-time":"2009-11-16T15:17:02Z","timestamp":1258384622000},"page":"133-150","source":"Crossref","is-referenced-by-count":21,"title":["On the purpose of Event-B proof obligations"],"prefix":"10.1145","volume":"23","author":[{"given":"Stefan","family":"Hallerstede","sequence":"first","affiliation":[{"name":"Institut f\u00fcr Informatik, University of D\u00fcsseldorf, Universit\u00e4tsstra\u00dfe 1, 40225, D\u00fcsseldorf, Germany"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"crossref","unstructured":"Abrial J-R Butler M Hallerstede S Voisin L (2006) An open extensible tool environment for Event-B. In: Liu Z He J (eds) ICFEM 2006 vol 4260. Springer Berlin pp 588\u2013605","DOI":"10.1007\/11901433_32"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511624162"},{"key":"e_1_2_1_2_3_2","unstructured":"Abrial J-R (1999) Event driven system construction (unpublished)"},{"key":"e_1_2_1_2_4_2","unstructured":"Abrial J-R (1999) Models of computations (unpublished)"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"crossref","unstructured":"Abrial J-R (2003) Event based sequential program development: Application to constructing a pointer program. In: Araki K Gnesi S Mandrioli D (eds) FME 2003: formal methods. LNCS vol 2805. Springer Berlin pp 51\u201374","DOI":"10.1007\/978-3-540-45236-2_5"},{"key":"e_1_2_1_2_6_2","volume-title":"Modeling in event-B: system and software engineering","author":"Abrial J-R","year":"2008"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"publisher","DOI":"10.1007\/s001650300002"},{"issue":"1","key":"e_1_2_1_2_8_2","first-page":"1","article-title":"Refinement, decomposition and instantiation of discrete models: application to Event-B","volume":"77","author":"Abrial J-R","year":"2007","journal-title":"Fundam Inf"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"crossref","unstructured":"Abrial J-R Mussat L (1998) Introducing dynamic constraints in B. In: Bert D (ed) B\u201998 : the 2nd international B conference. LNCS vol 1393. Springer Berlin pp 83\u2013128","DOI":"10.1007\/BFb0053357"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4757-4376-0","volume-title":"Verification of sequential and concurrent programs","author":"Apt KR","year":"1991"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"crossref","unstructured":"Badeau F Amelot A (2005) Using B as a high level programming language in an industrial project: Roissy VAL. In: Treharne H King S Henson M Schneider S (eds) ZB 2005. LNCS vol 3455 pp 334\u2013354","DOI":"10.1007\/11415787_20"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"crossref","unstructured":"Back R-J (1989) Refinement calculus II: parallel and reactive programs. In: deBakker JW deRoever WP Rozenberg G (eds) Stepwise refinement of distributed systems. Lecture notes in computer science vol 430. Springer Berlin pp 67\u201393","DOI":"10.1007\/3-540-52559-9_61"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(96)81173-7"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-1674-2"},{"key":"e_1_2_1_2_15_2","volume-title":"A discipline of programming","author":"Dijkstra EW","year":"1976"},{"key":"e_1_2_1_2_16_2","first-page":"423","volume-title":"FMOODS \u201997, vol 2","author":"Fischer C","year":"1997"},{"key":"e_1_2_1_2_17_2","first-page":"101","volume-title":"ZB. LNCS, vol 2651","author":"Hallerstede S","year":"2003"},{"key":"e_1_2_1_2_18_2","unstructured":"Hallerstede S (2005) The Event-B proof obligation generator. Technical report ETH Z\u00fcrich"},{"key":"e_1_2_1_2_19_2","first-page":"293","volume-title":"IFM 2007. LNCS, vol 4591","author":"Hallerstede S","year":"2007"},{"key":"e_1_2_1_2_20_2","volume-title":"Unifying theories of programming","author":"Hoare CAR","year":"1998"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"publisher","DOI":"10.5555\/3921"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"publisher","DOI":"10.1109\/MAHC.1984.10017"},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"crossref","first-page":"319","DOI":"10.1007\/978-1-4612-4476-9_37","volume-title":"Beauty is our business: a birthday salute to Edsger W","author":"Morgan CC","year":"1990"},{"key":"e_1_2_1_2_24_2","volume-title":"Programming from specifications: second edition","author":"Morgan CC","year":"1994"},{"key":"e_1_2_1_2_25_2","doi-asserted-by":"crossref","unstructured":"de Roever WP Engelhardt K (1998) Data refinement: model-oriented proof methods and their comparison. Cambridge tracts in theoretical computer science 47 vol 46. Cambridge University Press","DOI":"10.1017\/CBO9780511663079"},{"key":"e_1_2_1_2_26_2","unstructured":"Roscoe AW (1988) Unbounded nondeterminism in CSP. Technical Monograph PRG-67 Programming Research Group Oxford University"},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"crossref","unstructured":"Sekerinski E (1993) A calculus for predicative programming. In: Bird RS Morgan CC Woodcock JCP (eds) MPC. LNCS. Springer Berlin","DOI":"10.1007\/3-540-56625-2_20"},{"key":"e_1_2_1_2_28_2","unstructured":"Turing AM (1949) Checking a large routine. In: Report of a conference on high speed automatic calculating machines EDSAC inaugural conference University Mathematical Laboratory Cambridge UK pp 67\u201369"},{"key":"e_1_2_1_2_29_2","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0020908","volume-title":"On the shape of mathematical arguments, vol 445","author":"van Gasteren AJM","year":"1990"},{"key":"e_1_2_1_2_30_2","volume-title":"Using Z. Specification, refinement, and proof","author":"Woodcock J","year":"1996"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-009-0138-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-009-0138-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-009-0138-3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:55:13Z","timestamp":1641484513000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-009-0138-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,1]]},"references-count":30,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2011,1]]}},"alternative-id":["10.1007\/s00165-009-0138-3"],"URL":"https:\/\/doi.org\/10.1007\/s00165-009-0138-3","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011,1]]}}}