{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,29]],"date-time":"2025-03-29T17:23:06Z","timestamp":1743268986097},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540405610"},{"type":"electronic","value":"9783540450894"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/3-540-45089-0_18","type":"book-chapter","created":{"date-parts":[[2007,10,27]],"date-time":"2007-10-27T03:27:35Z","timestamp":1193455655000},"page":"188-200","source":"Crossref","is-referenced-by-count":32,"title":["Conversation Protocols: A Formalism for Specification and Verification of Reactive Electronic Services"],"prefix":"10.1007","author":[{"given":"Xiang","family":"Fu","sequence":"first","affiliation":[]},{"given":"Tevfik","family":"Bultan","sequence":"additional","affiliation":[]},{"given":"Jianwen","family":"Su","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2003,6,24]]},"reference":[{"key":"18_CR1","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/BFb0035748","volume-title":"Proc. of 16th Int. Colloq. on Automata, Languages and Programming","author":"M. Abadi","year":"1989","unstructured":"M. Abadi, L. Lamport, and P. Wolper. Realizable and unrealizable specifications of reactive systems. In Proc. of 16th Int. Colloq. on Automata, Languages and Programming, volume 372 of LNCS, pages 1\u201317. Springer Verlag, 1989."},{"key":"18_CR2","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1006\/inco.1996.0053","volume":"127","author":"P.A. Abdulla","year":"1996","unstructured":"P.A. Abdulla and B. Jonsson. Verifying programs with unreliable channels. Journal of Information and Computation, 127:91\u2013101, 1996.","journal-title":"Journal of Information and Computation"},{"key":"18_CR3","doi-asserted-by":"crossref","unstructured":"L.D. Alfaro and T.A. Henzinger. Interface automata. In Proc. of 9th ACM Symp. on Foundations of Software Engineering, pages 109\u2013120, 2001.","DOI":"10.1145\/503209.503226"},{"key":"18_CR4","doi-asserted-by":"crossref","unstructured":"R. Alur, K. Etessami, and M. Yannakakis. Realizability and verification of MSC graphs. In Proc. 28th Int. Colloq. on Automata, Languages, and Programming, 2001.","DOI":"10.1007\/3-540-48224-5_65"},{"key":"18_CR5","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1006\/inco.1999.2847","volume":"160","author":"R. Alur","year":"2000","unstructured":"R. Alur, K. McMillan, and D. Peled. Model-checking of correctness conditions for concurrent objects. Information and Computation, 160:167\u2013188, 2000.","journal-title":"Information and Computation"},{"key":"18_CR6","unstructured":"Business process execution language for web services (BPEL4WS), version 1.1. available at http:\/\/www.ibm.com\/developerworks\/library\/ws-bpel ."},{"key":"18_CR7","unstructured":"Business process modeling language (BPML). http:\/\/www.bpmi.org ."},{"issue":"2","key":"18_CR8","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1145\/322374.322380","volume":"30","author":"D. Brand","year":"1983","unstructured":"D. Brand and P. Zafiropulo. On communicating finite-state machines. Journal of the ACM, 30(2):323\u2013342, 1983.","journal-title":"Journal of the ACM"},{"key":"18_CR9","doi-asserted-by":"crossref","unstructured":"T. Bultan, X. Fu, R. Hull, and J. Su. Conversation specification: A new approach to design and analysis of e-service composition. In Proc. of 12th Intl. World Wide Web Conf., May 2003.","DOI":"10.1145\/775152.775210"},{"key":"18_CR10","unstructured":"M. Chiodo, P. Giusto, A. Jurecska, L. Lavagno, H. Hsieh, and A. Sangiovanni-Vincentelli. A formal specification model for hardware\/software codesign. In Proc. of the Intl. Workshop on Hardware-Software Codesign, October 1993."},{"key":"18_CR11","volume-title":"Model Checking","author":"E. M. Clarke","year":"1999","unstructured":"E. M. Clarke, O. Grumberg, and D.A. Peled. Model Checking. The MIT Press, Cambridge, Massachusetts, 1999."},{"key":"18_CR12","doi-asserted-by":"crossref","unstructured":"E.A. Emerson. Temporal and modal logic. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science: Volume B: Formal Models and Semantics, pages 995\u20131072. Elsevier, 1990.","DOI":"10.1016\/B978-0-444-88074-1.50021-4"},{"issue":"1\u20132","key":"18_CR13","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1016\/S0304-3975(96)00026-6","volume":"174","author":"A. Finkel","year":"1997","unstructured":"A. Finkel and P. McKenzie. Verifying identical communicating processes is undecidable. Theoretical Computer Science, 174(1\u20132):217\u2013230, 1997.","journal-title":"Theoretical Computer Science"},{"key":"18_CR14","unstructured":"S. J. Garland and N. Lynch. Using I\/O automata for developing distributed systems. In Foundations of Component-Based Systems. Cambridge Univ. Press, 2000."},{"key":"18_CR15","series-title":"Lect Notes Comput Sci","volume-title":"Proc. of 12th European Symp. on Programming","author":"P. Graunke","year":"2003","unstructured":"P. Graunke, R.B. Findler, S. Krishnamurthi, and M. Felleisen. Modeling web interactions. In Proc. of 12th European Symp. on Programming, LNCS 2618, 2003."},{"key":"18_CR16","doi-asserted-by":"crossref","unstructured":"J.E. Hanson, P. Nandi, and S. Kumaran. Conversation support for business process integration. In Proc. of 6th IEEE Int. Enterprise Distributed Object Computing Conference, 2002.","DOI":"10.1109\/EDOC.2002.1137697"},{"issue":"8","key":"18_CR17","doi-asserted-by":"publisher","first-page":"666","DOI":"10.1145\/359576.359585","volume":"21","author":"C.A.R. Hoare","year":"1978","unstructured":"C.A.R. Hoare. Communicating sequential processes. Communications of the ACM, 21(8):666\u2013677, 1978.","journal-title":"Communications of the ACM"},{"key":"18_CR18","doi-asserted-by":"crossref","unstructured":"R. Hull, M. Benedikt, C. Christophides, and J. Su. E-services: A look behind the curtain. In Proc. of 22nd ACM Symp. on Principles of Database Systems, 2003.","DOI":"10.1145\/773153.773154"},{"key":"18_CR19","unstructured":"IBM. Conversation support project. http:\/\/www.research.ibm.com\/convsupport\/"},{"key":"18_CR20","unstructured":"G. Kahn. The semantics of a simple language for parallel programming. In Proc. of IFIP 74, pages 471\u2013475. North-Holland, 1974."},{"key":"18_CR21","doi-asserted-by":"crossref","unstructured":"H. Liu and R. E. Miller. Generalized fair reachability analysis for cyclic protocols. In IEEE\/ACM Transactions on Networking, pages 192\u2013204, 1996.","DOI":"10.1109\/90.490747"},{"key":"18_CR22","doi-asserted-by":"crossref","unstructured":"N. Lynch and M. Tuttle. Hierarchical correctness proofs for distributed algorithms. In Proc. 6th ACM Symp. Principles of Distributed Computing, pages 137\u2013151, 1987.","DOI":"10.1145\/41840.41852"},{"key":"18_CR23","unstructured":"R. Milner. Communicating and Mobile Systems: the \u03c0-Calculus. Cambridge University Press, 1999."},{"key":"18_CR24","doi-asserted-by":"crossref","unstructured":"A. Pnueli and R. Rosner. On the synthesis of a reactive module. In Proc. of 16th ACM Symp. Principles of Programming Languages, pages 179\u2013190, 1989.","DOI":"10.1145\/75277.75293"},{"key":"18_CR25","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"652","DOI":"10.1007\/BFb0035790","volume-title":"Proc. of 16th Int. Colloq. on Automata, Languages, and Programs","author":"A. Pnueli","year":"1989","unstructured":"A. Pnueli and R. Rosner. On the synthesis of an asynchronous reactive module. In Proc. of 16th Int. Colloq. on Automata, Languages, and Programs, volume 372 of LNCS, pages 652\u2013671, 1989."},{"key":"18_CR26","doi-asserted-by":"crossref","unstructured":"S.K. Rajamani and J. Rehof. A behavioral module system for the pi-calculus. In Proc. of Static Analysis Symposium (SAS), July 2001.","DOI":"10.1007\/3-540-47764-0_22"},{"key":"18_CR27","unstructured":"Sun. Java message service. http:\/\/java.sun.com\/products\/jms\/ ."},{"key":"18_CR28","unstructured":"W3C. Web service choreography interface (WSCI) version 1.0. available at http:\/\/www.w3.org\/2003\/01\/wscwg-charter ."},{"key":"18_CR29","unstructured":"W3C. Web services description language (WSDL) version 1.1. available at http:\/\/www.w3.org\/TR\/wsdl , 2001."}],"container-title":["Lecture Notes in Computer Science","Implementation and Application of Automata"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45089-0_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,3]],"date-time":"2019-05-03T22:08:18Z","timestamp":1556921298000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45089-0_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540405610","9783540450894"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/3-540-45089-0_18","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2003]]}}}