{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T21:16:53Z","timestamp":1725484613957},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540431664"},{"type":"electronic","value":"9783540456483"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45648-1_7","type":"book-chapter","created":{"date-parts":[[2007,5,28]],"date-time":"2007-05-28T05:26:02Z","timestamp":1180329962000},"page":"120-139","source":"Crossref","is-referenced-by-count":2,"title":["Extraction of Abstraction Invariants for Data Refinement"],"prefix":"10.1007","author":[{"given":"Marielle","family":"Doche","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrew","family":"Gravell","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,1,22]]},"reference":[{"key":"7_CR1","doi-asserted-by":"crossref","unstructured":"J-R. Abrial. The B-Book: Assigning Programs to Meanings. Cambridge University Press, 1996.","DOI":"10.1017\/CBO9780511624162"},{"key":"7_CR2","doi-asserted-by":"crossref","unstructured":"M. Abadi and L. Lamport. The existence of refinement mappings. Theoretical Computer Science, 82(2), May 1991.","DOI":"10.1016\/0304-3975(91)90224-P"},{"key":"7_CR3","unstructured":"B-Core (UK) Limited, Oxon, UK. B-Toolkit, On-line manual., 1999. Available at http:\/\/www.b-core.com\/ONLINEDOC\/Contents.html ."},{"key":"7_CR4","series-title":"Lect Notes Comput Sci","first-page":"223","volume-title":"An approach to the design of distributed systems with B AMN","author":"M. J. Butler","year":"1997","unstructured":"M. J. Butler. An approach to the design of distributed systems with B AMN. In J. Bowen, M. Hinchey, and D. Till, editors, Proc. 10th Int. Conf. of Z Users: The Z Formal Specification Notation (ZUM), LNCS 1212, pages 223\u2013241, Reading, UK, April 1997. Springer-Verlag, Berlin. Available at http:\/\/www.dsse.ecs.soton.ac.uk\/ ."},{"key":"7_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"490","DOI":"10.1007\/3-540-48119-2_28","volume-title":"csp2B: A practical approach to combining CSP and B","author":"M. J. Butler","year":"1999","unstructured":"M. J. Butler. csp2B: A practical approach to combining CSP and B. In J. M. Wing, J. Woodcock, and J. Davies, editors, Proc. FM\u201999: World Congress on Formal Methods, LNCS 1708, pages 490\u2013508. Springer-Verlag, Berlin, September 1999. Available at http:\/\/www.dsse.ecs.soton.ac.uk\/ ."},{"key":"7_CR6","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-40911-4_12","volume-title":"IFM\u20192000 (Integrated Formal Methods)","author":"J. Derrick","year":"2000","unstructured":"J. Derrick and G. Smith. Structural refinement in object-z \/ csp. In IFM\u20192000 (Integrated Formal Methods), volume 1945 of LNCS. Springer-Verlag, 2000. Available at http:\/\/www.cs.ukc.ac.uk\/research\/tcs\/index.html ."},{"key":"7_CR7","unstructured":"Formal Systems (Europe) Ltd. Failures-Divergence Refinement-FDR2 user manual, Octobre 1997. Available at www.formal.demon.co.uk\/fdr2manual\/index.html ."},{"key":"7_CR8","doi-asserted-by":"crossref","unstructured":"C. Fischer and H. Wehrheim. Model-checking CSP-OZ specifications with FDR. In First international Conference on Integrated Formal Methods (IFM99), pages 315\u2013334. Springer-Verlag, 1999. Available at http:\/\/semantik.Informatik.Uni-Oldenburg.DE\/persons\/clemens.ficher\/ .","DOI":"10.1007\/978-1-4471-0851-1_17"},{"key":"7_CR9","unstructured":"P. Hartel, M. Butler, A. Currie, P. Henderson, M. Leuschel, A. Martin, A. Smith, U. Ultes-Nitsche, and B. Walters. Questions and answers about ten formal methods. In S. Gnesi and D. Latella, editors, Proc. 4th Int. Workshop on Formal Methods for Industrial Critical Systems, volume II, pages 179\u2013203, Trento, Italy, July 1999. ERCIM, STAR\/CNR, Pisa, Italy. Available at http:\/\/www.dsse.ecs.soton.ac.uk\/ ."},{"key":"7_CR10","doi-asserted-by":"crossref","unstructured":"C.A.R Hoare. Communicating Sequential Processes. Prentice Hall, 1985.","DOI":"10.1007\/978-3-642-82921-5_4"},{"key":"7_CR11","doi-asserted-by":"crossref","unstructured":"I. MacColl and D. Carrington. Specifying interactive systems in Object-Z and CSP. In First international Conference on Integrated Formal Methods (IFM99). Springer-Verlag, 1999. Available at http:\/\/archive.csse.uq.edu.au\/ ianm\/ .","DOI":"10.1007\/978-1-4471-0851-1_18"},{"key":"7_CR12","doi-asserted-by":"crossref","unstructured":"C.C. Morgan. Of wp and CSP. In W.H.J. Feijen, A.J.M. van Gasteren, D. Gries, and J. Misra, editors, Beauty is our business: a birthday salute to Edsger W. Dijkstra. Springer Verlag, 1990.","DOI":"10.1007\/978-1-4612-4476-9_37"},{"key":"7_CR13","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"205","DOI":"10.1007\/BFb0053592","volume-title":"Fundamental Approach of Software Engineering (FASE98)","author":"A. Mota","year":"1998","unstructured":"A. Mota and A. Sampaio. Model-checking CSP-Z. In Fundamental Approach of Software Engineering (FASE98), number 1382 in LNCS, pages 205\u2013220. Springer Verlag, 1998. Available at http:\/\/www.di.ufpe.br\/ acm\/ ."},{"key":"7_CR14","unstructured":"A.W. Roscoe. The Theory and Practice of Concurrency. Prentice-Hall, 1997."},{"key":"7_CR15","unstructured":"J. M. Spivey. The Z Notation: A Reference Manual. Prentice Hall International Series in Computer Science, 2nd edition, 1992."},{"key":"7_CR16","series-title":"Lect Notes Comput Sci","volume-title":"VDM\u201990","author":"J.C.P. Woodcock","year":"1990","unstructured":"J.C.P. Woodcock and C.C. Morgan. Refinement of state-based concurrent systems. In D. Bjorner, C.A.R. Hoare, and H. Langmaack, editors, VDM\u201990, volume 428 of LNCS. Springer-Verlag, 1990. Available at http:\/\/www.iro.umontreal.ca\/labs\/teleinfo\/PubListIndex.html ."}],"container-title":["Lecture Notes in Computer Science","ZB 2002:Formal Specification and Development in Z and B"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45648-1_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,12]],"date-time":"2023-05-12T01:34:32Z","timestamp":1683855272000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45648-1_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540431664","9783540456483"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/3-540-45648-1_7","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}