Algorithms for checking channel passing in web service choreography

Abstract

Web service choreography describes global models of service interactions among a set of participants. For an interaction to be executed, the participants must know the required channel(s) used in the interaction, otherwise the execution will get stuck. Since channels are composed dynamically, the initial channel set of each participant is often insufficient to meet the requirements. It is the responsibility of the participants to pass required channels owned (known) by one to others. Since service choreography may involve many participants and complex channel constraints, it is hard for designers to specify channel passing in a choreography exactly as required. We address the problem of checking whether a service choreography lacks channels or has redundant channels, and how to automatically generate channel passing based on interaction flows of the service choreography in the case of channel absence. Concretely, we propose a simple language Chorc, a channel interaction sub-language for modeling the channel passing aspect of service choreography. Based on the formal operational semantics of Chorc, the algorithms for static checking of service choreography and generating channel passing are also studied, and the complexity results of algorithms are discussed. Moreover, some illustrated service choreography examples are presented to show how to formalize and analyze service choreography with channel passing in Chorc.

Keywords

web service choreography / channel passing / algorithms

References

[1] Zaha J M, Dumas M, Hofstede T A, Barros A, Decker G. Service interaction modeling: Bridging global and local views. In: Proceedings of the 10th IEEE International Conference on Enterprise Distributed Object Computing. 2006, 45−55

[2] . Web Services Choreography Description Language, version 1.0, 2005. http://www.w3.org/TR/2005/CR-ws-cdl-10-20051109/

[3] Carbone M, Honda K, Yoshida N. Structured communication-centred programming for web services. In: Proceedings of the 16th European Conference on Programming. 2007, 2−17

[4] Thatte S. XLANG web services for business process design. 2001

[5] Leymann F. Web services flow language (WSFL 1.0). May 2001, http://www.ibm.com/software/solutions/webservices/pdf/WSFL.pdf

[6] . Business Process Execution Language for Web Services (BPEL4WS), version 1.1. May 2003, http://www.ibm.com/developerworks/webservices/library/ws-bpel/

[7] . Arkin A. Business process modeling language. November 2002, http://www.bpmi.org

[8] Yang H, Cai C, Peng L, Zhao X, Qiu Z. Reasoning about channel passing in choreography. In: Proceedings of the 2nd IEEE Interna tional Symposium on Theoretical Aspects of Software Engineering. 2008, 135−142

[9] Kavantzas N. A post at petri-pi mailing list, August 2005

[10] Carbone M, Honda K, Yoshida N, Milner R, Brown G, . Ross-Talbot S. A theoretical basis of communication-centred concurrent programming. Technical report, W3C, 2006. http://www.w3.org/2002/ws/chor/edcopies/theory/note.pdf

[11] Holzmann G J. The SPIN model checker: primer and reference manual. Addison-Wesley, 2003

[12] Barros A P, Dumas M, Hofstede t A HM. Service interaction patterns. In: Proceedings of the 3rd International Conference on Business Process Management. 2005, 302−318

[13] Ross-Talbot S, Fletcher T. Web services choreography description language: Primer version 1.0, May 2006. http://www.w3.org/TR/Year/WD-ws-cdl-10-primer-YearMMDD/

[14] Brogi A, Canal C, Pimentel E, Vallecillo A. Formalizing web service choreographies. Electronic Notes in Theoretical Computer Science, 2004, 105: 73−94

[15] Milner R. Communication and concurrency. Prentice Hall, 1989

[16] Busi N, Gorrieri R, Guidi C, Lucchi R, Zavattaro G. Towards a formal framework for choreography. In: Proceedings of the 14th IEEE International Workshops on Enabling Technologies: Infrastructure for Collaborative Enterprise. 2005, 107−112

[17] Foster H, Uchitel S, Magee J, Kramer J. Model-based analysis of obligations in web service choreography. In: Proceedings of the 2006 International Conference on Internet and Web Applications and Services, AICT-ICIW ’06. 2006, 149

