Algorithms for checking channel passing in web service choreography

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) .Computer Science, Information SystemsComputer Science, Software EngineeringComputer Science, Theory & MethodsSCI(E)EI中国科学引文数据库(CSCD)0REVIEW5710-728