Algorithms for checking channel passing in web service choreography

doi:10.1007/s11704-013-1238-z

Front. Comput. Sci.

2013, Vol. 7

Issue (5) : 710-728 https://doi.org/10.1007/s11704-013-1238-z

REVIEW ARTICLE

Algorithms for checking channel passing in web service choreography

Hongli YANG^1,²(

), Chao CAI³, Liyang PENG⁴, Xiangpeng ZHAO⁵, Zongyan QIU⁶, Shengchao QIN^1,⁷

¹. College of Computer Sciences, Beijing University of Technology, Beijing 100222, China
². Institute of Software, Chinese Academy of Sciences, Beijing 100080, China
³. China Defense Science and Technology Information Center, Beijing 100142, China
⁴. Vancl Research Lab, Beijing 100124, China
⁵. Facebook Inc., California 94025, USA
⁶. LMAM and Department of Informatics, School of Mathematical Sciences, Peking University, Beijing 100871, China
⁷. School of Computing, University of Teesside, Middlesbrough, TS1 3BA, UK

Download: PDF(0 KB)
Export: BibTeX | EndNote | Reference Manager | ProCite | RefWorks

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

Corresponding Author(s): Hongli YANG

Issue Date: 01 October 2013

Cite this article:

Hongli YANG,Chao CAI,Liyang PENG, et al. Algorithms for checking channel passing in web service choreography[J]. Front. Comput. Sci., 2013, 7(5): 710-728.

URL:

https://academic.hep.com.cn/fcs/EN/10.1007/s11704-013-1238-z
https://academic.hep.com.cn/fcs/EN/Y2013/V7/I5/710

1	J M Zaha , M Dumas , T A Hofstede , A Barros , G Decker . 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.
3	M Carbone , K Honda , N Yoshida . Structured communication-centred programming for web services. In: Proceedings of the 16th European Conference on Programming. 2007, 2−17
4	S Thatte . XLANG web services for business process design. 2001
5	F Leymann . Web services flow language (WSFL 1.0). May 2001,
6	. Business Process Execution Language for Web Services (BPEL4WS), version 1.1. May 2003,
7	. Arkin A. Business process modeling language. November 2002,
8	H Yang , C Cai , L Peng , X Zhao , Z Qiu . 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	N Kavantzas . A post at petri-pi mailing list, August 2005
10	M Carbone , K Honda , N Yoshida , R Milner , G Brown , . Ross-Talbot S. A theoretical basis of communication-centred concurrent programming. Technical report, W3C, 2006.
11	G J Holzmann . The SPIN model checker: primer and reference manual. Addison-Wesley, 2003
12	A P Barros , M Dumas , HM Hofstede t A . Service interaction patterns. In: Proceedings of the 3rd International Conference on Business Process Management. 2005, 302−318
13	S Ross-Talbot , T Fletcher . Web services choreography description language: Primer version 1.0, May 2006.
14	A Brogi , C Canal , E Pimentel , A Vallecillo . Formalizing web service choreographies. Electronic Notes in Theoretical Computer Science, 2004, 105: 73−94 https://doi.org/10.1016/j.entcs.2004.05.007
15	R Milner . Communication and concurrency. Prentice Hall, 1989
16	N Busi , R Gorrieri , C Guidi , R Lucchi , G Zavattaro . 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	H Foster , S Uchitel , J Magee , J Kramer . 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	J M Zaha , A P Barros , M Dumas , A H M Hofstede t . 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	G Decker , J M Zaha , M Dumas . Execution semantics for service choreographies. In: Proceedings of the 3rd International Conference on Web Services and Formal Methods. 2006 https://doi.org/10.1007/11841197_11
20	D Sangiorgi , D Walker . The π-Calculus: a theory of mobile processes. New York: Cambridge University Press, 2001
21	R Gorrieri , C Guidi , R Lucchi . 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	M Carbone , K Honda , N Yoshida . A calculus of global interaction based on session types. Electronic Notes in Theoretical Computer Science, 2007, 171(3): 127−151 https://doi.org/10.1016/j.entcs.2006.12.041
23	G Decker , F Puhlmann , M Weske . Formalizing service interactions. In: Proceedings of the 4th International Conference on Business Process Management. 2006, 414−419
24	S Basu , T Bultan . Choreography conformance via synchronizability. In: Proceedings of the 20th International Conference on World Wide Web. 2011, 795−804 https://doi.org/10.1145/1963405.1963516
25	J Sun , Y Liu , J S Dong , G Pu , T H Tan . 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	N Busi , R Gorrieri , C Guidi , R Lucchi , G Zavattaro . Choreography and orchestration: a synergic approach for system design. In: Proceedings of the 3rd International Conference on Service-Oriented Computing. 2005, 228−240
27	N Busi , R Gorrieri , C Guidi , R Lucchi , G Zavattaro . Choreography and orchestration conformance for system design. In: Proceedings of the 8th International Conference on Coordination Models and Language. 2006, 63−81 https://doi.org/10.1007/11767954_5
28	M Baldoni , C Baroglio , A Martelli , V Patti , C Schifanella . 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	X Fu , T Bultan , J Su . Conversation protocols: a formalism for specification and verification of reactive electronic services. Theoretical Computer Science, 2004, 328(1): 19−37 https://doi.org/10.1016/j.tcs.2004.07.004
30	M Bravetti , G Zavattaro . Towards a unifying theory for choreography conformance and contract compliance. In: Proceedings of the 6th International Conference on Software Composition. 2007, 34−50 https://doi.org/10.1007/978-3-540-77351-1_4
31	G Decker , M Weske . Local enforceability in interaction petri nets. In: Proceedings of the 5th International Conference on Business Process Management. 2007, 305−319
32	W Aalst v. d , M Dumas , C Ouyang , A Rozinat , H Verbeek . 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	Z Qiu , X Zhao , C Cai , H Yang . Towards the theoretical foundation of choreography. In: Proceedings of the 16th International World Wide Web Conference (WWW 2007). 2007, 973−982 https://doi.org/10.1145/1242572.1242704
34	C Cai , Z Qiu . 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	C Cai , H Yang , X Zhao , Z Qiu . A formal model for channel passing in web service composition. In: Proceedings of the 2008 IEEE International Conference on Services Computing. 2008, 495−496 https://doi.org/10.1109/SCC.2008.110
36	C Cai , Z Qiu , X Zhao , H Yang . Correct channel passing by construction. In: Proceedings of 10th International Conference on Formal Engineering Methods. 2008, 338−354