[18] Zaha J M, Barros A P, Dumas M, Hofstede t A H M. Let’s Dance: a language for service behavior modeling. In: Proceedings of the 2006 Confederated International Conference on On the Move to Meaningful Internet Systems. 2006, 145−162

[19] Decker G, Zaha J M, Dumas M. Execution semantics for service choreographies. In: Proceedings of the 3rd International Conference on Web Services and Formal Methods. 2006

[20] Sangiorgi D, Walker D. The π-Calculus: a theory of mobile processes. New York: Cambridge University Press, 2001

[21] Gorrieri R, Guidi C, Lucchi R. Reasoning about interaction patterns in choreography. In: Proceedings of the 2005 International Conference on European Performance Engineering, and Web Services and Formal Methods. 2005, 333−348

[22] Carbone M, Honda K, Yoshida N. A calculus of global interaction based on session types. Electronic Notes in Theoretical Computer Science, 2007, 171(3): 127−151

[23] Decker G, Puhlmann F, Weske M. Formalizing service interactions. In: Proceedings of the 4th International Conference on Business Process Management. 2006, 414−419

[24] Basu S, Bultan T. Choreography conformance via synchronizability. In: Proceedings of the 20th International Conference on World Wide Web. 2011, 795−804

[25] Sun J, Liu Y, Dong J S, Pu G, Tan T H. Model-based methods for linking web service choreography and orchestration. In: Proceedings of the 17th Conference on Asia Pacific Software Engineering. 2010, 166−175

[26] Busi N, Gorrieri R, Guidi C, Lucchi R, Zavattaro G. Choreography and orchestration: a synergic approach for system design. In: Proceedings of the 3rd International Conference on Service-Oriented Computing. 2005, 228−240

[27] Busi N, Gorrieri R, Guidi C, Lucchi R, Zavattaro G. Choreography and orchestration conformance for system design. In: Proceedings of the 8th International Conference on Coordination Models and Language. 2006, 63−81

[28] Baldoni M, Baroglio C, Martelli A, Patti V, Schifanella C. Verifying the conformance of web services to global interaction protocols: A first step. In: Proceedings of the 2005 International Conference on European Performance Engineering, and Web Services and Formal Methods. 2005, 257−271

[29] Fu X, Bultan T, Su J. Conversation protocols: a formalism for specification and verification of reactive electronic services. Theoretical Computer Science, 2004, 328(1): 19−37

[30] Bravetti M, Zavattaro G. Towards a unifying theory for choreography conformance and contract compliance. In: Proceedings of the 6th International Conference on Software Composition. 2007, 34−50

[31] Decker G, Weske M. Local enforceability in interaction petri nets. In: Proceedings of the 5th International Conference on Business Process Management. 2007, 305−319

[32] Aalst v. d W, Dumas M, Ouyang C, Rozinat A, Verbeek H. Choreography conformance checking: an approach based on BPEL and Petri Nets (extended version). Technical report, BPM Center Report BPM-05-25, BPMcenter.org, 2005

[33] Qiu Z, Zhao X, Cai C, Yang H. Towards the theoretical foundation of choreography. In: Proceedings of the 16th International World Wide Web Conference (WWW 2007). 2007, 973−982

[34] Cai C, Qiu Z. An approach to check choreography with channel passing inWS-CDL. In: Proceedings of the 2008 IEEE International Conference on Web Services. 2008, 700−707

[35] Cai C, Yang H, Zhao X, Qiu Z. A formal model for channel passing in web service composition. In: Proceedings of the 2008 IEEE International Conference on Services Computing. 2008, 495−496

[36] Cai C, Qiu Z, Zhao X, Yang H. Correct channel passing by construction. In: Proceedings of 10th International Conference on Formal Engineering Methods. 2008, 338−354

RIGHTS & PERMISSIONS

2013 Higher Education Press and Springer-Verlag Berlin Heidelberg