{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:25:38Z","timestamp":1761611138427},"reference-count":22,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2004,11,1]],"date-time":"2004-11-01T00:00:00Z","timestamp":1099267200000},"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":[[2004,11]]},"abstract":"<jats:title>Abstract.<\/jats:title>\n          <jats:p>\n            This paper investigates the issue of responsiveness of interoperating components: one not causing the other to deadlock. This is obviously related to the question of whether the two deadlock when put in parallel. However, it is different in that we require that a specific process\n            <jats:italic>P<\/jats:italic>\n            is not itself blocked by a plugin\n            <jats:italic>Q<\/jats:italic>\n            when it could otherwise have progressed, instead of asking that either process can always proceed (deadlock freedom). The issue becomes yet more subtle when dealing with processes which can nondeterministically block, either through graceful termination or unfortunate deadlock. The relational predicate, that is, binary relation on processes, which we provide is refinement-closed. This is significant as it allows components to be developed independently. In addition, it can be mechanically verified. The contribution of this paper is to identify the issue of responsiveness; to define appropriate properties; to demonstrate the suitability of these properties and consider how they can be mechanically verified. The notation used is CSP with automatic model-checking provided by the FDR tool.\n          <\/jats:p>","DOI":"10.1007\/s00165-004-0050-9","type":"journal-article","created":{"date-parts":[[2004,10,16]],"date-time":"2004-10-16T07:48:54Z","timestamp":1097912934000},"page":"394-411","source":"Crossref","is-referenced-by-count":10,"title":["Responsiveness of interoperating components"],"prefix":"10.1145","volume":"16","author":[{"given":"J. N.","family":"Reed","sequence":"first","affiliation":[{"name":"Department of Information Technology, Armstrong Atlantic State University, Savannah, GA, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"J. E.","family":"Sinclair","sequence":"additional","affiliation":[{"name":"Department of Computer Science, University of Warwick, CV4 7AL, Coventry, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"A. W.","family":"Roscoe","sequence":"additional","affiliation":[{"name":"Oxford University Computing Laboratory, University of Oxford, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"p_1","volume-title":"The B-Book","author":"Abr J-R","year":"1996"},{"key":"p_2","volume-title":"Assume-guarantee based compositional reasoning for synchronous timing diagrams. Lect Notes Comput Sci 2031:465+","author":"Nina Amla E","year":"2001"},{"key":"p_3","volume-title":"Developing and integrating enterprise components and services. Commun ACM 45(10)","author":"Ars A","year":"2002"},{"key":"p_4","volume-title":"6th international workshop in formal methods Dublin","author":"Bolton C","year":"2003"},{"key":"p_5","doi-asserted-by":"crossref","first-page":"305","DOI":"10.1007\/978-3-642-82453-1_10","volume-title":"Apt KR (ed) Logics and models of concurrent systems, NATO ASI vol 13 Ser F","author":"Brookes SD","year":"1985"},{"key":"p_6","first-page":"490","volume-title":"Wing JM, Woodcock J, Davies J (eds) Proceedings of FM99: world congress on formal methods in the development of computing systems, vol 1","author":"But MJ","year":"1999"},{"key":"p_7","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1007\/s001650200025","article-title":"On the use of data refinement in the development of secure communications systems","volume":"14","author":"But M","year":"2002","journal-title":"Formal Aspects Comput Sci"},{"key":"p_8","volume-title":"Specification, implementation, and deployment of components. Commun ACM 45(10)","author":"Crnkovic I","year":"2002"},{"key":"p_9","volume-title":"Electronic notes in theoretical computer science, vol 70:3","author":"Cavalcanti A","year":"2002"},{"key":"p_10","volume-title":"A discipline of programming","author":"Dij EW","year":"1976"},{"key":"p_11","unstructured":"[For] Formal Systems (Europe) Ltd. Failures divergence refinement. User manual and tutorial. http:\/\/www.formal.demon.co.uk\/ fdr2manual\/index.html"},{"key":"p_12","volume-title":"Communicating sequential processes","author":"Hoa","year":"1985"},{"key":"p_13","unstructured":"[Int] Internet. MasterCraft integrated development framework for distributed applications. Tata Consultancy Services. http:\/\/www.tcs.com\/0 products\/mastercraft\/index.htm"},{"key":"p_14","volume-title":"A semantic study of data independence with applications to model checking. DPhil Thesis","author":"Laz RS","year":"1999"},{"key":"p_15","volume-title":"Gries D, Feijen WHJ, van Gasteren AGM, Misra J (eds) Beauty is our business: a birthday salute to Edsger W. Dijkstra","author":"Mor CC","year":"1990"},{"issue":"3","key":"p_16","doi-asserted-by":"crossref","first-page":"289","DOI":"10.1016\/0890-5401(87)90004-6","article-title":"The pursuit of deadlock freedom","volume":"75","author":"Roscoe AW","year":"1987","journal-title":"Inform Comput"},{"key":"p_17","volume-title":"The theory and practice of concurrency","author":"Ros AW","year":"1998"},{"key":"p_18","volume-title":"On the expressiveness of CSP refinement checking","author":"Ros AW","year":"2003"},{"key":"p_19","volume-title":"Combining action systems and CSP: Plug-in specifications view. Electronic Notes Theor Comput Sci 40","author":"Reed JN","year":"2001"},{"key":"p_20","first-page":"45","volume-title":"FASE","author":"Reed JN","year":"2001"},{"key":"p_21","first-page":"437","volume-title":"Araki K, Galloway A, Taguchi K (eds) Integated Formal Methods","author":"Treharne H","year":"1999"},{"key":"p_22","series-title":"Lecture Notes in Computer Science vol","doi-asserted-by":"crossref","first-page":"188","DOI":"10.1007\/3-540-44525-0_12","volume-title":"Bowen JP, Dunne S, Galloway A, King S (eds) In: Proceedings of ZB2000","author":"Treharne H","year":"2000"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-004-0050-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-004-0050-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-004-0050-9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:47:13Z","timestamp":1641484033000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-004-0050-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004,11]]},"references-count":22,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2004,11]]}},"alternative-id":["10.1007\/s00165-004-0050-9"],"URL":"https:\/\/doi.org\/10.1007\/s00165-004-0050-9","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2004,11]]}}}