Channel passing mechanisms enable dynamically determining destinations of message transferring. WS-CDL, a language developed by W3C for the specification of Web services choreographies, adopts channel passing to support dynamic Web services composition. A choreography can be projected into individual services or orchestration skeletons. It is a challenge to ensure the services generated from a choreography always have sufficient and correct channels to complete their collaboration. In fact, WS-CDL is not ready for rigorous validation and implementation with respect to channel passing, since it provides no structure for specifying explicitly which role should firstly initialize which channel variable. Here we propose an algorithm to uncover these implicit assumptions, that is implemented as an extension to Pi4SOA. With the help of the algorithm, some existing methods for verification and implementation can be applied on choreographies written in WS-CDL. In addition, we propose an approach to detect design defects in choreographies, and show how a defect is found from the main sample choreography in WS-CDL Primer. It seems that choreographies with channel passing are error prone. Methods and tools are necessary to support designers in this field. Also, we suggest improving the situation by adding a syntactical construct to WS-CDL.

BPEL (Business Process Execution Language) has become the standard for specifying and executing workflow specifications for Web service composition invocation. A major weakness of BPEL is the lack of so-called "human workflow" support. The BPEL4People specification tries to amend this by adding human task support to BPEL. In this paper, we propose a formal model of BPEL4People using the CSP process algebra, and discuss some issues we found through analyzing the model. Although based on BPEL4People, this is a general work, and can also be viewed as a formal model of human workflow.

Web services 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. Because of dynamic composition, the initial channel set on 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 some others. Since a choreography may involve many participants and complex channel constraints, it is hard for designers to specify channel passing in a choreography exactly as required. In this paper, we address the problem of checking whether a choreography lacks channels or has redundant channels, and how to automatically generate channel passing based on interaction flows of the choreography in the case of channel absence. Concretely, we propose a small language Chorcnamed for a channel interaction sub-language for modeling the channel passing aspect of choreography. Based on the formal operational semantics of Chorc, the algorithms for static checking choreography and generating channel passing are studied as well.

With the growth of interest on the web services, people pay increasinglyattention to the choreography, that is, to describe collaborations ofparticipants in accomplishing a common business goal from a globalviewpoint. In this paper, based on a simple choreography language and arole-oriented process language, we study some fundamental issues relatedto choreography, especially those related to implementation, includingsemantics, projection and natural projection, dominant role in choices anditerations, etc. We propose the concept of dominant role and somenovel languages structures related to it. The study reveals some cluesabout the language, the semantics, the specification and theimplementation of choreography.