Typed formal model for WS-CDL specification of web services composition

In order to formally reason and verify web services composition described by web services choreography specification WS-CDL,a typed formal model named typed Abstract WS-CDL（web services choreography description language）for WS-CDL specifications is proposed.In typed Abstract WS-CDL,the syntax of type and session,typing rules and operational semantics are formalized;the collaborations of web services are formally described by sessions;the operational semantics of a session can help to formally reason the execution of the choreography;the typing rules can help to formally check the data type consistency of exchanged information between web services and capture run-time errors due to type mismatches.Particularly,the concepts of type assumption set extension and type assumption set compatibility are proposed,and the merging algorithm of type assumption sets is defined so as to eliminate type assumption conflict.Based on the formal model,typed mapping rules for mapping web services choreography to orchestration is also defined.With the typed mapping rules,orchestration stubs and their type assumption sets can be generated from a given choreography; thus, web services composition can be verified at choreography and orchestration levels,respectively.The model is proved to have properties of type safety,and how the model can help to reason and verify web services composition is illustrated through a case study.

Algorithms for checking channel passing in web service choreography

Web service choreography describes global mod- els 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 ex- ecution will get stuck. Since channels are composed dynami- cally, the initial channel set of each participant is often insuf- ficient 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 par- ticipants and complex channel constraints, it is hard for de- signers 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 chan- nels, 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 sim- ple language Chorc, a channel interaction sub-language for modeling the channel passing aspect of service choreography. Based on the formal operational semantics of Chore, the algo- rithms for static checking of service choreography and gen- erating channel passing are also studied, and the complexity results of algorithms are discussed. Moreover, some illus- trated service choreography examples are presented to show how to formalize and analyze service choreography with channel passing in Chorc.