Formal checking of WS-BPEL orchestrations

This paper is focused on understanding techniques used to formally verify behaviour of business processes developed using WS-BPEL standard. The first part of the paper gives an overview of WS-BPEL control-flow constructs. We analyze offered constructs and try to derive control-flow scenarios that can be built out of them. Derived complex control-flow scenarios are further discussed. Possible execution misbehaviour, which cannot be discovered by pure static analysis of WS-BPEL code, is identified. Misbehaviour can be any of the following: unreachable code, deadlock states, non-progress cycles (code is repeated without passing through progress state), or any other unwanted scenario, like unwanted execution order of activities, unwanted order of messages being exchanged and similar execution misbehaviour. The second part of the paper describes techniques used for formal verification of any code in general with an emphasis on research how these techniques are exploited to verify WS-BPEL code. The final part of the paper concludes with the discussion how successful described work was in verification of possible identified misbehaviour from the first part of the paper.