Formalizing exception handling in WS-CDL and WS-BPEL for conformance verification

We have previously developed a formal approach to verifying conformance for Web services choreography based on the formalism of Communicating Sequential Processes (CSP). In this paper, we extend the approach to cover exception handling, which is commonly used in specifying the choreography as well as orchestration of Web services. In particular, we show how timeout exceptions and message events are handled in the formal approach and illustrate it using a document ordering and delivery process as an example.