{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,1]],"date-time":"2026-04-01T14:40:35Z","timestamp":1775054435673,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":5,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540255598","type":"print"},{"value":"9783540320074","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11415787_14","type":"book-chapter","created":{"date-parts":[[2010,7,11]],"date-time":"2010-07-11T22:07:36Z","timestamp":1278886056000},"page":"222-241","source":"Crossref","is-referenced-by-count":31,"title":["Refinement and Reachability in Event_B"],"prefix":"10.1007","author":[{"given":"Jean-Raymond","family":"Abrial","sequence":"first","affiliation":[]},{"given":"Dominique","family":"Cansell","sequence":"additional","affiliation":[]},{"given":"Dominique","family":"M\u00e9ry","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"14_CR1","doi-asserted-by":"publisher","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) ISBN 0-521-49619-5"},{"key":"14_CR2","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, p. 83. Springer, Heidelberg (1998)"},{"key":"14_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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":"14_CR4","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.R. Back","year":"1990","unstructured":"Back, R.J.R.: Refinement calculus, part 2: Parallel and reactive systems. In: de Bakker, J.W., de Roever, W.-P., Rozenberg, G. (eds.) REX 1989. LNCS, vol.\u00a0430, pp. 67\u201393. Springer, Heidelberg (1990)"},{"issue":"3","key":"14_CR5","doi-asserted-by":"publisher","first-page":"872","DOI":"10.1145\/177492.177726","volume":"16","author":"L. Lamport","year":"1994","unstructured":"Lamport, L.: The temporal logic of actions. ACM Transactions on Programming Languages and Systems\u00a016(3), 872\u2013923 (1994)","journal-title":"ACM Transactions on Programming Languages and Systems"}],"container-title":["Lecture Notes in Computer Science","ZB 2005: Formal Specification and Development in Z and B"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11415787_14.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T07:03:43Z","timestamp":1619507023000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11415787_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540255598","9783540320074"],"references-count":5,"URL":"https:\/\/doi.org\/10.1007\/11415787_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2005]]}}}