This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Synchronizability of Conversations among Web Services
December 2005 (vol. 31 no. 12)
pp. 1042-1055
ASCII Text
x 
 
Xiang Fu, Tevfik Bultan, Jianwen Su, "Synchronizability of Conversations among Web Services," IEEE Transactions on Software Engineering, vol. 31, no. 12, pp. 1042-1055, December, 2005.
 
 
BibTex
x
 
@article{ 10.1109/TSE.2005.141,
author = {Xiang Fu and Tevfik Bultan and Jianwen Su},
title = {Synchronizability of Conversations among Web Services},
journal ={IEEE Transactions on Software Engineering},
volume = {31},
number = {12},
issn = {0098-5589},
year = {2005},
pages = {1042-1055},
doi = {http://doi.ieeecomputersociety.org/10.1109/TSE.2005.141},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
}
 
 
RefWorks Procite/RefMan/Endnote
x 
 
TY - JOUR
JO - IEEE Transactions on Software Engineering
TI - Synchronizability of Conversations among Web Services
IS - 12
SN - 0098-5589
SP1042
EP1055
EPD - 1042-1055
A1 - Xiang Fu,
A1 - Tevfik Bultan,
A1 - Jianwen Su,
PY - 2005
KW - Index Terms- Web services
KW - asynchronous communication
KW - conversations
KW - model checking
KW - verification
KW - synchronizability
KW - realizability.
VL - 31
JA - IEEE Transactions on Software Engineering
ER -
 
We present a framework for analyzing interactions among Web services that communicate with asynchronous messages. We model the interactions among the peers participating in a composite Web service as conversations, the global sequences of messages exchanged among the peers. This naturally leads to the following model checking problem: Given an LTL property and a composite Web service, do the conversations generated by the composite Web service satisfy the property? We show that asynchronous messaging leads to state space explosion for bounded message queues and undecidability of the model checking problem for unbounded message queues. We propose a technique called synchronizability analysis to tackle this problem. If a composite Web service is synchronizable, its conversation set remains the same when asynchronous communication is replaced with synchronous communication. We give a set of sufficient conditions that guarantee synchronizability and that can be checked statically. Based on our synchronizability results, we show that a large class of composite Web services with unbounded message queues can be verified completely using a finite state model checker such as SPIN. We also show that synchronizability analysis can be used to check the realizability of top-down conversation specifications and we contrast the conversation model with the Message Sequence Charts. We integrated synchronizability analysis to a tool we developed for analyzing composite Web services.

[1] M. Abadi, L. Lamport, and P. Wolper, “Realizable and Unrealizable Specifications of Reactive Systems,” Proc. 16th Int'l Colloquium Automata, Languages, and Programming, pp. 1-17, 1989.
[2] L.D. Alfaro and T.A. Henzinger, “Interface Automata,” Proc. Ninth Ann. Symp. Foundations of Software Eng., pp. 109-120, 2001.
[3] G. Alonso, F. Casati, H. Kuno, and V. Machiraju, Web Services Concepts, Architectures and Applications Series: Data-Centric Systems and Applications. Addison Wesley Professional, 2002.
[4] R. Alur, K. Etessami, and M. Yannakakis, “Inference of Message Sequence Charts,” Proc. 22nd Int'l Conf. Software Eng., pp. 304-313, 2000.
[5] R. Alur, K. Etessami, and M. Yannakakis, “Realizability and Verification of MSC Graphs,” Proc. 28th Int'l Colloquium Automata, Languages, and Programming, pp. 797-808, 2001.
[6] A. Bosworth, “Loosely Speaking,” XML & Web Services Magazine, vol. 3, no. 4, Apr. 2002.
[7] Business Process Execution Language for Web Services (BPEL), Version 1.1, http://www-128.ibm.com/developerworks/library/ specificationws-bpel. 2002
[8] D. Brand and P. Zafiropulo, “On Communicating Finite-State Machines,” J. ACM, vol. 30, no. 2, pp. 323-342, 1983.
[9] T. Bultan, X. Fu, R. Hull, and J. Su, “Conversation Specification: A New Approach to Design and Analysis of e-Service Composition,” Proc. 12th Int'l World Wide Web Conf., pp. 403-410, May 2003.
[10] M. Chiodo, P. Giusto, A. Jurecska, L. Lavagno, H. Hsieh, and A. Sangiovanni-Vincetelli, “A Formal Specification Model for Hardware/Software Codesign,” Proc. Int'l Workshop Hardware-Software Codesign, Oct. 1993.
[11] E.M. Clarke, O. Grumberg, and D.A. Peled, Model Checking. Cambridge, Mass.: MIT Press, 1999.
[12] World Wide Web Consortium, “Extensible Markup Language (XML),” http://www.w3c.orgXML. 1998.
[13] C. Ferris and J. Farrell, “What Are Web Services?” Comm. ACM, vol. 46, no. 6, pp. 31-31, June 2003.
[14] H. Foster, S. Uchitel, J. Magee, and J. Kramer, “Model-Based Verification of Web Service Compositions,” Proc. 18th IEEE Int'l Conf. Automated Software Eng. Conf., pp. 152-163, 2003.
[15] X. Fu, “Formal Specification and Verification of Asynchronously Communicating Web Services,” PhD thesis, Univ. of California, Santa Barbara, 2004.
[16] X. Fu, T. Bultan, and J. Su, “Analysis of Interacting Web Services,” Proc. 13th Int'l World Wide Web Conf., pp. 621-630, May 2004.
[17] X. Fu, T. Bultan, and J. Su, “Conversation Protocols: A Formalism for Specification and Analysis of Reactive Electronic Services,” Theoretical Computer Science, vol. 328, nos. 1-2, pp. 19-37, Nov. 2004.
[18] X. Fu, T. Bultan, and J. Su, “Model Checking XML Manipulating Software,” Proc. 2004 ACM/SIGSOFT Int'l Symp. Software Testing and Analysis, pp. 252-262, July 2004.
[19] X. Fu, T. Bultan, and J. Su, “Realizability of Conversation Protocols with Message Contents,” Proc. 2004 IEEE Int'l Conf. Web Services, pp. 96-103, July 2004.
[20] X. Fu, T. Bultan, and J. Su, “WSAT: A Tool for Formal analysis of Web Service Compositions,” Proc. 16th Int'l Conf. Computer-Aided Verification, pp. 510-514, July 2004.
[21] C.A.R. Hoare, “Communicating Sequential Processes,” Comm. ACM, vol. 21, no. 8, pp. 666-677, 1978.
[22] G.J. Holzmann, The SPIN Model Checker: Primer and Reference Manual. Boston: Addison-Wesley, 2003.
[23] IBM, Conversation Support Project, http://www.research.ibm. comconvsupport/, 2002
[24] Java Message Service, http://java.sun.com/productsjms/, 2002
[25] G. Kahn, “The Semantics of a Simple Language for Parallel Programming,” Proc. IFIP 74, pp. 471-475, 1974.
[26] S. Kleijnen and S. Raju, “An Open Web Services Architecture,” ACM Queue, vol. 1, no. 1, pp. 39-46, Mar. 2003.
[27] N. Lynch and M. Tuttle, “Hierarchical Correctness Proofs for Distributed Algorithms,” Proc. Sixth ACM Symp. Principles of Distributed Computing, pp. 137-151, 1987.
[28] G. Miller, “.Net vs. J2EE,” Comm. ACM, vol. 46, no. 6, pp. 64-67, June 2003.
[29] R. Milner, Communicating and Mobile Systems: The $\pi{\hbox{-}}Calculus$ . Cambridge Univ. Press, 1999.
[30] Message Sequence Chart (MSC), ITU-T, Geneva Recommendation Z.120, 1994.
[31] Microsoft Message Queuing Service, http://www.microsoft.com/windows2000/technologies/ communications/msmqde fault.mspx , 2003
[32] E. Newcomer, Understanding Web Services: XML, WSDL, SOAP, and UDDI. Springer, 2004.
[33] W. Peng, “Single-Link and Time Communicating Finite State Machines,” Proc. Second Int'l Conf. Network Protocols, pp. 126-133, 1994.
[34] A. Pnueli and R. Rosner, “On the Synthesis of a Reactive Module,” Proc. 16th ACM Symp. Principles of Programming Languages, pp. 179-190, 1989.
[35] A. Pnueli and R. Rosner, “On the Synthesis of an Asynchronous Reactive Module,” Proc. 16th Int'l Colloquium Automata, Languages, and Programs, pp. 652-671, 1989.
[36] S.K. Rajamani and J. Rehof, “A Behavioral Module System for the pi-Calculus,” Proc. Eighth Static Analysis Symp., pp. 375-394, July 2001.
[37] Simple Object Access Protocol (SOAP) 1.1, W3C Note 08, May 2000, http://www.w3.org/TRSOAP/.
[38] S. Uchitel, J. Kramer, and J. Magee, “Incremental Elaboration of Scenario-Based Specifications and Behavior Models Using Implied Scenarios,” ACM Trans. Software Eng. and Methodology, vol. 13, no. 1, pp. 37-85, 2004.
[39] Universal Description, Discovery and Integration (UDDI) Protocol, http:/www.uddi.org, 2002.
[40] J. Williams, “The Web Services Debate J2EE vs. .Net,” Comm. ACM, vol. 46, no. 6, pp. 59-63, June 2003.
[41] Web Service Choreography Description Language (WS-CDL), http://www.w3.org/TR/2004ws-cdl-10-20041217 , 2004.
[42] Web Services Description Language (WSDL) 1.1, http://www.w3.org/TRwsdl, Mar. 2001.
[43] XML Schema, http://www.w3c.org/XMLSchema.html, 2001.

Index Terms:
Index Terms- Web services, asynchronous communication, conversations, model checking, verification, synchronizability, realizability.
Citation:
Xiang Fu, Tevfik Bultan, Jianwen Su, "Synchronizability of Conversations among Web Services," IEEE Transactions on Software Engineering, vol. 31, no. 12, pp. 1042-1055, Dec. 2005, doi:10.1109/TSE.2005.141
Usage of this product signifies your acceptance of the Terms of Use.