{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:44:51Z","timestamp":1780994691276,"version":"3.54.1"},"reference-count":59,"publisher":"Association for Computing Machinery (ACM)","issue":"5","license":[{"start":{"date-parts":[[2016,9,1]],"date-time":"2016-09-01T00:00:00Z","timestamp":1472688000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2016,9]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>\n            Asynchronous communication is often viewed as a single entity, the counterpart of synchronous communication. Although the basic concept of asynchronous communication is the decoupling of send and receive events, there is actually room for a variety of additional specification of the communication, for instance in terms of ordering. Yet, these different asynchronous communications are used interchangeably and seldom distinguished. This paper is a contribution to the study of these models, their differences, and how they are related. In this paper, the variety of point-to-point asynchronous communication paradigms is considered with two approaches. In the first and theoretical one, communication models are specified as properties on the ordering of events in distributed executions. In the second and more practical approach that involves composition of peers, they are modeled with transition systems and message histories as part of a framework. The described framework enables to model peer composition and compatibility properties. Besides, an implemented tool chain based on the TLA\n            <jats:sup>+<\/jats:sup>\n            formalism and model checking is also proposed and illustrated. The conformance of the two approaches is highlighted. A hierarchy is established between the studied communication models. From the execution viewpoint, it completes existing work in the area by introducing more asynchronous communication models and showing their differences. The framework is shown to offer abstract implementations of the communication models. Both the correctness and the completeness of the descriptions in the framework are studied. This reveals necessary restrictions on the behavior of the peers so that the communication models are actually implementable.\n          <\/jats:p>","DOI":"10.1007\/s00165-016-0379-x","type":"journal-article","created":{"date-parts":[[2016,5,3]],"date-time":"2016-05-03T13:24:48Z","timestamp":1462281888000},"page":"847-879","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":19,"title":["On the diversity of asynchronous communication"],"prefix":"10.1145","volume":"28","author":[{"given":"Florent","family":"Chevrou","sequence":"first","affiliation":[{"name":"IRIT\u2013Universit\u00e9 de Toulouse, 2 rue Camichel, 31000, Toulouse, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Aur\u00e9lie","family":"Hurault","sequence":"additional","affiliation":[{"name":"IRIT\u2013Universit\u00e9 de Toulouse, 2 rue Camichel, 31000, Toulouse, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Philippe","family":"Qu\u00e9innec","sequence":"additional","affiliation":[{"name":"IRIT\u2013Universit\u00e9 de Toulouse, 2 rue Camichel, 31000, Toulouse, France"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"crossref","unstructured":"Ait-Bachir A Dumas M Fauvet MC (2008) BESERIAL: behavioural service analyser. In: Business process management international conference. Demo session. LNCS 5240 pp 374\u2013377","DOI":"10.1007\/978-3-540-85758-7_27"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90185-I"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"crossref","unstructured":"Basu S Bultan T Ouederni M (2012) Synchronizability for verification of asynchronously communicating systems. In: 13th international conference on verification model checking and abstract interpretation VMCAI\u201912. Springer-Verlag pp 56\u201371","DOI":"10.1007\/978-3-642-27940-9_5"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2004.05.007"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"crossref","unstructured":"Benatallah B Casati F Toumani F (2004) Analysis and management of web service protocols. In: Conceptual modeling\u2013ER 2004 Lecture Notes in Computer Science vol 3288. Springer pp 524\u2013541","DOI":"10.1007\/978-3-540-30464-7_40"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"crossref","unstructured":"Birman KP (1996) Building secure and reliable network applications. Manning","DOI":"10.1007\/3-540-63343-X_35"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"publisher","DOI":"10.1145\/7351.7478"},{"key":"e_1_2_1_2_8_2","unstructured":"Babao\u011flu \u00d6 Marzullo K (1993) Consistent global states of distributed systems: fundamental concepts and mechanisms. In: Mullender SJ (ed) Distributed systems 2nd edn. ACM Press Frontier Series pp 55\u201396"},{"key":"e_1_2_1_2_9_2","unstructured":"Boudol G (1992) Asynchrony and the Pi-calculus. Research Report RR-1702 INRIA"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"crossref","unstructured":"Beauxis R Palamidessi C Valencia FD (2008) On the asynchronous nature of the asynchronous \u03c0-calculus. In: De Nicola R Degano P Meseguer J (eds) Concurrency graphs and models Lecture notes in computer science. Springer pp 473\u2013492","DOI":"10.1007\/978-3-540-68679-8_29"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"publisher","DOI":"10.1145\/322374.322380"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"publisher","DOI":"10.1007\/s004460050018"},{"key":"e_1_2_1_2_13_2","unstructured":"Coulouris G Dollimore J Kindberg T. (1994) Distributed systems: concepts and design 2nd edn. Addison Wesley"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"publisher","DOI":"10.1109\/71.774912"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"crossref","unstructured":"Cardelli L Gordon AD (1998) Mobile ambients. In: First international conference on foundations of software science and computation structure FoSSaCS \u201998. Springer-Verlag pp 140\u2013155","DOI":"10.1007\/BFb0053547"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"crossref","unstructured":"Charpentier M (1997) A U nity mapping operator for distributed programs. In: Fitzgerald J Jones CB Lucas P (eds) 4th Int\u2019l symposium of formal methods europe (FME\u201997) Lecture notes in computer science vol 1313. Springer-Verlag pp 665\u2013684","DOI":"10.1007\/3-540-63533-5_35"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"crossref","unstructured":"Chevrou F Hurault A Mauran P Qu\u00e9innec P (2016) Mechanized refinement of communication models with TLA+. In: International ABZ Conference. Springer-Verlag p 6","DOI":"10.1007\/978-3-319-33600-8_27"},{"key":"e_1_2_1_2_18_2","unstructured":"Chevrou F Hurault A Qu\u00e9innec P (2015) Automated verification of asynchronous communicating systems with TLA+. In: Electronic communications of the EASST (PostProceedings of the 15th international workshop on automated verification of critical systems) vol 72"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"publisher","DOI":"10.1145\/214451.214456"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"publisher","DOI":"10.1142\/S0218194008003647"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"publisher","DOI":"10.1145\/151646.151648"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0167-6423(01)00002-8"},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2011.03.009"},{"key":"e_1_2_1_2_24_2","doi-asserted-by":"publisher","DOI":"10.1145\/1041680.1041682"},{"key":"e_1_2_1_2_25_2","doi-asserted-by":"crossref","unstructured":"Deng S Wu Z Zhou M Li Y Wu J (2006) Modeling service compatibility with pi-calculus for choreography. In: 25th International conference on conceptual modeling Conceptual Modeling-ER 2006. Springer-Verlag pp 26\u201339","DOI":"10.1007\/11901181_4"},{"key":"e_1_2_1_2_26_2","doi-asserted-by":"crossref","unstructured":"Fournet C Gonthier G (1996) The reflexive cham and the join-calculus. In: 23rd ACM symposium on principles of programming languages POPL \u201996. ACM pp 372\u2013385","DOI":"10.1145\/237721.237805"},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"crossref","unstructured":"Fournet C Gonthier G L\u00e9vy J-J Maranget L R\u00e9my D. (1996) A calculus of mobile agents. In: Montanari U Sassone V (eds) CONCUR Lecture Notes in Computer Science vol 1119 pp 406\u2013421","DOI":"10.1007\/3-540-61604-7_67"},{"key":"e_1_2_1_2_28_2","doi-asserted-by":"crossref","unstructured":"Filli\u00e2tre J-C (2013) One logic to use them all. In: 24th international conference on automated deduction (CADE-24) Lecture Notes in Artificial Intelligence vol 7898 Lake Placid. Springer pp 1\u201320","DOI":"10.1007\/978-3-642-38574-2_1"},{"key":"e_1_2_1_2_29_2","doi-asserted-by":"crossref","unstructured":"Foster H Uchitel S Magee J Kramer J (2004) Compatibility verification for web service choreography. In: IEEE international conference on web services pp 738","DOI":"10.1109\/ICWS.2004.1314806"},{"key":"e_1_2_1_2_30_2","unstructured":"Gardiner P Goldsmith M Hulance J Jackson D Roscoe B Scattergood B Armstrong P (2010) FDR2 user manual. Technical report Oxford University"},{"key":"e_1_2_1_2_31_2","doi-asserted-by":"crossref","unstructured":"Garavel H Lang F Mateescu R Serwe W (2013) CADP 2011: a toolbox for the construction and analysis of distributed processes. Int J Softw Tools Technol Transf 15(2):89\u2013107","DOI":"10.1007\/s10009-012-0244-z"},{"key":"e_1_2_1_2_32_2","unstructured":"Holzmann GJ (2004) The spin model checker: primer and reference manual. Addison-Wesley"},{"key":"e_1_2_1_2_33_2","doi-asserted-by":"crossref","unstructured":"Honda K Tokoro M (1991) An object calculus for asynchronous communication. In: Proceedings of the European conference on object-oriented programming ECOOP \u201991. Springer-Verlag pp 133\u2013147","DOI":"10.1007\/BFb0057019"},{"key":"e_1_2_1_2_34_2","doi-asserted-by":"publisher","DOI":"10.1007\/s004460050044"},{"key":"e_1_2_1_2_35_2","unstructured":"Kshemkalyani AD Singhal M (2011) Distributed computing: principles algorithms and systems. Cambridge University Press"},{"key":"e_1_2_1_2_36_2","doi-asserted-by":"publisher","DOI":"10.1145\/359545.359563"},{"key":"e_1_2_1_2_37_2","unstructured":"Lamport L(2002) Specifying systems. Addison Wesley"},{"key":"e_1_2_1_2_38_2","doi-asserted-by":"crossref","unstructured":"Lamport L(2009) The PlusCal algorithm language. In: Leucker M Morgan C (eds) Theoretical aspects of computing Lecture notes in computer science vol 5684. Springer pp 36\u201360","DOI":"10.1007\/978-3-642-03466-4_2"},{"key":"e_1_2_1_2_39_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSMCA.2010.2093884"},{"key":"e_1_2_1_2_40_2","doi-asserted-by":"crossref","unstructured":"Lohmann N Wolf K (2011) Decidability results for choreography realization. In: 9th International conference on service-oriented computing ICSOC\u201911. Springer-Verlag pp 92\u2013107","DOI":"10.1007\/978-3-642-25535-9_7"},{"key":"e_1_2_1_2_41_2","unstructured":"Lynch NA (1996) Distributed algorithms. Morgan Kaufmann Publishers Inc."},{"key":"e_1_2_1_2_42_2","unstructured":"Martens A (2003) On compatibility of web services. Petri Net Newsletter pp 12\u201320"},{"key":"e_1_2_1_2_43_2","unstructured":"Mattern F (1989) Virtual time and global state in distributed systems. In: Cosnard M Robert Y Quinton P Raynal M (eds) Int\u2019l workshop on parallel and distributed algorithms. Elsevier Science Publishers pp 215\u2013226"},{"key":"e_1_2_1_2_44_2","doi-asserted-by":"publisher","DOI":"10.1109\/2.161279"},{"key":"e_1_2_1_2_45_2","unstructured":"Milner R (1982) A calculus of communicating systems. Springer-Verlag New York Inc."},{"key":"e_1_2_1_2_46_2","volume-title":"Communicating and mobile systems: the \u03c0-calculus","author":"Milner R","year":"1999"},{"key":"e_1_2_1_2_47_2","doi-asserted-by":"crossref","unstructured":"Misra J (1983) Detecting termination of distributed computations using markers. In: Proceedings of the second annual ACM symposium on principles of distributed computing PODC \u201983. ACM pp 290\u2013294","DOI":"10.1145\/800221.806729"},{"key":"e_1_2_1_2_48_2","doi-asserted-by":"crossref","unstructured":"Manna Z Pnueli A (1992) The temporal logic of reactive and concurrent systems\u2013specification. Springer-Verlag","DOI":"10.1007\/978-1-4612-0931-7"},{"key":"e_1_2_1_2_49_2","doi-asserted-by":"crossref","unstructured":"Ouederni M Sala\u00fcn G Bultan T (2013) Compatibility checking for asynchronously communicating software. In: International symposium on formal aspects of component software (FACS 2013) LNCS vol 8348 pp 310\u2013328","DOI":"10.1007\/978-3-319-07602-7_19"},{"key":"e_1_2_1_2_50_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129503004043"},{"key":"e_1_2_1_2_51_2","doi-asserted-by":"publisher","DOI":"10.1145\/65000.65001"},{"key":"e_1_2_1_2_52_2","doi-asserted-by":"publisher","DOI":"10.1006\/jpdc.1996.1300"},{"key":"e_1_2_1_2_53_2","doi-asserted-by":"crossref","unstructured":"Raynal M (2010) Communication and agreement abstractions for fault-tolerant asynchronous distributed systems. Synthesis Lectures on Distributed Computing Theory. Morgan and Claypool Publishers","DOI":"10.2200\/S00236ED1V01Y201004DCT002"},{"key":"e_1_2_1_2_54_2","doi-asserted-by":"crossref","unstructured":"Raynal M (2013) Distributed algorithms for message-passing systems. Springer","DOI":"10.1007\/978-3-642-38123-2"},{"key":"e_1_2_1_2_55_2","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(91)90008-6"},{"key":"e_1_2_1_2_56_2","unstructured":"Sighireanu M Chaudet C Garavel H Herbert M Mateescu R Vivien B (2000) LOTOS NT user manual"},{"key":"e_1_2_1_2_57_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF02277859"},{"key":"e_1_2_1_2_58_2","doi-asserted-by":"crossref","unstructured":"Tel G (2000) Introduction to distributed algorithms 2nd edn. Cambridge University Press","DOI":"10.1017\/CBO9781139168724"},{"key":"e_1_2_1_2_59_2","doi-asserted-by":"publisher","DOI":"10.1109\/TASE.2008.916747"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-016-0379-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-016-0379-x\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-016-0379-x","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T16:16:35Z","timestamp":1641485795000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-016-0379-x"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,9]]},"references-count":59,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2016,9]]}},"alternative-id":["10.1007\/s00165-016-0379-x"],"URL":"https:\/\/doi.org\/10.1007\/s00165-016-0379-x","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,9]]}}}