{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,9,13]],"date-time":"2023-09-13T16:23:09Z","timestamp":1694622189057},"reference-count":36,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2003,7,1]],"date-time":"2003-07-01T00:00:00Z","timestamp":1057017600000},"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":[[2003,7]]},"abstract":"<jats:title>Abstract.<\/jats:title>\n          <jats:p>This paper is concerned with methods for refinement of specifications written using a combination of Object-Z and CSP. Such a combination has proved to be a suitable vehicle for specifying complex systems which involve state and behaviour, and several proposals exist for integrating these two languages. The basis of the integration in this paper is a semantics of Object-Z classes identical to CSP processes. This allows classes specified in Object-Z to be combined using CSP operators. It has been shown that this semantic model allows state-based refinement relations to be used on the Object-Z components in an integrated Object-Z\/CSP specification. However, the current refinement methodology does not allow the structure of a specification to be changed in a refinement, whereas a full methodology would, for example, allow concurrency to be introduced during the development life-cycle. In this paper, we tackle these concerns and discuss refinements of specifications written using Object-Z and CSP where we change the structure of the specification when performing the refinement. In particular, we develop a set of structural simulation rules which allow single components to be refined to more complex specifications involving CSP operators. The soundness of these rules is verified against the common semantic model and they are illustrated via a number of examples.<\/jats:p>","DOI":"10.1007\/s00165-003-0002-9","type":"journal-article","created":{"date-parts":[[2003,12,10]],"date-time":"2003-12-10T21:38:13Z","timestamp":1071092293000},"page":"1-27","source":"Crossref","is-referenced-by-count":11,"title":["Structural Refinement of Systems Specified in Object-Z and CSP"],"prefix":"10.1145","volume":"15","author":[{"given":"John","family":"Derrick","sequence":"first","affiliation":[{"name":"Computing Laboratory, University of Kent, CT2 7NF, Canterbury, Kent, UK"},{"name":"Computing Laboratory, University of Kent, CT2 7NF, Canterbury, Kent, UK"}]},{"given":"Graeme","family":"Smith","sequence":"additional","affiliation":[{"name":"Software Verification Research Centre, University of Queensland 4072, Australia"}]}],"member":"320","reference":[{"key":"p_1","volume-title":"International conference on Integrated Formal Methods 1999 (IFM'99)","author":"Araki K.","year":"1999"},{"key":"p_2","volume-title":"A Singleton Failures Semantics for Communicating Sequential Processes. Submitted for publication","author":"Bolton C.","year":"2002"},{"key":"p_3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"225","DOI":"10.1007\/3-540-47884-1_13","volume-title":"Integrated Formal Methods (IFM","author":"Bolton C.","year":"2002"},{"key":"p_4","first-page":"273","volume-title":"Araki et al. [AGT99]","author":"Bolton C."},{"key":"p_5","volume-title":"Pittsburgh Symposium on Concurrency","volume":"197","author":"Brookes S. D.","year":"1985"},{"key":"p_6","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4471-0257-1","volume-title":"Refinement in Z and Object-Z","author":"Derrick J.","year":"2001"},{"key":"p_7","doi-asserted-by":"crossref","unstructured":"[DBB97] \n      Derrick J. Boiten E. A. Bowman H.\n       and \n      Steen M. W. A\n  .: \n  Weak refinement in Z\n  . In J. P. Bowen M. G. Hinchey and D. Till editors. ZUM'97: The Z Formal Specification Notation volume \n  1212\n   of \n  Lecture Notes in Computer Science pages \n  369\n  -\n  388\n  . \n  Springer-Verlag April \n  1997\n  .","DOI":"10.1007\/BFb0027298"},{"key":"p_8","first-page":"125","article-title":"A","volume":"10","author":"Derrick J.","year":"1998","journal-title":"Formal Aspects of Computing"},{"key":"p_9","volume-title":"REFINE - a FLoC'02 FME workshop, Electronic Notes in Theoretical Computer Science","author":"Derrick J.","year":"2002"},{"key":"p_10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"194","DOI":"10.1007\/3-540-40911-4_12","volume-title":"International conference on Integrated Formal Methods 2000 (IFM'00)","author":"Derrick J.","year":"2000"},{"key":"p_11","doi-asserted-by":"crossref","first-page":"423","DOI":"10.1007\/978-0-387-35261-9_29","volume-title":"Second IFIP International conference on Formal Methods for Open Object-based Distributed Systems","author":"Fischer C.","year":"1997"},{"key":"p_12","doi-asserted-by":"crossref","unstructured":"[Fis98] \n      Fischer C.\n  : \n  How to combine Z with a process algebra\n  . In J. P. Bowen A. Fett and M. G. Hinchey editors. ZUM'98: The Z Formal Specification Notation volume \n  1493\n   of \n  Lecture Notes in Computer Science pages \n  5\n  -\n  23\n  . \n  Springer-Verlag September \n  1998\n  .","DOI":"10.1007\/978-3-540-49676-2_2"},{"key":"p_14","first-page":"315","volume-title":"Araki et al. [AGT99]","author":"Fischer C."},{"key":"p_15","volume-title":"Failures-Divergences Refinement: FDR","author":"Ltd","year":"1997"},{"key":"p_16","first-page":"272","volume-title":"Hinchey and Liu [HiL97]","author":"Galloway A."},{"key":"p_17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"187","DOI":"10.1007\/3-540-16442-1_14","volume-title":"Proc. ESOP 86","author":"He J.","year":"1986"},{"key":"p_18","volume-title":"Hiroshima","author":"Hinchey M. G.","year":"1997"},{"key":"p_19","volume-title":": Communicating Sequential Processes","author":"Hoare C. A. R.","year":"1985"},{"key":"p_20","volume-title":"The Theory and Practice of Refinement. Butterworths","author":"He J.","year":"1989"},{"key":"p_21","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_22","first-page":"335","volume-title":"International Conference on Integrated Formal Methods (IFM'99)","author":"MacColl I.","year":"1999"},{"key":"p_23","volume-title":"20th International Conference on Software Engineering (ICSE'98)","author":"Mahony B. P.","year":"1998"},{"key":"p_24","first-page":"1166","volume-title":"World Congress on Formal Methods (FM'99)","author":"Mahony B. P.","year":"1999"},{"key":"p_25","volume-title":"Communication and Concurrency","author":"Milner R.","year":"1989"},{"key":"p_26","series-title":"International Series in Computer Science","volume-title":": The Theory and Practice of Concurrency","author":"Roscoe A. W.","year":"1998"},{"issue":"3","key":"p_27","doi-asserted-by":"crossref","first-page":"289","DOI":"10.1007\/BF01211075","article-title":"A fully abstract semantics of classes for Object-Z","volume":"7","author":"Smith G.","year":"1995","journal-title":"Formal Aspects of Computing"},{"key":"p_28","doi-asserted-by":"crossref","unstructured":"[Smi97] \n      Smith G.\n  : \n  A semantic integration of Object-Z and CSP for the specification of concurrent systems\n  . In J. Fitzgerald C. B. Jones and P. Lucas editors. FME'97: Industrial Application and Strengthened Foundations of Formal Methods volume \n  1313\n   of \n  Lecture Notes in Computer Science pages \n  62\n  -\n  81\n  . \n  Springer-Verlag September \n  1997\n  .","DOI":"10.1007\/3-540-63533-5_4"},{"key":"p_29","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-5265-9","volume-title":"The Object-Z specification language","author":"Smith G.","year":"2000"},{"key":"p_30","first-page":"293","volume-title":"Hinchey and Liu [HiL97]","author":"Smith G."},{"key":"p_31","doi-asserted-by":"crossref","first-page":"249","DOI":"10.1023\/A:1011269103179","article-title":"Specification, refinement and verification of concurrent systems - an integration of Object-Z and CSP","volume":"18","author":"Smith G.","year":"2001","journal-title":"Formal Methods in Systems Design"},{"key":"p_32","series-title":"International Series in Computer Science","volume-title":": The Z notation: A reference manual","author":"Spivey J. M.","year":"1992","edition":"2"},{"key":"p_33","first-page":"29","volume-title":"International Conference on Integrated Formal Methods (IFM'99)","author":"S\u00fchl C.","year":"1999"},{"key":"p_34","first-page":"283","volume-title":"Hinchey and Liu [HiL97]","author":"Taguchi K."},{"key":"p_35","first-page":"437","volume-title":"International Conference on Integrated Formal Methods 1999 (IFM'99)","author":"Treharne H.","year":"1999"},{"key":"p_36","volume-title":"Using Z: Specification, Refinement, and Proof","author":"Woodcock J. C. P.","year":"1996"},{"key":"p_37","series-title":"Lecture Notes in Computer Science","volume-title":"Refinement of state-based concurrent systems","author":"Woodcock J. C. P.","year":"1990"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-003-0002-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-003-0002-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-003-0002-9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,3]],"date-time":"2022-01-03T16:10:05Z","timestamp":1641226205000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-003-0002-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,7]]},"references-count":36,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2003,7]]}},"alternative-id":["10.1007\/s00165-003-0002-9"],"URL":"https:\/\/doi.org\/10.1007\/s00165-003-0002-9","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2003,7]]}}}