A Formal Basis for Cross-Checking ebXML BPSS Choreography and Web Service Orchestration

ebXML is a global business-to-business (B2B) electronic commerce standard which addresses not only the formats and vocabularies of electronic business documents exchanged between business partners, but also the choreography of business transactions during a collaborative process. On the other hand, the service-oriented architectures (SOA) together with Web services promise a new era for B2B collaboration with dynamically created business partnerships transacting based on published choreographies, for which the ebXML BPSS (business process specification scheme) is a major specification language. To implement such a collaboration process, business partners can package their enterprise applications as Web services and orchestrate them in WS-BPEL according to the published choreography for the process. This paper contributes to the successful implementation of collaborative processes based on Web services by introducing a formal basis for verifying the consistency between ebXML BPSS choreography and WS-BPEL Web service orchestration. We illustrate the approach with a contract negotiation process.