{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,6]],"date-time":"2025-08-06T13:39:43Z","timestamp":1754487583367},"reference-count":37,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[1998,11,1]],"date-time":"1998-11-01T00:00:00Z","timestamp":909878400000},"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":[[1998,11]]},"abstract":"<jats:title>Abstract.<\/jats:title>\n          <jats:p>An important aspect in the specification of distributed systems is the \nrole of the internal (or unobservable) operation. Such operations are not part of the interface to the environment (i.e. the user cannot invoke them), however, they are essential to our understanding and correct modelling of the system. In this paper we are interested in the use of the formal specification notation Z for the description of distributed systems. Various conventions have been employed to model internal operations when specifying such systems in Z. If internal operations are distinguished in the specification notation, then refinement needs to deal with internal operations in appropriate ways.<\/jats:p>\n          <jats:p>Using an example of a telecommunications protocol we show that standard Z refinement is inappropriate for refining a system when internal operations are specified explicitly. We present a generalisation of Z refinement, called weak refinement, which treats internal operations differently from observable operations when refining a system. We discuss the role of internal operations in a Z specification, and in particular whether an equivalent specification not containing internal operations can be found. The nature of divergence through livelock is also discussed.<\/jats:p>","DOI":"10.1007\/s001650050007","type":"journal-article","created":{"date-parts":[[2002,8,25]],"date-time":"2002-08-25T07:30:30Z","timestamp":1030260630000},"page":"125-159","source":"Crossref","is-referenced-by-count":18,"title":["Specifying and Refining Internal Operations in Z"],"prefix":"10.1145","volume":"10","author":[{"given":"John","family":"Derrick","sequence":"first","affiliation":[{"name":"Computing Laboratory, University of Kent, Canterbury, UK, , , , , , GB"}]},{"given":"Eerke","family":"Boiten","sequence":"additional","affiliation":[{"name":"Computing Laboratory, University of Kent, Canterbury, UK, , , , , , GB"}]},{"given":"Howard","family":"Bowman","sequence":"additional","affiliation":[{"name":"Computing Laboratory, University of Kent, Canterbury, UK, , , , , , GB"}]},{"given":"Maarten","family":"Steen","sequence":"additional","affiliation":[{"name":"Computing Laboratory, University of Kent, Canterbury, UK, , , , , , GB"}]}],"member":"320","reference":[{"key":"p_1","volume-title":"CUP","author":"Abrial J. R.","year":"1996"},{"issue":"1","key":"p_2","doi-asserted-by":"crossref","first-page":"25","DOI":"10.1016\/0169-7552(87)90085-7","article-title":"Introduction to the ISO Specification Language LOTOS","volume":"14","author":"Bolognesi T.","year":"1988","journal-title":"Computer Networks and ISDN Systems"},{"key":"p_3","first-page":"644","volume-title":"Formal Methods Europe (FME '97), LNCS 1313","author":"Boiten E.","year":"1997"},{"key":"p_4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1007\/3-540-60973-3_93","volume-title":"M.-C","author":"Boiten E.","year":"1996"},{"key":"p_5","first-page":"221","volume-title":"Workshops in Computing","author":"Benjamin M.","year":"1989"},{"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":"Journ. ACM"},{"key":"p_7","first-page":"63","volume-title":"Protocol Specification, Testing and Verification, VIII","author":"Brinksma E.","year":"1988"},{"key":"p_8","first-page":"349","volume-title":"VI","author":"Brinksma E.","year":"1986"},{"key":"p_9","first-page":"223","volume-title":"An approach to the design of distributed systems with B AMN","author":"Butler M.","year":"1997"},{"key":"p_10","first-page":"113","volume-title":"Workshops in Computing","author":"Cusack E.","year":"1992"},{"key":"p_11","first-page":"167","volume-title":"Object oriented modelling in Z for Open Distributed Systems","author":"Cusack E.","year":"1991"},{"key":"p_12","first-page":"180","volume-title":"Seventh Annual Z User Workshop","author":"Cusack E.","year":"1992"},{"key":"p_13","first-page":"399","volume-title":"First IFIP International workshop on Formal Methods for Open Object-based Distributed Systems","author":"Derrick J.","year":"1996"},{"key":"p_14","first-page":"501","volume-title":"FORTE\/PSTV'96","author":"Derrick J.","year":"1996"},{"key":"p_15","first-page":"369","volume-title":"Weak refinement in Z","author":"Derrick J.","year":"1997"},{"issue":"3","key":"p_16","doi-asserted-by":"crossref","first-page":"83","DOI":"10.1016\/0304-3975(84)90113-0","article-title":"Testing equivalences for processes","volume":"34","author":"Nicola R.","year":"1984","journal-title":"Theoretical Computer Science"},{"key":"p_17","volume-title":"FMPPTA'97","author":"Evans A. S.","year":"1997"},{"key":"p_18","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_19","volume-title":"editors","author":"Finkelstein A.","year":"1996"},{"key":"p_20","volume-title":"Algebraic Theory of Processes","author":"Hennessy M.","year":"1988"},{"key":"p_21","first-page":"3","volume-title":"Protocol Specification Testing and Verification IX","author":"Hayes I.","year":"1989"},{"key":"p_22","volume-title":": Communicating Sequential Processes","author":"Hoare C. A. R.","year":"1985"},{"key":"p_23","volume-title":"Open Distributed Processing - Reference Model - Parts","year":"1995"},{"key":"p_24","volume-title":": Systematic Software Development using VDM","author":"Jones C. B.","year":"1989"},{"key":"p_25","volume-title":"ZUM'94","author":"Lamport L.","year":"1994"},{"key":"p_26","first-page":"242","volume-title":"Specifying reactive systems in B AMN","author":"Lano K.","year":"1997"},{"key":"p_28","volume-title":"Int. Conf. on Software Engineering. IEEE Computer Press","author":"Mahony B.","year":"1998"},{"key":"p_29","volume-title":"Communication and Concurrency","author":"Milner R.","year":"1989"},{"key":"p_30","first-page":"29","volume-title":"Eighth Annual Z User Workshop","author":"Mataga P.","year":"1994"},{"key":"p_31","volume-title":"BT","author":"Rafsanjani G. H. B.","year":"1994"},{"key":"p_32","first-page":"267","volume-title":"Modelling information objects in Z","author":"Rudkin S.","year":"1991"},{"issue":"3","key":"p_33","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_34","first-page":"62","volume-title":"Formal Methods Europe (FME '97), LNCS 1313","author":"Smith G.","year":"1997"},{"key":"p_35","volume-title":": The Z notation: A reference manual","author":"Spivey J. M.","year":"1989"},{"key":"p_36","first-page":"264","volume-title":"Ninth Annual Z User Workshop, LNCS 967","author":"Strulo B.","year":"1995"},{"key":"p_37","volume-title":"Using Z: Specification, Refinement, and Proof","author":"Woodcock J.","year":"1996"},{"key":"p_38","first-page":"108","volume-title":"Eighth Annual Z User Workshop","author":"Wezeman C.","year":"1994"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s001650050007.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s001650050007\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s001650050007","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:24:09Z","timestamp":1641482649000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s001650050007"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998,11]]},"references-count":37,"journal-issue":{"issue":"2","published-print":{"date-parts":[[1998,11]]}},"alternative-id":["10.1007\/s001650050007"],"URL":"https:\/\/doi.org\/10.1007\/s001650050007","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[1998,11]]}}}