Correct Channel Passing by Construction

摘要

Channel passing is a mechanism to describe dynamic composition of parallel systems. As to Web services, both WS-BPEL and WS-CDL adopts this mechanism to support dynamic business processes. Web service composition may suffer from channel passing, e.g., some service might not get a correct channel to complete an interaction, and then the whole system would get stuck. The work presented here is aimed at designing services which are immune to channel problems. Firstly, we define a pair of model languages on both global and local levels with formally defined semantics. Based on these languages, we propose a top-down design methodology that generates local-level processes from a global specification. Finally, we give out a set of conditions for global specifications, from which the generated processes are guaranteed correct.