乐胖代购免代理版

{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,9,13]],"date-time":"2023-09-13T16:36:41Z","timestamp":1694623001808},"reference-count":45,"publisher":"Association for Computing Machinery (ACM)","issue":"2-3","license":[{"start":{"date-parts":[[2003,11,1]],"date-time":"2003-11-01T00:00:00Z","timestamp":1067644800000},"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,11]]},"abstract":"Abstract<\/jats:title>\n Refinement in a concurrent context, as typified by a process algebra, takes a number of different forms depending on what is considered observable. Observations record, for example, which events a system is prepared to accept or refuse. Concurrent refinement relations include trace refinement, failures\u2013divergences refinement, readiness refinement and bisimulation. Refinement in a state-based language such as Z, on the other hand, is defined using a relational model in terms of the input\u2013output behaviour of abstract programs. These refinements are normally verified by using two simulation rules which help make the verification tractable. This paper unifies these two standpoints by generalising the standard relational model to include additional observable aspects. These are chosen in such a way that they represent exactly the notions of observation embedded in the various concurrent refinement relations. As a consequence, simulation rules for the tractable verification of concurrent refinement can be derived. We develop such simulation rules for failures\u2013divergences refinement and readiness refinement in particular, using an alternative relational model in the latter case.<\/jats:p>","DOI":"10.1007\/s00165-003-0007-4","type":"journal-article","created":{"date-parts":[[2004,3,19]],"date-time":"2004-03-19T02:31:00Z","timestamp":1079663460000},"page":"182-214","source":"Crossref","is-referenced-by-count":41,"title":["Relational Concurrent Refinement"],"prefix":"10.1145","volume":"15","author":[{"given":"John","family":"Derrick","sequence":"first","affiliation":[{"name":"Computing Laboratory, University of Kent, CT2 7NF, Canterbury, UK"}]},{"given":"Eerke","family":"Boiten","sequence":"additional","affiliation":[{"name":"Computing Laboratory, University of Kent, CT2 7NF, Canterbury, UK"}]}],"member":"320","reference":[{"key":"p_1","volume-title":"editors","author":"Araki K.","year":"1999"},{"key":"p_2","first-page":"82","volume-title":"7th International Seminar on Relational Methods in Computer Science (RelMiCS 7)","author":"Boiten E. A.","year":"2003"},{"key":"p_3","first-page":"70","article-title":"Unifying concurrent and relational refinement. In: Derrick, J., Boiten, E. A., von Wright, J. and Woodcock, J. C. P., editors, Proceedings REFINE'02","author":"Boiten E. A.","year":"2002","journal-title":"ENTCS"},{"issue":"1","key":"p_4","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_5","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_6","volume-title":"Formal Aspects of Computing","author":"Bolton C.","year":"2003"},{"key":"p_7","first-page":"273","volume-title":"Araki et al. [AGT99]","author":"Bolton C."},{"key":"p_8","first-page":"349","volume-title":"B. Sarikaya and G. v","author":"Brinksma E.","year":"1986"},{"issue":"3","key":"p_9","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_10","volume-title":"Pittsburgh Symposium on Concurrency","volume":"197","author":"Brookes S. D.","year":"1985"},{"key":"p_11","volume-title":"CUP","author":"de Roever W. -P.","year":"1998"},{"key":"p_12","doi-asserted-by":"crossref","volume-title":"Refinement in Z and Object-Z","author":"Derrick J.","year":"2001","DOI":"10.1007\/978-1-4471-0257-1"},{"key":"p_13","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: Bowen J. P. Hinchey M. G. and Till D. 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_14","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":"Formal Aspects of Computing"},{"key":"p_15","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_16","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_17","doi-asserted-by":"crossref","unstructured":"[Fis98] \n Fischer C.\n : \n How to combine Z with a process algebra\n . In: Bowen J. P. Fett A. and Hinchey M. G. 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_19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"469","DOI":"10.1007\/3-540-45499-3_33","volume-title":"Algebraic Methodology and Software Technology","author":"Fischer C.","year":"2000"},{"key":"p_20","first-page":"272","volume-title":"Hinchey and Liu [HiS97]","author":"Galloway A."},{"key":"p_21","volume-title":"Data Refinement in a Categorical Setting, Technical Monograph, number PRG-90","author":"Hoare C. A. R","year":"1990"},{"key":"p_22","doi-asserted-by":"crossref","unstructured":"[HHS86] \n He Jifeng Hoare C. A. R.\n and \n Sanders J. W\n .: '\n 86 volume \n 213\n of \n Lecture Notes in Computer Science pages \n 187\n -\n 196\n . \n Springer-Verlag 1986\n .","DOI":"10.1007\/3-540-16442-1_14"},{"key":"p_23","volume-title":"Hiroshima","author":"Hinchey M. G.","year":"1997"},{"key":"p_24","volume-title":": Communicating Sequential Processes","author":"Hoare C. A. R.","year":"1985"},{"key":"p_25","volume-title":"The Theory and Practice of Refinement. Butterworths","author":"He Jifeng","year":"1989"},{"key":"p_26","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"},{"issue":"6","key":"p_28","doi-asserted-by":"crossref","first-page":"1811","DOI":"10.1145\/197320.197383","article-title":"A behavioural notion of subtyping","volume":"16","author":"Liskov B.","year":"1994","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"p_29","volume-title":"20th International Conference on Software Engineering (ICSE'98)","author":"Mahony B. P.","year":"1998"},{"key":"p_30","doi-asserted-by":"crossref","unstructured":"[MBD00] \n Miarka R. Boiten E. A. and \n Derrick J\n .: \n Guards preconditions and refinement in Z\n . In: Bowen J. P. Dunne S. Galloway A. and King S. editors ZB\n 2000\n : Formal Specification and Development in Z and B volume \n 1878\n of \n Lecture Notes in Computer Science pages \n 286\n -\n 303\n . \n Springer-Verlag September 2000.","DOI":"10.1007\/3-540-44525-0_17"},{"key":"p_31","volume-title":"Communication and Concurrency","author":"Milner R.","year":"1989"},{"key":"p_32","doi-asserted-by":"crossref","first-page":"9","DOI":"10.1007\/BF00268075","article-title":": Specification-oriented semantics for communicating processes","volume":"23","author":"Olderog E.-R.","year":"1986","journal-title":"Acta Informatica"},{"issue":"2","key":"p_33","article-title":"An alternative order for the failures model","volume":"3","author":"Roscoe A. W.","year":"1993","journal-title":"Journal of Logic and Computation"},{"key":"p_34","series-title":"International Series in Computer Science","volume-title":": The Theory and Practice of Concurrency","author":"Roscoe A. W.","year":"1998"},{"key":"p_35","unstructured":"[Sch02] Schneider S.: 2002. Personal communication."},{"key":"p_36","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: Fitzgerald J. Jones C. B. and Lucas P. 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_37","doi-asserted-by":"crossref","volume-title":"The Object-Z Specification Language","author":"Smith G.","year":"2000","DOI":"10.1007\/978-1-4615-5265-9"},{"key":"p_38","first-page":"293","volume-title":"Hinchey and Liu [HiS97]","author":"Smith G."},{"key":"p_39","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_40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"108","DOI":"10.1007\/3-540-36103-0_14","volume-title":"Formal Methods and Software Engineering","author":"Smith G.","year":"2002"},{"key":"p_41","volume-title":": The Z Notation: A Reference Manual","author":"Spivey J. M.","year":"1992","edition":"2"},{"key":"p_42","first-page":"29","volume-title":"International Conference on Integrated Formal Methods (IFM'99)","author":"S\u00fchl C.","year":"1999"},{"key":"p_43","first-page":"437","volume-title":"Araki et al. [AGT99]","author":"Treharne H."},{"key":"p_44","doi-asserted-by":"crossref","unstructured":"[van90] \n van Glabbeek R. J.\n : The linear time : branching time spectrum\n . In: Baeten J. C. M. and Klop J. W. editors CONCUR 90 volume \n 458\n of \n Lecture Notes in Computer Science pages \n 278\n -\n 297\n . \n Springer-Verlag 1990\n .","DOI":"10.1007\/BFb0039066"},{"key":"p_45","first-page":"213","volume-title":"Formal Methods for Open Object-Based Distributed Systems (FMOODS 2000","author":"Wehrheim H.","year":"2000"},{"key":"p_46","volume-title":"Using Z: Specification, Refinement, and Proof","author":"Woodcock J. C. P.","year":"1996"},{"key":"p_47","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-0007-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-003-0007-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-003-0007-4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:38:30Z","timestamp":1641483510000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-003-0007-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,11]]},"references-count":45,"journal-issue":{"issue":"2-3","published-print":{"date-parts":[[2003,11]]}},"alternative-id":["10.1007\/s00165-003-0007-4"],"URL":"https:\/\/doi.org\/10.1007\/s00165-003-0007-4","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2003,11]]}}}