{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,9,13]],"date-time":"2023-09-13T16:52:20Z","timestamp":1694623940312},"reference-count":23,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[1997,3,1]],"date-time":"1997-03-01T00:00:00Z","timestamp":857174400000},"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":[[1997,3]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>This paper studies the correctness of distributed systems made up of replicated processes that communicate by message passing. Processes are described within the divergence model of CSP. The notion of correctness introduced is based on a relation that formally expresses the conformance of an implementation process with the target process it is intended to implement. A weak and a strong version of the relation are introduced, aimed at treating acyclic and cyclic process networks respectively. Both allow the study of (total) correctness and may cope with non-deterministic targets and implementations.<\/jats:p>\n          <jats:p>We then show how a target process may be implemented (in the formal sense introduced) by replicating it in a set of copies, a majority of which is non-faulty.<\/jats:p>","DOI":"10.1007\/bf01211616","type":"journal-article","created":{"date-parts":[[2005,2,25]],"date-time":"2005-02-25T13:02:19Z","timestamp":1109336539000},"page":"119-148","source":"Crossref","is-referenced-by-count":5,"title":["Two implementation relations and the correctness of communicating replicated processes"],"prefix":"10.1145","volume":"9","author":[{"given":"Maciej","family":"Koutny","sequence":"first","affiliation":[{"name":"Department of Computer Science, The University of Newcastle upon Tyne, NE1 7RU, Newcastle upon Tyne, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Luigi V.","family":"Mancini","sequence":"additional","affiliation":[{"name":"DISI, Universit\u00e0 \u201cLa Sapienza\u201d di Roma, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Giuseppe","family":"Pappalardo","sequence":"additional","affiliation":[{"name":"DIMET, Universit\u00e0 di Reggio Calabria, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","unstructured":"Aizikowitz J.: Designing Distributed Services Using Refinement Mappings PhD thesis Computer Science Dept Cornell University 1989."},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(91)90224-P"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"publisher","DOI":"10.1145\/828.833"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"crossref","unstructured":"Birman K. P.: Replication and fault-tolerance in the ISIS system Proc. 10th ACM Symp. on Operating Systems Principles pp. 79\u201386 1985.","DOI":"10.1145\/323627.323636"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"crossref","unstructured":"E. Brinksma B. Jonsson and F Orava. Refining interfaces of communicating systems. In Proc. Coll. on Combining Paradigms for Software Development LNCS 494 Springer-Verlag 1991.","DOI":"10.1007\/3540539816_73"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"crossref","unstructured":"Brookes S. D. and Roscoe A. W.: An improved failures model for communicating processes Seminar on Concurrency Brookes S. D. et al. (eds) LNCS 197 Springer-Verlag pp. 281\u2013305 1985.","DOI":"10.1007\/3-540-15670-4_14"},{"key":"e_1_2_1_2_7_2","unstructured":"Cristian F. Aghili H. Strong R. and Dolev D.: Atomic Broadcast: From Simple Message Diffusion to Byzantine Agreement Digest of FTCS-15 1985."},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"crossref","unstructured":"Cooper E.: Replicated distributed programs Proc. 10th ACM Symp. on Operating Systems Principles pp. 63\u201378 1985.","DOI":"10.1145\/323627.323635"},{"issue":"2","key":"e_1_2_1_2_9_2","doi-asserted-by":"crossref","first-page":"458","DOI":"10.1145\/201019.201032","article-title":"Three logics for branching bisimulation","volume":"42","author":"De Nicola R.","year":"1985","journal-title":"J. ACM."},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"crossref","unstructured":"Hoare C. A. R.: Communicating Sequential Processes . Prentice Hall 1985.","DOI":"10.1007\/978-3-642-82921-5_4"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"publisher","DOI":"10.1145\/174662.174665"},{"key":"e_1_2_1_2_12_2","unstructured":"Koutny M. and Mancini L. V. and Pappalardo G.: Replication in acyclic networks of communicating processes Technical Report 378 Computing Laboratory The University of Newcastle upon Tyne 1992."},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"crossref","unstructured":"Koutny M. and Mancini L. V. and Pappalardo G.: Modelling replicated processing Proc. PARLE 93 Bode A. et al. (eds) LNCS 694 Springer-Verlag 1993.","DOI":"10.1007\/3-540-56891-3_56"},{"key":"e_1_2_1_2_14_2","first-page":"95","article-title":"The implementation of reliable distributed multiprocess systems","volume":"2","author":"Lamport L.","year":"1978","journal-title":"Computer Networks"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"publisher","DOI":"10.1145\/5383.5384"},{"key":"e_1_2_1_2_16_2","unstructured":"Little M. and Shrivastava S. K.: Replicated K-resilient objects in Arjuna Proc. IEEE Intl. Workshop on the Management of Replicated Data 1990."},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"crossref","unstructured":"Lynch N. A. and Tuttle M. R.: Hierarchical correctness proofs for distributed algorithms Proc. 6th ACM PODC pp. 137\u2013151 1987.","DOI":"10.1145\/41840.41852"},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1986.6312922"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"crossref","unstructured":"Mancini L. V. and Pappalardo G.: Towards a theory of replicated processing. Formal Techniques in Real-Time and Fault-Tolerant Systems Joseph M. (ed) LNCS 331 Springer-Verlag pp. 175\u2013192 1988.","DOI":"10.1007\/3-540-50302-1_13"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"crossref","unstructured":"Schepers H. and Hooman J.: Trace-based compositional reasoning about fault-tolerant systems Proc. PARLE 93 LNCS 694 Springer-Verlag 1993.","DOI":"10.1007\/3-540-56891-3_16"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"crossref","first-page":"145","DOI":"10.1145\/190.357399","article-title":"Byzantine generals in action: Implementing fail-stop processors","volume":"2","author":"Schneider F. B.","year":"1984","journal-title":"ACM TOCS"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"publisher","DOI":"10.1145\/98163.98167"},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(86)90007-1"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01211616.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF01211616\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/BF01211616","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:22:58Z","timestamp":1641482578000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/BF01211616"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997,3]]},"references-count":23,"journal-issue":{"issue":"2","published-print":{"date-parts":[[1997,3]]}},"alternative-id":["10.1007\/BF01211616"],"URL":"https:\/\/doi.org\/10.1007\/bf01211616","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[1997,3]]}}}