{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T04:20:55Z","timestamp":1743135655858,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":10,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540402534"},{"type":"electronic","value":"9783540448808"}],"license":[{"start":{"date-parts":[[2003,1,1]],"date-time":"2003-01-01T00:00:00Z","timestamp":1041379200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2003,1,1]],"date-time":"2003-01-01T00:00:00Z","timestamp":1041379200000},"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":[[2003]]},"DOI":"10.1007\/3-540-44880-2_28","type":"book-chapter","created":{"date-parts":[[2007,7,3]],"date-time":"2007-07-03T16:12:53Z","timestamp":1183479173000},"page":"477-496","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Using B Refinement to Analyse Compensating Business Processes"],"prefix":"10.1007","author":[{"given":"Carla","family":"Ferreira","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael","family":"Butler","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2003,5,27]]},"reference":[{"key":"28_CR1","doi-asserted-by":"crossref","unstructured":"J.-R. Abrial and L. Mussat. Introducing dynamic constraints in B. In Recent Advances in the Development and Use of the B Method (B\u201998), volume 1393. Springer-Verlag, 1998.","DOI":"10.1007\/BFb0053357"},{"key":"28_CR2","doi-asserted-by":"crossref","unstructured":"J.R. Abrial. The B-Book: Assigning Programs to Meanings. Cambridge University Press, 1996.","DOI":"10.1017\/CBO9780511624162"},{"key":"28_CR3","unstructured":"J. Augusto and M. Butler. Some observations about using SPIN and STeP to verify StAC specifications. Technical report, Department of Electronics and Computer Science, University of Southampton, October 2002."},{"issue":"1","key":"28_CR4","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1016\/S0304-3975(96)00191-0","volume":"173","author":"N. Bjorner","year":"1997","unstructured":"N. Bjorner, A. Browne, and Z. Manna. Automatic generation of invariants and intermediate assertions. Theoretical Computer Science, 173(1):49\u201387, 1997.","journal-title":"Theoretical Computer Science"},{"key":"28_CR5","doi-asserted-by":"publisher","first-page":"182","DOI":"10.1007\/PL00003930","volume":"12","author":"M. Butler","year":"2000","unstructured":"M. Butler. csp2B: A practical approach to combining CSP and B. Formal Aspects of Computing, 12: 182\u2013198, 2000.","journal-title":"Formal Aspects of Computing"},{"key":"28_CR6","doi-asserted-by":"crossref","unstructured":"M. Butler. On the use of data refinement in the development of secure communications systems. Formal Aspects of Computing, To appear, 2002.","DOI":"10.1007\/s001650200025"},{"issue":"4","key":"28_CR7","doi-asserted-by":"publisher","first-page":"355","DOI":"10.1023\/A:1016503426126","volume":"6","author":"M. Butler","year":"2002","unstructured":"M. Butler. A system-based approach to the formal development of embedded controllers for a railway. Design Automation for Embedded Systems, 6(4):355\u2013366, 2002.","journal-title":"Design Automation for Embedded Systems"},{"key":"28_CR8","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1007\/3-540-40911-4_5","volume-title":"Integrated Formal Methods(IFM\u20192000)","author":"M. Butler","year":"2000","unstructured":"M. Butler and C. Ferreira. A process compensation language. In Integrated Formal Methods(IFM\u20192000), volume 1945 of LNCS, pages 61\u201376. Springer-Verlag, 2000."},{"issue":"4","key":"28_CR9","doi-asserted-by":"publisher","first-page":"743","DOI":"10.1147\/sj.414.0743","volume":"41","author":"M. Chessell","year":"2002","unstructured":"M. Chessell, D. Vines, C. Griffin, M. Butler, C. Ferreira, and P. Henderson. Extending the concept of transaction compensation. IBM Systems Journal, 41(4):743\u2013758, 2002.","journal-title":"IBM Systems Journal"},{"key":"28_CR10","unstructured":"C. Ferreira. Precise Modelling of Business Processes with Compensation. PhD thesis, Department of Electronics and Computer Science, University of Southampton, 2002."}],"container-title":["Lecture Notes in Computer Science","ZB 2003: Formal Specification and Development in Z and B"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44880-2_28","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,18]],"date-time":"2023-02-18T01:57:59Z","timestamp":1676685479000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/3-540-44880-2_28"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540402534","9783540448808"],"references-count":10,"URL":"https:\/\/doi.org\/10.1007\/3-540-44880-2_28","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2003]]},"assertion":[{"value":"27 May 2003","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}