{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,31]],"date-time":"2025-10-31T23:43:15Z","timestamp":1761954195531,"version":"build-2065373602"},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540876021"},{"type":"electronic","value":"9783540876038"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-87603-8_11","type":"book-chapter","created":{"date-parts":[[2008,9,20]],"date-time":"2008-09-20T07:56:24Z","timestamp":1221897384000},"page":"125-138","source":"Crossref","is-referenced-by-count":24,"title":["On the Purpose of Event-B Proof Obligations"],"prefix":"10.1007","author":[{"given":"Stefan","family":"Hallerstede","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"11_CR1","doi-asserted-by":"crossref","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, Cambridge (1996)"},{"key":"11_CR2","unstructured":"Abrial, J.-R.: Event driven system construction (1999)"},{"key":"11_CR3","unstructured":"Abrial, J.-R.: Models of computations (1999)"},{"key":"11_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"51","DOI":"10.1007\/978-3-540-45236-2_5","volume-title":"FME 2003: Formal Methods","author":"J.-R. Abrial","year":"2003","unstructured":"Abrial, J.-R.: Event based sequential program development: Application to constructing a pointer program. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol.\u00a02805, pp. 51\u201374. Springer, Heidelberg (2003)"},{"key":"11_CR5","volume-title":"Modeling in Event-B: System and Software Engineering","author":"J.-R. Abrial","year":"2008","unstructured":"Abrial, J.-R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press, Cambridge (to appear, 2008)"},{"key":"11_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"588","DOI":"10.1007\/11901433_32","volume-title":"Formal Methods and Software Engineering","author":"J.-R. Abrial","year":"2006","unstructured":"Abrial, J.-R., Butler, M., Hallerstede, S., Voisin, L.: An open extensible tool environment for Event-B. In: Liu, Z., He, J. (eds.) ICFEM 2006. LNCS, vol.\u00a04260, pp. 588\u2013605. Springer, Heidelberg (2006)"},{"issue":"3","key":"11_CR7","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1007\/s001650300002","volume":"14","author":"J.-R. Abrial","year":"2003","unstructured":"Abrial, J.-R., Cansell, D., M\u00e9ry, D.: A mechanically proved and incremental development of IEEE 1394 tree identify protocol. Formal Aspects of Computing\u00a014(3), 215\u2013227 (2003)","journal-title":"Formal Aspects of Computing"},{"key":"11_CR8","unstructured":"Abrial, J.-R., Hallerstede, S.: Refinement, Decomposition and Instantiation of Discrete Models: Application to Event-B. Fundamentae Informatica\u00a077(1-2) (2007)"},{"key":"11_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1007\/BFb0053357","volume-title":"B\u201998: Recent Advances in the Development and Use of the B Method","author":"J.-R. Abrial","year":"1998","unstructured":"Abrial, J.-R., Mussat, L.: Introducing dynamic constraints in B. In: Bert, D. (ed.) B 1998. LNCS, vol.\u00a01393, pp. 83\u2013128. Springer, Heidelberg (1998)"},{"key":"11_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"67","DOI":"10.1007\/3-540-52559-9_61","volume-title":"Stepwise Refinement of Distributed Systems","author":"R.-J. Back","year":"1990","unstructured":"Back, R.-J.: Refinement Calculus II: Parallel and Reactive Programs. In: de Bakker, J.W., de Roever, W.-P., Rozenberg, G. (eds.) REX 1989. LNCS, vol.\u00a0430, pp. 67\u201393. Springer, Heidelberg (1990)"},{"key":"11_CR11","volume-title":"Graduate Texts in Computer Science","author":"R.-J. Back","year":"1998","unstructured":"Back, R.-J., von Wright, J.: Refinement Calculus: A Systematic Introduction. In: Graduate Texts in Computer Science. Springer, Heidelberg (1998)"},{"issue":"2","key":"11_CR12","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1016\/0167-6423(96)81173-7","volume":"27","author":"M.J. Butler","year":"1996","unstructured":"Butler, M.J.: Stepwise refinement of communicating systems. Science of Computer Programming\u00a027(2), 139\u2013173 (1996)","journal-title":"Science of Computer Programming"},{"key":"11_CR13","volume-title":"A Discipline of Programming","author":"E.W. Dijkstra","year":"1976","unstructured":"Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall, Englewood Cliffs (1976)"},{"key":"11_CR14","first-page":"423","volume-title":"FMOODS 1997","author":"C. Fischer","year":"1997","unstructured":"Fischer, C.: CSP-OZ: A combination of Object-Z and CSP. In: Bowmann, H., Derrick, J. (eds.) FMOODS 1997, vol.\u00a02, pp. 423\u2013438. Chapman & Hall, Boca Raton (1997)"},{"key":"11_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1007\/3-540-44880-2_8","volume-title":"ZB 2003: Formal Specification and Development in Z and B","author":"S. Hallerstede","year":"2003","unstructured":"Hallerstede, S.: Parallel hardware design in B. In: Bert, D., Bowen, J.P., King, S., Wald\u00e9n, M.A. (eds.) ZB 2003. LNCS, vol.\u00a02651, pp. 101\u2013102. Springer, Heidelberg (2003)"},{"key":"11_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1007\/978-3-540-73210-5_16","volume-title":"Integrated Formal Methods","author":"S. Hallerstede","year":"2007","unstructured":"Hallerstede, S., Hoang, T.S.: Qualitative probabilistic modelling in event-B. In: Davies, J., Gibbons, J. (eds.) IFM 2007. LNCS, vol.\u00a04591, pp. 293\u2013312. Springer, Heidelberg (2007)"},{"key":"11_CR17","volume-title":"Communicating Sequential Processes","author":"C.A.R. Hoare","year":"1985","unstructured":"Hoare, C.A.R.: Communicating Sequential Processes. Prentice Hall, Englewood Cliffs (1985)"},{"key":"11_CR18","volume-title":"Unifying Theories of Programming","author":"C.A.R. Hoare","year":"1998","unstructured":"Hoare, C.A.R., Jifeng, H.: Unifying Theories of Programming. Prentice Hall, Englewood Cliffs (1998)"},{"key":"11_CR19","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. Dijkstra","author":"C.C. Morgan","year":"1990","unstructured":"Morgan, C.C.: Of wp and CSP. In: Feijen, W.H.J., van Gasteren, A.J.M., Gries, D., Misra, J. (eds.) Beauty is Our Business: A Birthday Salute to Edsger W. Dijkstra, pp. 319\u2013326. Springer, Heidelberg (1990)"},{"key":"11_CR20","volume-title":"Programming from Specifications","author":"C.C. Morgan","year":"1994","unstructured":"Morgan, C.C.: Programming from Specifications, 2nd edn. Prentice Hall, Englewood Cliffs (1994)","edition":"2"},{"key":"11_CR21","doi-asserted-by":"crossref","unstructured":"de Roever, W.P., Engelhardt, K.: Data Refinement: Model-Oriented Proof Methods and their Comparison. Cambridge Tracts in Theoretical Computer Science 47. CUP (1998)","DOI":"10.1017\/CBO9780511663079"},{"key":"11_CR22","unstructured":"Roscoe, A.W.: Unbounded nondeterminism in CSP. Technical Monograph PRG-67, Programming Research Group, Oxford University (1988)"},{"key":"11_CR23","series-title":"Lecture Notes in Computer Science","volume-title":"MPC","author":"E. Sekerinski","year":"1993","unstructured":"Sekerinski, E.: A calculus for predicative programming. In: Bird, R.S., Morgan, C.C., Woodcock, J.C.P. (eds.) MPC 1993. LNCS. Springer, Heidelberg (1993)"},{"key":"11_CR24","volume-title":"Using Z. Specification, Refinement, and Proof","author":"J. Woodcock","year":"1996","unstructured":"Woodcock, J., Davies, J.: Using Z. Specification, Refinement, and Proof. Prentice-Hall, Englewood Cliffs (1996)"}],"container-title":["Lecture Notes in Computer Science","Abstract State Machines, B and Z"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-87603-8_11.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T11:43:29Z","timestamp":1619523809000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-87603-8_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540876021","9783540876038"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-87603-8_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}