[1]	Shuaiqiang WANG, Yilong YIN. Polygene-based evolutionary algorithms with frequent pattern mining[J]. Front. Comput. Sci., 2018, 12(5): 950-965.
[2]	Quanjun YIN, Long QIN, Yong PENG, Wei DUAN. Learning real-time search on c-space GVDs[J]. Front. Comput. Sci., 2017, 11(6): 1036-1049.
[3]	Yingying ZHU,Cong YAO,Xiang BAI. Scene text detection and recognition: recent advances and future trends[J]. Front. Comput. Sci., 2016, 10(1): 19-36.
[4]	Silvano COLOMBO TOSATTO,Pierre KELSEN,Qin MA,Marwane el KHARBILI,Guido GOVERNATORI,Leendert van der TORRE. Algorithms for tractable compliance problems[J]. Front. Comput. Sci., 2015, 9(1): 55-74.
[5]	Chaoqun LI,Liangxiao JIANG,Hongwei LI. Naive Bayes for value difference metric[J]. Front. Comput. Sci., 2014, 8(2): 255-264.
[6]	Dunwei GONG, Yan ZHANG. Generating test data for both path coverage and fault detection using genetic algorithms[J]. Front Comput Sci, 2013, 7(6): 822-837.
[7]	Yi WANG, Renfa LI. FPGA based unified architecture for public key and private key cryptosystems[J]. Front Comput Sci, 2013, 7(3): 307-316.
[8]	Jie LUO. A general framework for computing maximal contractions[J]. Front Comput Sci, 2013, 7(1): 83-94.
[9]	Bo YUAN, Wenhuang LIU. Measure oriented training: a targeted approach to imbalanced classification problems[J]. Front Comput Sci, 2012, 6(5): 489-497.
[10]	Min XIE, Laks V. S. LAKSHMANAN, Peter T. WOOD. Composite recommendations: from items to packages[J]. Front Comput Sci, 2012, 6(3): 264-277.
[11]	Fabian GIESEKE, Gabriel MORUZ, Jan VAHRENHOLD. Resilient k-d trees: k-means in space revisited[J]. Front Comput Sci, 2012, 6(2): 166-178.
[12]	Kenli LI, Zhao TONG, Dan LIU, Teklay TESFAZGHI, Xiangke LIAO. A PTS-PGATS based approach for data-intensive scheduling in data grids[J]. Front Comput Sci Chin, 2011, 5(4): 513-525.
[13]	Maryjane TREMAYNE, Samantha Y. CHONG, Duncan BELL. Optimisation of algorithm control parameters in cultural differential evolution applied to molecular crystallography[J]. Front Comput Sci Chin, 2009, 3(1): 101-108.
[14]	Carlos A. COELLO COELLO. Evolutionary multi-objective optimization:some current research trends and topics that remain to be explored[J]. Front Comput Sci Chin, 2009, 3(1): 18-30.
[15]	ZHANG Jian, ZHANG Wenhui, ZHAN Naijun, SHEN Yidong, CHEN Haiming, ZHANG Yunquan, WANG Yongji, WU Enhua, WANG Hongan, ZHU Xueyang. Basic research in computer science and software engineering at SKLCS[J]. Front. Comput. Sci., 2008, 2(1): 1-11.

Viewed

Full text

Abstract

Cited

Shared

Discussed