{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,6]],"date-time":"2025-04-06T20:10:05Z","timestamp":1743970205829,"version":"3.40.3"},"publisher-location":"Boston, MA","reference-count":22,"publisher":"Springer US","isbn-type":[{"type":"print","value":"9781475710182"},{"type":"electronic","value":"9780387355207"}],"license":[{"start":{"date-parts":[[2000,1,1]],"date-time":"2000-01-01T00:00:00Z","timestamp":946684800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/978-0-387-35520-7_8","type":"book-chapter","created":{"date-parts":[[2012,8,10]],"date-time":"2012-08-10T12:32:14Z","timestamp":1344601934000},"page":"163-182","source":"Crossref","is-referenced-by-count":5,"title":["Using Relational and Behavioural Semantics in the Verification of Object Models"],"prefix":"10.1007","author":[{"given":"Christie","family":"Bolton","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jim","family":"Davies","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"8_CR1","doi-asserted-by":"crossref","unstructured":"D. Amyot and L. Logrippo. Use case maps and lotos for the prototyping and validation of a mobile group call system. Computer Communications, 23 (8), 2000.","DOI":"10.1016\/S0140-3664(99)00242-X"},{"key":"8_CR2","unstructured":"D. Amyot, L. Logrippo, R.J.A. Buhr, and T. Gray. Use case maps for the capture and validation of distributed systems requirements. In Proceedings of RE \u201889, 1999."},{"key":"8_CR3","volume-title":"University of Oxford","author":"C Bolton","year":"2000","unstructured":"C. Bolton. Iodata types and processes. Technical Report PRG-TR01\u201300, University of Oxford, 2000."},{"key":"8_CR4","doi-asserted-by":"crossref","unstructured":"C. Bolton, J. Davies, and J. Woodcock. On the refinement and simulation of data types and processes. In K. Araki, A. Galloway, and K. Taguchi, editors, Proceedings of IFM\u201999. Springer, 1999.","DOI":"10.1007\/978-1-4471-0851-1_15"},{"key":"8_CR5","doi-asserted-by":"crossref","unstructured":"H. Bowman and J. Derrick. A junction between state-based and behavioural specification. In P. Ciancarini, A. Fantechi, and R. Gorrieri, editors, Proceedings of FMOODS \u201889. Kluwer, 1999.","DOI":"10.1007\/978-0-387-35562-7_18"},{"key":"8_CR6","unstructured":"R. J. A. Buhr and R. S. Casselman. Use case maps for object-oriented systems. Prentice-Hall International, 1996."},{"key":"8_CR7","doi-asserted-by":"crossref","unstructured":"S. J. Creese and A. W. Roscoe. Verifying an independent family of inductions simultaneously using data independence and fdr. In Proceedings of FORTE\/PSTV \u201889. Kluwer Academic Press, 1999.","DOI":"10.1007\/978-0-387-35578-8_25"},{"key":"8_CR8","volume-title":"Macmillan","author":"R Duke","year":"2000","unstructured":"R. Duke and G. Rose. Formal Object-Oriented Specification Using Object-Z. Macmillan, 2000. To appear."},{"key":"8_CR9","doi-asserted-by":"crossref","unstructured":"C. Fischer. CSP-OZ: A combination of Object-Z and CSP. In H. Bowman and J. Derrick, editors, Proceedings of FMOODS \u201887,volume 2. Chapman and Hall, 1997.","DOI":"10.1007\/978-0-387-35261-9_29"},{"key":"8_CR10","doi-asserted-by":"crossref","unstructured":"C. Fischer. How to combine Z with a process algebra. In J. Bowen, A. Fett, and M. Hinchey, editors, Proceedings of ZUM \u201888,volume 1493 of LNCS. Springer-Verlag, 1998.","DOI":"10.1007\/978-3-540-49676-2_2"},{"key":"8_CR11","doi-asserted-by":"crossref","unstructured":"R. B. France, J.-M. Bruel, M. M. Larrondo-Petrie, and M. Shroff. Exploring the semantics of UML type structures with Z. In H. Bowman and J. Derrick, editors, Proceedings of FMOODS \u201887,volume 2. Chapman and Hall, 1997.","DOI":"10.1007\/978-0-387-35261-9_17"},{"key":"8_CR12","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":"8_CR13","doi-asserted-by":"crossref","unstructured":"C. A. R. Hoare, J. He, and J. W. Sanders. Prespecification in data refinement. Information Processing Letters, 1987.","DOI":"10.1016\/0020-0190(87)90224-9"},{"key":"8_CR14","unstructured":"ISO. LOTOS \u2014 A formal description technique based on the temporal ordering of observational behaviour. IS 8807, ISO, Geneva, Switzerland, 1989."},{"key":"8_CR15","doi-asserted-by":"crossref","unstructured":"D. Latella, I. Majzik, and M. Massink. Towards a formal operational semantics of UML statechart diagrams. In A. Fantechi P. Ciancarini and R. Gorrieri, editors, Proceedings of FMOODS \u201889. Kluwer, 1999.","DOI":"10.1007\/978-0-387-35562-7_25"},{"key":"8_CR16","unstructured":"R. Lazic. A semantic study of data independence with applications to model checking. PhD thesis, University of Oxford, 1999."},{"key":"8_CR17","unstructured":"precise UML group. http:\/\/www.cs.york.ac.uk\/puml\/, 2000."},{"key":"8_CR18","unstructured":"A. W. Roscoe. The Theory and Practice of Concurrency. Prentice Hall Series in Computer Science, 1998."},{"key":"8_CR19","unstructured":"J. Rumbaugh, I. Jacobson, and G. Booch. The Unified Modeling Language reference manual. Addison-Wesley, 1997."},{"key":"8_CR20","unstructured":"G. Smith and J. Derrick. Refinement and verification of concurrent systems specified in Object-Z and CSP. In Proceedings of ICFEM\u201997. IEEE Computer Press, 1997."},{"key":"8_CR21","volume-title":"Prentice-Hall International","author":"JM Spivey","year":"1992","unstructured":"J. M. Spivey. The Z notation: a reference manual. Prentice-Hall International, 1992."},{"key":"8_CR22","volume-title":"Prentice Hall International Series in Computer Science","author":"JCP Woodcock","year":"1996","unstructured":"J. C. P. Woodcock and J. Davies. Using Z: Specification, Proof and Refinement. Prentice Hall International Series in Computer Science, 1996."}],"container-title":["IFIP Advances in Information and Communication Technology","Formal Methods for Open Object-Based Distributed Systems IV"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-0-387-35520-7_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,6]],"date-time":"2025-04-06T19:29:48Z","timestamp":1743967788000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-0-387-35520-7_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9781475710182","9780387355207"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-0-387-35520-7_8","relation":{},"ISSN":["1868-4238","1868-422X"],"issn-type":[{"type":"print","value":"1868-4238"},{"type":"electronic","value":"1868-422X"}],"subject":[],"published":{"date-parts":[[2000]]}}}