A Formal Model for Service Choreography with Exception Handling and Finalization

The service choreography gives a global view on the collaboration among a collection of services involving multiple different organizations or independent processes. In this paper, a formal model for service choreography based on WS-CDL language is proposed. This model explores the key concepts related to choreography, such as passing channel, fault handling and finalization mechanisms. This study brings us the insights for the analysis, synthesis and verification of service choreography. For instance, the choreography synthesis is discussed based on our trace semantics achieved.