{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,9,13]],"date-time":"2023-09-13T16:23:35Z","timestamp":1694622215105},"reference-count":45,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2002,5,1]],"date-time":"2002-05-01T00:00:00Z","timestamp":1020211200000},"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":[[2002,5]]},"abstract":"<jats:title>Abstract.<\/jats:title>\n          <jats:p>\n            This paper discusses the separation of components from the contexts in which they are used, and how this separation can be supported whilst using different specification languages. There are a number of ways in which this might be possible and here we show how the technique of promotion in Object-Z can be used to combine components which are specified using process algebras. We outline two approaches. The first is to separate out a single specification into a number of distinct\n            <jats:italic>viewpoints<\/jats:italic>\n            (i.e., partial specifications), each possibly written in a different notation. These viewpoints can be developed separately, but combined if necessary by a process of translation and unification. The alternative approach we discuss is to use a single hybrid language which is composed of a combination of notations, which we illustrate here by combining CSP and Object-Z. We illustrate both approaches with a simple example, and also consider how such component-based descriptions can be refined, which involves addressing the question of compositionality.\n          <\/jats:p>","DOI":"10.1007\/s001650200002","type":"journal-article","created":{"date-parts":[[2003,12,10]],"date-time":"2003-12-10T21:38:13Z","timestamp":1071092293000},"page":"111-127","source":"Crossref","is-referenced-by-count":4,"title":["Combining Component Specifications in Object-Z and CSP"],"prefix":"10.1145","volume":"13","author":[{"given":"John","family":"Derrick","sequence":"first","affiliation":[{"name":"Computing Laboratory, University of Kent, Canterbury, CT2 7NF, UK., , , , , , GB"}]},{"given":"Eerke","family":"Boiten","sequence":"additional","affiliation":[{"name":"Computing Laboratory, University of Kent, Canterbury, CT2 7NF, UK., , , , , , GB"}]}],"member":"320","reference":[{"issue":"1","key":"p_1","first-page":"25","article-title":"Introduction to the ISO Specification Language LOTOS","volume":"14","author":"Bo","year":"1988","journal-title":"Computer Networks and ISDN Systems"},{"key":"p_2","first-page":"503","volume-title":"Computer Networks","author":"Boiten E. A.","year":"2000"},{"issue":"1","key":"p_3","doi-asserted-by":"crossref","first-page":"29","DOI":"10.1016\/S0167-6423(99)00006-4","article-title":": Constructive consistency checking for partial specification","volume":"35","author":"Boiten E. A.","year":"1999","journal-title":"Z. Science of Computer Programming"},{"key":"p_4","doi-asserted-by":"crossref","first-page":"457","DOI":"10.1016\/0920-5489(95)00021-L","volume":"17","author":"Bowman H.","year":"1995","journal-title":"FDTs for ODP. Computer Standards and Interfaces"},{"key":"p_5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/b68208","volume-title":"editors","author":"Bowen J. P.","year":"1998"},{"issue":"3","key":"p_6","doi-asserted-by":"crossref","first-page":"560","DOI":"10.1145\/828.833","article-title":"A theory of communicating sequential processes","volume":"31","author":"Brookes S. D.","year":"1984","journal-title":"Journal of the ACM"},{"key":"p_7","volume-title":"Pittsburgh Symposium on Concurrency","volume":"197","author":"Br","year":"1985"},{"key":"p_8","volume-title":"Z in practice","author":"Barden R.","year":"1994"},{"key":"p_9","first-page":"349","volume-title":"B. Sarikaya and G. v","author":"Brinksma E.","year":"1986"},{"key":"p_10","doi-asserted-by":"crossref","unstructured":"[\n      But\n    99] Butler M.\n  : \n  csp2B: A practical approach to combining CSP and B\n  . In J.M. Wing J.C.P. Woodcock and J. Davies editors FM'99 World Congress on Formal Methods in the Development of Computing Systems volume \n  1708\n   of \n  LNCS pages \n  490\n  -\n  508 Berlin 1999\n  . \n  Springer\n  .","DOI":"10.1007\/3-540-48119-2_28"},{"key":"p_11","first-page":"293","volume-title":"International Conference on Integrated Formal Methods 1999 (IFM'99)","author":"De","year":"1999"},{"key":"p_12","doi-asserted-by":"crossref","unstructured":"[\n      De\n    B99b] Derrick J. and \n      Boiten E. A\n  .: \n  Non-atomic refinement in Z\n  . In J. M. Wing J. C. P. Woodcock and J. Davies editors FM'99 World Congress on Formal Methods in the Development of Computing Systems volume \n  1708\n   of \n  Lecture Notes in Computer Science pages \n  1477\n  -\n  1496 Berlin 1999\n  . \n  Springer-Verlag\n  .","DOI":"10.1007\/3-540-48118-4_28"},{"key":"p_13","volume-title":"Computing Laboratory","author":"De","year":"2000"},{"key":"p_14","volume-title":"Refinement in Z and Object-Z, Foundations and Advanced Applications","author":"De","year":"2001"},{"key":"p_15","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1007\/s001650050007","article-title":": Specifying and refining internal operations","volume":"10","author":"Derrick J.","year":"1998","journal-title":"Z. Formal Aspects of Computing"},{"key":"p_16","first-page":"251","volume-title":"Computer Standards and Interfaces","author":"Derrick J.","year":"1999"},{"key":"p_17","volume-title":"CUP","author":"de Roever W.-P.","year":"1998"},{"key":"p_18","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_19","first-page":"194","volume-title":"International Conference on Integrated Formal Methods 2000 (IFM'00)","volume":"1945","author":"De","year":"2000"},{"key":"p_20","first-page":"423","volume-title":"Second IFIP International Conference on Formal Methods for Open Object-Based Distributed Systems","author":"Fis","year":"1997"},{"key":"p_21","first-page":"5","volume-title":"Bowen et al. [BFH98]","author":"Fis"},{"key":"p_23","first-page":"503","volume-title":"Combining CSP and Object-Z: finite or infinite trace semantics","author":"Fi","year":"1997"},{"key":"p_24","first-page":"272","volume-title":"Hinchey and Liu [HiL97]","author":"Ga A."},{"key":"p_25","volume-title":"Data Refinement in a Categorical Setting, Technical Monograph, number PRG-90","author":"He","year":"1990"},{"key":"p_26","volume-title":"editors","author":"Hi","year":"1997"},{"key":"p_27","volume-title":": Communicating Sequential Processes","author":"Hoa","year":"1985"},{"key":"p_28","volume-title":"Parts","author":"Recommendation X.","year":"1995"},{"key":"p_29","doi-asserted-by":"crossref","first-page":"9","DOI":"10.1007\/BF01788563","article-title":"A state-based approach to communicating processes","volume":"3","author":"Jos","year":"1988","journal-title":"Distributed Computing"},{"key":"p_30","first-page":"27","volume-title":"Workshops in Computing","author":"Lup","year":"1991"},{"key":"p_31","first-page":"308","volume-title":"Bowen et al. [BFH98]","author":"Ma"},{"key":"p_32","volume-title":"20th International Conference on Software Engineering (ICSE'98)","author":"Ma","year":"1998"},{"issue":"2","key":"p_33","doi-asserted-by":"crossref","first-page":"150","DOI":"10.1109\/32.841115","article-title":"Timed communicating Object-Z","volume":"26","author":"Ma","year":"2000","journal-title":"IEEE Transactions on Software Engineering"},{"key":"p_34","doi-asserted-by":"crossref","unstructured":"[Old98] Olderog E.-R.: Combining specification techniques for processes data and time. In Bowen et al. [BFH98] page 192. Abstract.","DOI":"10.1007\/978-3-540-49676-2_14"},{"key":"p_35","first-page":"293","volume-title":"Hinchey and Liu [HiL97]","author":"Sm"},{"key":"p_36","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":"Sm","year":"2001","journal-title":"Formal Methods in System Design"},{"issue":"3","key":"p_37","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":"Smi","year":"1995","journal-title":"Formal Aspects of Computing"},{"key":"p_38","first-page":"62","volume-title":"Formal Methods Europe (FME '97), LNCS 1313","author":"Smi","year":"1997"},{"key":"p_39","volume-title":"The Object-Z specification language","author":"Smi","year":"2000"},{"key":"p_40","first-page":"42","volume-title":"Formal Specification and Development in Z and B","author":"Smi","year":"2000"},{"key":"p_41","volume-title":": The Z Notation: A Reference Manual","author":"Spi","year":"1989"},{"key":"p_42","first-page":"283","volume-title":"Hinchey and Liu [HiL97]","author":"Ta"},{"key":"p_43","first-page":"437","volume-title":"Integrated Formal Methods","author":"Tr","year":"1999"},{"key":"p_44","volume-title":"Using Z: Specification, Refinement, and Proof","author":"Wo","year":"1996"},{"key":"p_45","first-page":"340","volume-title":"Formal Methods in Software Development, LNCS 428","author":"Wo","year":"1990"},{"key":"p_46","volume-title":"Object-Oriented Concurrent Programming","author":"Yo","year":"1987"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s001650200002.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s001650200002\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s001650200002","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:39:11Z","timestamp":1641483551000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s001650200002"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002,5]]},"references-count":45,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2002,5]]}},"alternative-id":["10.1007\/s001650200002"],"URL":"https:\/\/doi.org\/10.1007\/s001650200002","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2002,5]]}}}