{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T00:07:36Z","timestamp":1725494856421},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540665885"},{"type":"electronic","value":"9783540481188"}],"license":[{"start":{"date-parts":[[1999,1,1]],"date-time":"1999-01-01T00:00:00Z","timestamp":915148800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48118-4_5","type":"book-chapter","created":{"date-parts":[[2007,11,14]],"date-time":"2007-11-14T01:30:57Z","timestamp":1195003857000},"page":"1028-1047","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Data abstraction for CSP-OZ"],"prefix":"10.1007","author":[{"given":"Heike","family":"Wehrheim","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[1999,9,17]]},"reference":[{"key":"5_CR1","doi-asserted-by":"crossref","unstructured":"E.M. Clarke, O. Grumberg, and D.E. Long. Model checking and abstraction. In 19th ACM POPL, 1992.","DOI":"10.1145\/143165.143235"},{"key":"5_CR2","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"417","DOI":"10.1007\/978-3-540-48654-1_31","volume-title":"CONCUR\u201994","author":"R. Cleaveland","year":"1994","unstructured":"R. Cleaveland and J. Riely. Testing-based abstractions for value-passing systems. In B. Jonsson and J. Parrow, editors, CONCUR\u201994,volume 836 ofLecture Notes in Computer Science, pages 417\u2013432, 1994."},{"key":"5_CR3","doi-asserted-by":"crossref","unstructured":"J. Corbett. Constructing abstract models for concurrent real time software. In International Symposium on Software Testing and Analysis, 1996.","DOI":"10.1145\/229000.226323"},{"key":"5_CR4","doi-asserted-by":"crossref","unstructured":"P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In 4th ACM POPL, 1977.","DOI":"10.1145\/512950.512973"},{"key":"5_CR5","unstructured":"D. Dams, O. Grumberg, and R. Gerth. Abstract interpretation of reactive systems: Abstractions preserving \u2200CTL\u2703, \u2203 CTL\u2703and CTL\u2703. In E.-R. Olderog,editor, Programming concepts, methods and calculi, volume A-56,pages 573\u2013592. Elsevier, 1994."},{"key":"5_CR6","doi-asserted-by":"publisher","first-page":"511","DOI":"10.1016\/0920-5489(95)00024-O","volume":"17","author":"R. Duke","year":"1995","unstructured":"R. Duke, G. Rose, and G. Smith. Object-Z: A specification language advocated for the description of standards. Computer Standards and Interfaces, 17:511\u2013533, 1995.","journal-title":"Computer Standards and Interfaces"},{"key":"5_CR7","doi-asserted-by":"crossref","unstructured":"C. Fischer. CSP-OZ: A combination of Object-Z and CSP. In H. Bowman and J. Derrick, editors, Formal Methods for Open Object-Based Distributed Systems (FMOODS\u2019 97), volume 2, pages 423\u2013438. Chapman & Hall, 1997.","DOI":"10.1007\/978-0-387-35261-9_29"},{"key":"5_CR8","doi-asserted-by":"crossref","unstructured":"C. Fischer and H. Wehrheim. Model-checking CSP-OZ specifications with FDR. In IFM\u2019 99: International Workshop on Integrated Formal Methods, Workshops in Computing.Springer, 1999.","DOI":"10.1007\/978-1-4471-0851-1_17"},{"key":"5_CR9","unstructured":"Formal Systems (Europe) Ltd. Failures-Divergence Refinement: FDR2 User Manual, Oct 1997."},{"key":"5_CR10","doi-asserted-by":"crossref","unstructured":"J.F. Groote and A. Ponse. Proof theory for \u03bc-CRL: A language for processes with data. In Semantics of specification languages, Workshops in Computing. Springer,1993.","DOI":"10.1007\/978-1-4471-3229-5_13"},{"key":"5_CR11","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":"5_CR12","doi-asserted-by":"crossref","unstructured":"B. Jonsson and J. Parrow. Deciding bisimulation equivalence for a class of non-finite state programs.Information and Computation, pages 272\u2013302, 1993.","DOI":"10.1006\/inco.1993.1069"},{"key":"5_CR13","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"283","DOI":"10.1007\/BFb0105411","volume-title":"Theorem Proving in Higher Order Logics","author":"T. S. Kolyang","year":"1996","unstructured":"Kolyang, T. Santen, and B. Wolff. A structure preserving encoding of Z in Isabelle\/HOL. In J. von Wright, J. Grundy, and J. Harrison, editors, Theorem Proving in Higher Order Logics, LNCS 1125, pages 283\u2013298. Springer Verlag, 1996. Data Abstraction for CSP-OZ 1045"},{"key":"5_CR14","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/BF01384313","volume":"6","author":"C. Loiseaux","year":"1995","unstructured":"C. Loiseaux, S. Graf, J. Sifakis, A. Bouajjani, and S. Bensalem. Property preserving abstractions for the verification of concurrent systems. Formal methods in system design, 6:1\u201335,1995.","journal-title":"Formal methods in system design"},{"key":"5_CR15","doi-asserted-by":"crossref","unstructured":"I. Meisels and M. Saaltink.The Z\/EVES Reference Manual. ORA Canada, 1997. http:\/\/www.ora.on.ca\/z-eves\/ .","DOI":"10.1007\/BFb0027284"},{"key":"5_CR16","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"205","DOI":"10.1007\/BFb0053592","volume-title":"In Proceedings of the European Joint Conference on Theory and Practice of Software","author":"A. Mota","year":"1998","unstructured":"A. Mota and A. Sampaio. Model-checking CSP-Z.In Proceedings of the European Joint Conference on Theory and Practice of Software, volume 1382 of LNCS,pages 205\u2013220, 1998."},{"key":"5_CR17","unstructured":"J. Quemada, editor. Revised working draft on enhancements to LOTOS (V4). 1996."},{"key":"5_CR18","unstructured":"A. W. Roscoe. The Theory and Practice of Concurrency. Prentice-Hall, 1997."},{"key":"5_CR19","series-title":"Lect Notes Comput Sci","first-page":"33","volume-title":"ESORICS 94","author":"A. W. Roscoe","year":"1994","unstructured":"A. W. Roscoe, J. C. P. Woodcock, and L. Wulf. Non-interference through determinism.In D. Gollmann, editor, ESORICS 94, volume 875 of LNCS, pages 33\u201354.Springer-Verlag, 1994."},{"key":"5_CR20","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"62","DOI":"10.1007\/3-540-63533-5_4","volume-title":"Proceedings of FME 1997","author":"G. Smith","year":"1997","unstructured":"G. Smith. A semantic integration of Object-Z and CSP for the specification of concurrent systems. In J. Fitzgerald, C. B. Jones, and P. Lucas, editors, Proceedings of FME 1997, volume 1313 of LNCS, pages 62\u201381. Springer, 1997."},{"key":"5_CR21","unstructured":"J. M. Spivey. The Z Notation: A Reference Manual.Prentice-Hall International Series in Computer Science, 2nd edition, 1992."},{"key":"5_CR22","unstructured":"K. Taguchi and K. Araki. Specifying concurrent systems by Z + CCS. In International Symposium on Future Software Technology (ISFST), pages 101\u2013108,1997."},{"key":"5_CR23","doi-asserted-by":"crossref","unstructured":"P. Wolper.Expressing interesting properties of programs in propositional temporal logic. InACM POPL, pages 184\u2013193, 1986.","DOI":"10.1145\/512644.512661"},{"key":"5_CR24","unstructured":"J. Woodcock and J. Davies. Using Z. Prentice-Hall International, 1996."}],"container-title":["Lecture Notes in Computer Science","FM\u201999 \u2014 Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48118-4_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,14]],"date-time":"2023-05-14T18:25:41Z","timestamp":1684088741000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48118-4_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540665885","9783540481188"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/3-540-48118-4_5","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1999]]},"assertion":[{"value":"17 September 1999","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}