A Petri Net Semantics for Web Service in Choreography Description Language

Web service composition refers to the process of combining several value-added services. It has received much interest in enterprise applications. Web Service Choreography Description Language (WSCDL) is a W3C specification for the description of peer-to-peer collaborations of participants from a global viewpoint. As an XML-based language aimed to become a Web service composition standard for choreography, WSCDL may clarify the opaque points, detect and repair design errors in the language definition, yet provide the theoretical grounding for relative tools development. Petri net is a first-class formal modeling tool that has been widely used in many fields. Based on a Petri net, this paper proposed a formal model that can be used to clarify the semantics of WSCDL and verify some relative properties throughout. The model helps analyze the semantic compatibility between a business process specified in Business Process Execution Language (BPEL) and a WSCDL process.