{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,9,13]],"date-time":"2023-09-13T15:28:41Z","timestamp":1694618921785},"reference-count":34,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2000,11,1]],"date-time":"2000-11-01T00:00:00Z","timestamp":973036800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2000,11]]},"abstract":"<jats:title>Abstract.<\/jats:title>\n          <jats:p>\n            CSP-OZ is an integrated formal method which combines the state-oriented specification language Object-Z with the process algebra CSP, thereby allowing a description of static as well as dynamic aspects of a system. Checking correctness of CSP-OZ specifications can be done via a\n            <jats:sc>translation<\/jats:sc>\n            into (FDR-)CSP, on which automatic verification can be performed with the FDR model checker if the state space of the resulting CSP process is not too large to be processed. This paper investigates how\n            <jats:sc>data abstraction<\/jats:sc>\n            techniques can be used to bring a translated specification within range of automatic verification.\n          <\/jats:p>","DOI":"10.1007\/s001650070026","type":"journal-article","created":{"date-parts":[[2002,10,6]],"date-time":"2002-10-06T17:16:50Z","timestamp":1033924610000},"page":"147-164","source":"Crossref","is-referenced-by-count":5,"title":["Data Abstraction Techniques in the Validation of CSP-OZ Specifications"],"prefix":"10.1145","volume":"12","author":[{"given":"Heike","family":"Wehrheim","sequence":"first","affiliation":[{"name":"Universit\u00e4t Oldenburg, Fachbereich Informatik, Oldenburg, Germany, , , , , , DE"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"p_1","volume-title":"The Unified Modeling Language User Guide","author":"Booch G.","year":"1999"},{"key":"p_2","volume-title":"19th ACM POPL","author":"Clarke E. M.","year":"1992"},{"key":"p_3","doi-asserted-by":"crossref","unstructured":"[ClR94] \n      Cleaveland R.\n       and \n      Riely J\n  .: \n  Testing-based abstractions for value-passing systems\n  . In B. Jonsson and J. Parrow editors CONCUR'94 volume \n  836\n   of \n  Lecture Notes in Computer Science pages \n  417\n  -\n  432 Springer 1994\n  .","DOI":"10.1007\/978-3-540-48654-1_31"},{"issue":"2","key":"p_4","doi-asserted-by":"crossref","first-page":"324","DOI":"10.1145\/234528.234740","article-title":"Abstract interpretation","volume":"28","author":"Cousot P.","year":"1996","journal-title":"ACM Computing Surveys"},{"key":"p_5","volume-title":"4th ACM POPL","author":"Cousot P.","year":"1977"},{"key":"p_6","first-page":"573","volume-title":"E.-R","author":"Dams D.","year":"1994"},{"key":"p_7","doi-asserted-by":"crossref","first-page":"511","DOI":"10.1016\/0920-5489(95)00024-O","article-title":"Object-Z: A specification language advocated for the description of standards","volume":"17","author":"Duke R.","year":"1995","journal-title":"Computer Standards and Interfaces"},{"key":"p_8","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 '97)","author":"Fischer C.","year":"1997"},{"key":"p_9","doi-asserted-by":"crossref","unstructured":"[Fis98] \n      Fischer C.\n  : \n  How to combine Z with a process algebra\n  . In J. Bowen A. Fett and M. Hinchey editors ZUM'98: The Z Formal Specification Notation volume \n  1493\n   of \n  LNCS pages \n  5\n  -\n  23\n  . \n  Springer 1998\n  .","DOI":"10.1007\/978-3-540-49676-2_2"},{"key":"p_12","volume-title":"IFM '99: International Workshop on Integrated Formal Methods, Workshops in Computing. Springer","author":"Fischer C.","year":"1999"},{"key":"p_13","volume-title":"October","author":"Ltd","year":"1997"},{"key":"p_14","volume-title":"International Conference of Formal Engineering Methods (ICFEM). IEEE","author":"Galloway A. J.","year":"1997"},{"key":"p_15","volume-title":"Workshops in Computing. Springer","author":"Groote J. F.","year":"1993"},{"issue":"3","key":"p_16","first-page":"229","article-title":"Process simulation and refinement","volume":"1","author":"He J.","year":"1989","journal-title":"Formal Aspects of Computing"},{"key":"p_17","volume-title":": Communicating Sequential Processes","author":"Hoare C. A. R.","year":"1985"},{"key":"p_18","volume-title":"WG7 Enhancements to LOTOS","year":"1998"},{"key":"p_19","doi-asserted-by":"crossref","first-page":"272","DOI":"10.1006\/inco.1993.1069","article-title":"Deciding bisimulation equivalence for a class of non-finite state programs","author":"Jonsson B.","year":"1993","journal-title":"Information and Computation"},{"key":"p_20","doi-asserted-by":"crossref","first-page":"9","DOI":"10.1007\/BF01788563","article-title":"A state-based approach to communicating processes","volume":"3","author":"Josephs M. B.","year":"1988","journal-title":"Distributed Computing"},{"key":"p_21","doi-asserted-by":"crossref","first-page":"283","DOI":"10.1007\/BFb0105411","volume-title":"Theorem Proving in Higher Order Logics, LNCS 1125","author":"Kolyang Santen","year":"1996"},{"key":"p_22","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/BF01384313","article-title":"Property preserving abstractions for the verification of concurrent systems","volume":"6","author":"Loiseaux C.","year":"1995","journal-title":"Formal Methods in System Design"},{"key":"p_23","doi-asserted-by":"crossref","first-page":"95","DOI":"10.1109\/ICSE.1998.671106","volume-title":"20th International Conference on Software Engineering (ICSE'98)","author":"Mahony B. P.","year":"1998"},{"key":"p_24","volume-title":"ORA Canada","author":"Meisels I.","year":"1997"},{"key":"p_25","first-page":"205","volume-title":"Proceedings of the European Joint Conference on Theory and Practice of Software","volume":"1382","author":"Mota A.","year":"1998"},{"key":"p_26","volume-title":"June","author":"[Obj99] Object Management Group","year":"1999"},{"key":"p_27","volume-title":": The Theory and Practice of Concurrency","author":"Roscoe A. W.","year":"1997"},{"key":"p_28","doi-asserted-by":"crossref","unstructured":"[RWW94] \n      Roscoe A. W. Woodcock J. C. P. and \n      Wulf L\n  .: \n  Non-interference through determinism\n  . In D. Gollmann editor ESORICS 94 volume \n  875\n   of \n  LNCS pages \n  33\n  -\n  54\n  . \n  Springer 1994\n  .","DOI":"10.1007\/3-540-58618-0_55"},{"key":"p_29","series-title":"LNCS","first-page":"62","volume-title":"Proceedings of FME","author":"Smith G.","year":"1997"},{"key":"p_30","volume-title":": The Z Notation: A Reference Manual","author":"Spivey J. M.","year":"1992","edition":"2"},{"key":"p_31","first-page":"101","volume-title":"International Symposium on Future Software Technology (ISFST)","author":"Taguchi K.","year":"1997"},{"key":"p_32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"278","DOI":"10.1007\/BFb0039066","volume-title":"Concur '90","author":"van Glabbeek R. J.","year":"1990"},{"key":"p_33","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-48118-4_5","volume-title":"Data abstraction for CSP-OZ","author":"Wehrheim H.","year":"1999"},{"key":"p_34","volume-title":"FASE 2000: Fundamental Aspects of Software Engineering. LNCS 1783 Springer","author":"Wehrheim H.","year":"2000"},{"key":"p_35","first-page":"184","volume-title":"ACM POPL","author":"Wolper P.","year":"1986"},{"key":"p_36","volume-title":"Using Z","author":"Woodcock J.","year":"1996"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s001650070026.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s001650070026\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s001650070026","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:38:13Z","timestamp":1641483493000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s001650070026"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000,11]]},"references-count":34,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2000,11]]}},"alternative-id":["10.1007\/s001650070026"],"URL":"https:\/\/doi.org\/10.1007\/s001650070026","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2000,11]]}}}