{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,15]],"date-time":"2025-08-15T00:29:51Z","timestamp":1755217791715,"version":"3.43.0"},"reference-count":49,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2001,5,1]],"date-time":"2001-05-01T00:00:00Z","timestamp":988675200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2001,5,1]],"date-time":"2001-05-01T00:00:00Z","timestamp":988675200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Formal Methods in System Design"],"published-print":{"date-parts":[[2001,5]]},"DOI":"10.1023\/a:1011269103179","type":"journal-article","created":{"date-parts":[[2002,12,23]],"date-time":"2002-12-23T04:18:21Z","timestamp":1040617101000},"page":"249-284","source":"Crossref","is-referenced-by-count":40,"title":["Specification, Refinement and Verification of Concurrent Systems\u2014An Integration of Object-Z and CSP"],"prefix":"10.1007","volume":"18","author":[{"given":"Graeme","family":"Smith","sequence":"first","affiliation":[]},{"given":"John","family":"Derrick","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"322922_CR1","first-page":"221","volume-title":"Z User Workshop, Workshops in Computing","author":"M. Benjamin","year":"1989","unstructured":"M. Benjamin, \u201cA message passing system: An example of combining CSP and Z,\u201d in J.E. Nicholls (Ed.), Z User Workshop, Workshops in Computing, Springer-Verlag, Oxford, 1989, pp. 221\u2013228."},{"key":"322922_CR2","first-page":"644","volume":"1313","author":"E.A. Boiten","year":"1997","unstructured":"E.A. Boiten, H. Bowman, J. Derrick, and M.W.A. Steen, \u201cViewpoint consistency in Z and LOTOS: A case study,\u201d in J. Fitzgerald, C.B. Jones, and P. Lucas (Eds.), Formal Methods Europe (FME '97), Graz, Austria, September 1997, Lecture Notes in Computer Science, Vol. 1313, Springer-Verlag, pp. 644\u2013664.","journal-title":"Formal Methods Europe (FME '97)"},{"issue":"1","key":"322922_CR3","doi-asserted-by":"crossref","first-page":"25","DOI":"10.1016\/0169-7552(87)90085-7","volume":"14","author":"T. Bolognesi","year":"1998","unstructured":"T. Bolognesi and E. Brinksma, \u201cIntroduction to the ISO specification language LOTOS,\u201d Computer Networks and ISDN Systems, Vol. 14, No. 1, pp. 25\u201329, 1998.","journal-title":"Computer Networks and ISDN Systems"},{"key":"322922_CR4","doi-asserted-by":"crossref","unstructured":"C. Bolton, J. Davies, and J.C.P. Woodcock, \u201cOn the refinement and simulation of data types and processes,\u201d in K. Araki, A. Galloway, and K. Taguchi (Eds.), International Conference on Integrated Formal Methods 1999 (IFM '99), Springer, July 1999, pp. 273\u2013292.","DOI":"10.1007\/978-1-4471-0851-1_15"},{"issue":"3","key":"322922_CR5","doi-asserted-by":"crossref","first-page":"560","DOI":"10.1145\/828.833","volume":"31","author":"S.D. Brookes","year":"1984","unstructured":"S.D. Brookes, C.A.R. Hoare, and A.W. Roscoe, \u201cA theory of communicating sequential processes,\u201d Journal of the ACM, Vol. 31, No. 3, pp. 560\u2013599, 1984.","journal-title":"Journal of the ACM"},{"key":"322922_CR6","first-page":"281","volume":"197","author":"S.D. Brookes","year":"1985","unstructured":"S.D. Brookes and A.W. Roscoe, \u201cAn improved failures model for communicating processes,\u201d in Pittsburgh Symposium on Concurrency, Lecture Notes in Computer Science, Vol. 197, Springer-Verlag, 1985, pp. 281\u2013305.","journal-title":"Pittsburgh Symposium on Concurrency"},{"key":"322922_CR7","unstructured":"M.J. Butler, \u201cA CSP Approach to Action Systems,\u201d Ph.D. Thesis, Oxford University, 1992."},{"issue":"1","key":"322922_CR8","doi-asserted-by":"crossref","first-page":"37","DOI":"10.1007\/BF01214622","volume":"7","author":"M.J. Butler","year":"1995","unstructured":"M.J. Butler and C.C. Morgan, \u201cAction systems, unbounded nondeterminism, and infinite traces,\u201d Formal Aspects of Computing, Vol. 7, No. 1, pp. 37\u201353, 1995.","journal-title":"Formal Aspects of Computing"},{"key":"322922_CR9","doi-asserted-by":"crossref","unstructured":"J. Derrick and E.A. Boiten, \u201cSeparating component and context specification using promotion,\u201d in K. Araki, A. Galloway, and K. Taguchi (Eds.), International Conference on Integrated Formal Methods 1999 (IFM'99), Springer, July 1999, pp. 293\u2013312.","DOI":"10.1007\/978-1-4471-0851-1_16"},{"key":"322922_CR10","doi-asserted-by":"crossref","first-page":"369","DOI":"10.1007\/BFb0027298","volume-title":"ZUM'97: The Z formal specification notation","author":"J. Derrick","year":"1997","unstructured":"J. Derrick, E.A. Boiten, H. Bowman, and M.W.A. Steen,\u201cWeak refinement in Z,\u201d in J.P. Bowen, M.G. Hinchey, and D. Till (Eds.), ZUM'97: The Z formal specification notation, Lecture Notes in Computer Science, Vol. 1212, Springer-Verlag, Reading, April 1997, pp. 369\u2013388."},{"key":"322922_CR11","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1007\/s001650050007","volume":"10","author":"J. Derrick","year":"1998","unstructured":"J. Derrick, E.A. Boiten, H. Bowman, and M.W.A. Steen, \u201cSpecifying and refining internal operations in Z,\u201d Formal Aspects of Computing, Vol. 10, pp. 125\u2013159, 1998.","journal-title":"Formal Aspects of Computing"},{"key":"322922_CR12","doi-asserted-by":"crossref","unstructured":"J. Derrick, E.A. Boiten, H. Bowman, and M.W.A. Steen, \u201cSupporting ODP\u2014Translating LOTOS to Z,\u201d in First IFIP InternationalWorkshop on Formal Methods for Open Object-based Distributed Systems, Chapman & Hall, 1996.","DOI":"10.1007\/978-0-387-35082-0_29"},{"key":"322922_CR13","first-page":"242","volume":"428","author":"D. Duke","year":"1990","unstructured":"D. Duke and R. Duke, \u201cTowards a semantics for Object-Z,\u201d in D. Bjorner, C.A.R. Hoare, and H. Langmaack (Eds.), VDM'90: VDM and Z! Lecture Notes in Computer Science, Vol. 428, Springer-Verlag, 1990, pp. 242\u2013262.","journal-title":"VDM'90: VDM and Z! Lecture Notes in Computer Science"},{"key":"322922_CR14","doi-asserted-by":"crossref","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, \u201cObject-Z: A specification language advocated for the description of standards,\u201d Computer Standards and Interfaces, Vol. 17, pp. 511\u2013533, 1995.","journal-title":"Computer Standards and Interfaces"},{"key":"322922_CR15","doi-asserted-by":"crossref","first-page":"203","DOI":"10.1007\/BFb0019445","volume":"489","author":"H. ehrich","year":"1995","unstructured":"H. Ehrich, J. Goguen, and A. Sernadas, \u201cA categorical theory of objects as observed processes,\u201d in J.W. Bakker, W.P. de Roever, and G. Rozenberg (Eds.), Foundations of Object-Oriented Languages, Lecture Notes in Computer Science, Vol. 489, Springer-Verlag, 1991, pp. 203\u2013228.","journal-title":"Foundations of Object-Oriented Languages"},{"key":"322922_CR16","doi-asserted-by":"crossref","first-page":"85","DOI":"10.1007\/BF01887199","volume":"1","author":"M. Nielsen","year":"1989","unstructured":"M. Nielsen et al., \u201cThe RAISE language, methods and tools,\u201d Formal Aspects of Computing, Vol. 1, pp. 85\u2013114, 1989.","journal-title":"Formal Aspects of Computing"},{"key":"322922_CR17","doi-asserted-by":"crossref","unstructured":"C. Fischer, \u201cCSP-OZ\u2014A combination of CSP and Object-Z,\u201d in H. Bowman and J. Derrick (Eds.), Second IFIP International Conference on Formal Methods for Open Object-based Distributed Systems, Chapman & Hall, July 1997, pp. 423\u2013438.","DOI":"10.1007\/978-0-387-35261-9_29"},{"key":"322922_CR18","doi-asserted-by":"crossref","unstructured":"C. Fischer and G. Smith, \u201cCombining CSP and Object-Z: Finite or infinite trace semantics,\u201d in T. Higashino and A. Togashi (Eds.), FORTE\/PSTV'97, Osaka, Japan, November 1997. Chapman & Hall, pp. 503\u2013518.","DOI":"10.1007\/978-0-387-35271-8_31"},{"key":"322922_CR19","unstructured":"J. He, \u201cProcess refinement,\u201d in J. McDermid (Ed.), The Theory and Practice of Refinement, Butterworths, 1989."},{"key":"322922_CR20","doi-asserted-by":"crossref","unstructured":"M. Heisel and C. S\u00fchl, \u201cFormal specification of safety-critical software with Z and real-time CSP,\u201d in E. Schoitsch (Ed.), Proceedings 15th International Conference on Computer Safety, Reliability and Security, Springer, 1996, pp. 31\u201345.","DOI":"10.1007\/978-1-4471-0937-2_3"},{"key":"322922_CR21","unstructured":"C.A.R. Hoare, Communicating Sequential Processes, International Series in Computer Science, Prentice-Hall, 1985."},{"key":"322922_CR22","unstructured":"ITU Recommendation X.901\u2013904, Open Distributed Processing\u2014Reference Model\u2014Parts 1\u20134, July 1995."},{"key":"322922_CR23","unstructured":"C.B. Jones, Systematic SoftwareDevelopment usingVDM, International Series in Computer Science, Prentice-Hall, 1986."},{"key":"322922_CR24","doi-asserted-by":"crossref","first-page":"9","DOI":"10.1007\/BF01788563","volume":"3","author":"M.B. Josephs","year":"1988","unstructured":"M.B. Josephs, \u201cA state-based approach to communicating processes,\u201d Distributed Computing, Vol. 3, pp. 9\u201318, 1988.","journal-title":"Distributed Computing"},{"key":"322922_CR25","unstructured":"Formal Systems (Europe) Ltd., Failures-Divergences Refinement: FDR 2, Oct. 1997, FDR2 User Manual."},{"key":"322922_CR26","doi-asserted-by":"crossref","unstructured":"I. MacColl, \u201cSpecifying interactive systems in Object-Z and CSP,\u201d in K. Araki, A. Galloway, and K. Taguchi (Eds.), International Conference on Integrated Formal Methods (IFM'99), Springer-Verlag, 1999, pp. 335\u2013352.","DOI":"10.1007\/978-1-4471-0851-1_18"},{"key":"322922_CR27","unstructured":"B.P. Mahony and J.S. Dong, \u201cBlending Object-Z and timed CSP: An introduction to TCOZ,\u201d in K. Futatsugi, R. Kemmerer, and K. Torii (Eds.), 20th International Conference on Software Engineering (ICSE'98), IEEE Press, 1998."},{"key":"322922_CR28","doi-asserted-by":"crossref","unstructured":"B.P. Mahony and J.S. Dong, \u201cSensors and actuators in TCOZ,\u201d in J.M. Wing, J.C.P. Woodcock, and J. Davies (Eds.), World Congress on Formal Methods (FM'99), Springer-Verlag, 1999, pp. 1166\u20131185.","DOI":"10.1007\/3-540-48118-4_12"},{"key":"322922_CR29","unstructured":"R. Milner, Communication and Concurrency, International Series in Computer Science, Prentice-Hall, 1989."},{"key":"322922_CR30","unstructured":"A.W. Roscoe, The Theory and Practice of Concurrency, International Series in Computer Science, Prentice-Hall, 1998."},{"key":"322922_CR31","doi-asserted-by":"crossref","unstructured":"A.W. Roscoe, \u201cAn alternative order for the failures model,\u201d Journal of Logic and Computation, Vol. 3, No. 2, 1993.","DOI":"10.1093\/logcom\/2.5.557"},{"key":"322922_CR32","doi-asserted-by":"crossref","unstructured":"A.W. Roscoe, \u201cUnbounded nondeterminism in CSP,\u201d Journal of Logic and Computation, Vol. 3, No. 2, 1993.","DOI":"10.1093\/logcom\/3.2.131"},{"key":"322922_CR33","doi-asserted-by":"crossref","first-page":"160","DOI":"10.1007\/BFb0040257","volume":"442","author":"A.W. Roscoe","year":"1989","unstructured":"A.W. Roscoe and G. Barrett, \u201cUnbounded nondeterminism in CSP,\u201d in Mathematical Foundations of Programming Semantics, Lecture Notes in Computer Science, Vol. 442, Springer-Verlag, 1989, pp. 160\u2013193.","journal-title":"Mathematical Foundations of Programming Semantics"},{"key":"322922_CR34","doi-asserted-by":"crossref","first-page":"307","DOI":"10.1007\/BFb0015251","volume":"1000","author":"M. Shaw","year":"1995","unstructured":"M. Shaw and D. Garlan, \u201cFormulations and formalisms in software architecture,\u201d in J. van Leeuwen (Ed.), Computer Science Today: Recent Trends and Developments, Lecture Notes in Computer Science, Vol. 1000, Springer-Verlag, 1996, pp. 307\u2013323.","journal-title":"Computer Science Today: Recent Trends and Developments"},{"key":"322922_CR35","first-page":"276","volume":"967","author":"G. Smith","year":"1995","unstructured":"G. Smith, \u201cExtending W for Object-Z,\u201d in J. Bowen and M. Hinchey (Eds.), 9th International Conference of Z Users, Lecture Notes in Computer Science, Vol. 967, Springer-Verlag, 1995, pp. 276\u2013295.","journal-title":"9th International Conference of Z Users"},{"key":"322922_CR36","series-title":"Technical Report","volume-title":"Formal verification of Object-Z specifications","author":"G. Smith","year":"1995","unstructured":"G. Smith, \u201cFormal verification of Object-Z specifications,\u201d Technical Report 95-55, Software Verification Research Centre, Department of Computer Science, University of Queensland, Australia, 1995."},{"issue":"3","key":"322922_CR37","doi-asserted-by":"crossref","first-page":"289","DOI":"10.1007\/BF01211075","volume":"7","author":"G. Smith","year":"1995","unstructured":"G. Smith, \u201cA fully abstract semantics of classes for Object-Z,\u201d Formal Aspects of Computing, Vol. 7, No. 3, pp. 289\u2013313, 1995.","journal-title":"Formal Aspects of Computing"},{"key":"322922_CR38","first-page":"62","volume":"1313","author":"G. Smith","year":"1997","unstructured":"G. Smith, \u201cA semantic integration of Object-Z and CSP for the specification of concurrent systems,\u201d in J. Fitzgerald, C.B. Jones, and P. Lucas (Eds.), Formal Methods Europe (FME '97), Graz, Austria, Sept. 1997, Lecture Notes in Computer Science, Vol. 1313, Springer-Verlag, pp. 62\u201381.","journal-title":"Formal Methods Europe (FME '97)"},{"key":"322922_CR39","doi-asserted-by":"crossref","unstructured":"G. Smith, The Object-Z Specification Language, Kluwer Academic Publishers, 2000.","DOI":"10.1007\/978-1-4615-5265-9"},{"key":"322922_CR40","doi-asserted-by":"crossref","unstructured":"G. Smith and J. Derrick, \u201cRefinement and verification of concurrent systems specified in Object-Z and CSP,\u201d in M. Hinchey and Shaoying Liu (Eds.), First IEEE International Conference on Formal Engineering Methods (ICFEM '97), Hiroshima, Japan, Nov. 1997, IEEE Computer Society, pp. 293\u2013302.","DOI":"10.1109\/ICFEM.1997.630436"},{"key":"322922_CR41","unstructured":"J.M. Spivey, The Z Notation: A Reference Manual, 2nd Ed., International Series in Computer Science, Prentice-Hall, 1992."},{"key":"322922_CR42","doi-asserted-by":"crossref","unstructured":"C. S\u00fchl, \u201cRT-Z: An integration of Z and timed CSP,\u201d in K. Araki, A. Galloway, and K. Taguchi (Eds.), International Conference on Integrated Formal Methods (IFM'99), Springer-Verlag, 1999, pp. 29\u201348.","DOI":"10.1007\/978-1-4471-0851-1_3"},{"key":"322922_CR43","first-page":"318","volume":"1313","author":"H. Tej","year":"1997","unstructured":"H. Tej and B. Wolff, \u201cA corrected failure-divergence-model for CSP in Isabelle\/HOL,\u201d in J. Fitzgerald, C.B. Jones, and P. Lucas (Eds.), Formal Methods Europe (FME '97), Lecture Notes in Computer Science, Vol. 1313, Springer-Verlag, 1997, pp. 318\u2013337.","journal-title":"Formal Methods Europe (FME '97)"},{"key":"322922_CR44","series-title":"Technical Report","volume-title":"Process algebra semantics for POOL","author":"F.W. Vaandrager","year":"1991","unstructured":"F.W. Vaandrager, \u201cProcess algebra semantics for POOL,\u201d Technical Report CS-R8629, Centre for Mathematics and Computer Science, Amsterdam, The Netherlands, 1991."},{"key":"322922_CR45","doi-asserted-by":"crossref","first-page":"307","DOI":"10.1007\/3-540-60973-3_94","volume":"1051","author":"M. Weber","year":"1996","unstructured":"M. Weber, \u201cCombining statecharts and Z for the design of safety-critical systems,\u201d in M.-C. Gaudel and J.C.P. Woodcock (Eds.), FME '96\u2014Industrial Benefits and Advances in Formal Methods, Lecture Notes in Computer Science, Vol. 1051, Springer-Verlag, 1996, pp. 307\u2013326.","journal-title":"FME '96\u2014Industrial Benefits and Advances in Formal Methods"},{"key":"322922_CR46","doi-asserted-by":"crossref","unstructured":"J.C.P. Woodcock and S.M. Brien, \u201cW: A logic for Z,\u201d in J.E. Nicholls (Ed.), Z User Workshop, Workshops in Computing, Springer-Verlag, 1992, pp. 77\u201398.","DOI":"10.1007\/978-1-4471-3203-5_4"},{"key":"322922_CR47","unstructured":"J.C.P. Woodcock and J. Davies, Using Z: Specification, Refinement, and Proof, International Series in Computer Science, Prentice-Hall, 1996."},{"key":"322922_CR48","doi-asserted-by":"crossref","unstructured":"J.C.P. Woodcock and C.C. Morgan, \u201cRefinement of state-based concurrent systems,\u201d in D. Bjorner, C.A.R. Hoare, and H. Langmaack (Eds.), VDM'90: VDM and Z! Lecture Notes in Computer Science, Vol. 428, Springer-Verlag, 1990.","DOI":"10.1007\/3-540-52513-0_18"},{"key":"322922_CR49","doi-asserted-by":"crossref","unstructured":"A. Yonezawa and M. Tokoro (Eds.), Object-Oriented Concurrent Programming, MIT Press, 1987.","DOI":"10.1016\/B978-0-934613-63-7.50046-2"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1011269103179.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1011269103179\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1011269103179.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,5]],"date-time":"2025-08-05T19:09:03Z","timestamp":1754420943000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1011269103179"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001,5]]},"references-count":49,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2001,5]]}},"alternative-id":["322922"],"URL":"https:\/\/doi.org\/10.1023\/a:1011269103179","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"type":"print","value":"0925-9856"},{"type":"electronic","value":"1572-8102"}],"subject":[],"published":{"date-parts":[[2001,5]]}}}