Algorithms for checking channel passing in web service choreography
Tóm tắt
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 Chor
c
, a channel interaction sub-language for modeling the channel passing aspect of service choreography. Based on the formal operational semantics of Chor
c
, 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 Chor
c
.
Tài liệu tham khảo
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
Web Services Choreography Description Language, version 1.0, 2005. http://www.w3.org/TR/2005/CR-ws-cdl-10-20051109/
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
Thatte S. XLANG web services for business process design. 2001, http://www.gotdotnet.com/team/xml_wsspecs/xlang-c/default.htm
Leymann F. Web services flow language (WSFL 1.0). May 2001, http://www.ibm.com/software/solutions/webservices/pdf/WSFL.pdf
Business Process Execution Language for Web Services (BPEL4WS), version 1.1. May 2003, http://www.ibm.com/developerworks/webservices/library/ws-bpel/
Arkin A. Business process modeling language. November 2002, http://www.bpmi.org
Yang H, Cai C, Peng L, Zhao X, Qiu Z. Reasoning about channel passing in choreography. In: Proceedings of the 2nd IEEE International Symposium on Theoretical Aspects of Software Engineering. 2008, 135–142
Kavantzas N. A post at petri-pi mailing list, August 2005
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
Holzmann G J. The SPIN model checker: primer and reference manual. Addison-Wesley, 2003
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
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/
Brogi A, Canal C, Pimentel E, Vallecillo A. Formalizing web service choreographies. Electronic Notes in Theoretical Computer Science, 2004, 105: 73–94
Milner R. Communication and concurrency. Prentice Hall, 1989
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
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
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
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
Sangiorgi D, Walker D. The π-Calculus: a theory of mobile processes. New York: Cambridge University Press, 2001
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
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
Decker G, Puhlmann F, Weske M. Formalizing service interactions. In: Proceedings of the 4th International Conference on Business Process Management. 2006, 414–419
Basu S, Bultan T. Choreography conformance via synchronizability. In: Proceedings of the 20th International Conference on World Wide Web. 2011, 795–804
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
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
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
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
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
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
Decker G, Weske M. Local enforceability in interaction petri nets. In: Proceedings of the 5th International Conference on Business Process Management. 2007, 305–319
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
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
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
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
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