{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T14:45:17Z","timestamp":1725633917720},"publisher-location":"London","reference-count":25,"publisher":"Springer London","isbn-type":[{"type":"print","value":"9781852331078"},{"type":"electronic","value":"9781447108511"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/978-1-4471-0851-1_17","type":"book-chapter","created":{"date-parts":[[2011,11,16]],"date-time":"2011-11-16T07:27:59Z","timestamp":1321428479000},"page":"315-334","source":"Crossref","is-referenced-by-count":34,"title":["Model-Checking CSP-OZ Specifications with FDR"],"prefix":"10.1007","author":[{"given":"Clemens","family":"Fischer","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Heike","family":"Wehrheim","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"17_CR1","volume-title":"Up and down the temporal way","author":"H Barringer","year":"1985","unstructured":"H. Barringer. Up and down the temporal way. Technical Report UMCS-85\u20139-3, Department of Computer Science, University of Manchester, 1985."},{"key":"17_CR2","doi-asserted-by":"crossref","first-page":"281","DOI":"10.1007\/3-540-15670-4_14","volume-title":"Seminar on Semantics of Concurreny","author":"SD Brookes","year":"1985","unstructured":"S. D. Brookes and A. W. Roscoe. An improved failures model for communicating processes. In S. D. Brookes, editor, Seminar on Semantics of Concurreny, volume 197 of LNCS, pages 281\u2013305, 1985."},{"key":"17_CR3","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":"17_CR4","volume-title":"Failures-Divergence Refinement: FDR2 User Manual","author":"Formal Systems (Europe) Ltd","year":"1997","unstructured":"Formal Systems (Europe) Ltd. Failures-Divergence Refinement: FDR2 User Manual, Oct 1997."},{"key":"17_CR5","volume-title":"Data-Refinement in CSP-OZ","author":"C Fischer","year":"1997","unstructured":"C. Fischer and S. Hallerstede. Data-Refinement in CSP-OZ. Technical Report TRCF-97\u20133, University of Oldenburg, June 1997."},{"key":"17_CR6","doi-asserted-by":"crossref","first-page":"423","DOI":"10.1007\/978-0-387-35261-9_29","volume-title":"Formal Methods for Open Object-Based Distributed Systems (FMOODS\u201997)","author":"C Fischer","year":"1997","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\u201997), volume 2, pages 423\u2013438. Chapman Hall, 1997."},{"key":"17_CR7","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1007\/978-3-540-49676-2_2","volume-title":"ZUM\u201998 The Z Formal Specification Notation","author":"C Fischer","year":"1998","unstructured":"C. Fischer. How to combine Z with a process algebra. In J. Bowen, A. Fett, and M. Hinchey, editors, ZUM\u201998 The Z Formal Specification Notation, volume 1493 of LNCS, pages 5\u201323. Springer, 1998."},{"key":"17_CR8","volume-title":"Z user meeting","author":"HS Goodman","year":"1996","unstructured":"H.S. Goodman. The Z-into-Haskell tool-kit. In Z user meeting, Workshops in Computing. Springer, 1996."},{"key":"17_CR9","volume-title":"Semantics of specification languages","author":"JF Groote","year":"1993","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."},{"key":"17_CR10","volume-title":"Int. Conf. of Formal Engineering Methods (ICFEM)","author":"AJ Galloway","year":"1997","unstructured":"A. J. Galloway and W. Stoddart. An operational semantics for ZCCS. In M. Hinchey and Shaoying Liu, editors, Int. Conf. of Formal Engineering Methods (ICFEM). IEEE, 1997."},{"issue":"4","key":"17_CR11","doi-asserted-by":"publisher","first-page":"330","DOI":"10.1049\/sej.1989.0045","volume":"6","author":"IJ Hayes","year":"1989","unstructured":"I.J. Hayes and C.B. Jones. Specifications are not (necessarily) executable. Software Engineering Journal, 6(4):330\u2013338, 1989.","journal-title":"Software Engineering Journal"},{"key":"17_CR12","volume-title":"Communicating Sequential Processes","author":"CAR Hoare","year":"1985","unstructured":"C. A. R. Hoare. Communicating Sequential Processes. Prentice-Hall, 1985."},{"key":"17_CR13","doi-asserted-by":"publisher","first-page":"136","DOI":"10.1007\/978-3-540-49676-2_11","volume-title":"ZUM\u201998: The Z formal specification notation","author":"J Jacky","year":"1998","unstructured":"J. Jacky. Analyzing a real-time program with Z. In J.P. Bowen, A. Fett, and M.G. Hinchey, editors, ZUM\u201998: The Z formal specification notation, volume 1493 of Lecture Notes in Computer Science, pages 136\u2013153, 1998."},{"key":"17_CR14","doi-asserted-by":"publisher","first-page":"283","DOI":"10.1007\/BFb0105411","volume-title":"Theorem Proving in Higher Order Logics","author":"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."},{"key":"17_CR15","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1109\/ICSE.1998.671106","volume-title":"The 20th International Conference on Software Engineering (ICSE\u201998)","author":"BP Mahony","year":"1998","unstructured":"B. P. Mahony and J.S. Dong. Blending Object-Z and Timed CSP: An introduction to TCOZ. In The 20th International Conference on Software Engineering (ICSE\u201998), pages 95\u2013104. IEEE Computer Society Press, April 1998."},{"key":"17_CR16","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":"17_CR17","first-page":"205","volume-title":"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 loint Conference on Theory and Practice of Software, volume 1382 of LNCS, pages 205\u2013220, 1998."},{"volume-title":"Revised working draft on enhancements to LOTOS (V4)","year":"1996","key":"17_CR18","unstructured":"J. Quemada, editor. Revised working draft on enhancements to LOTOS (V4). 1996."},{"key":"17_CR19","unstructured":"Rational. UML Notation Guide - version 1.1, September 1997."},{"key":"17_CR20","volume-title":"The Theory and Practice of Concurrency","author":"AW Roscoe","year":"1997","unstructured":"A. W. Roscoe. The Theory and Practice of Concurrency. Prentice-Hall, 1997."},{"key":"17_CR21","first-page":"33","volume-title":"ESORICS 94","author":"AW 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":"17_CR22","first-page":"62","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":"17_CR23","volume-title":"The Z Notation: A Reference Manual","author":"JM Spivey","year":"1992","unstructured":"J. M. Spivey. The Z Notation: A Reference Manual. Prentice-Hall International Series in Computer Science, 2nd edition, 1992.","edition":"2"},{"key":"17_CR24","first-page":"101","volume-title":"International Symposium on Future Software Technology (ISFST)","author":"K Taguchi","year":"1997","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":"17_CR25","volume-title":"Proceedings of the Nineteenth International NATO Summer School","author":"P Zave","year":"1999","unstructured":"P. Zave. Formal description of telecommunication services in Promela and Z. In Proceedings of the Nineteenth International NATO Summer School, 1999. to appear."}],"container-title":["IFM\u201999"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-1-4471-0851-1_17.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,18]],"date-time":"2020-11-18T00:43:05Z","timestamp":1605660185000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-1-4471-0851-1_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9781852331078","9781447108511"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-1-4471-0851-1_17","relation":{},"subject":[],"published":{"date-parts":[[1999]]}}}