Towards a Formal Verification Approach for Business Process Coordination

BPEL (Business Process Execution Language) enacts a process-oriented web service orchestration, and multi-business processes can be regarded as BPEL composition. A business process can be regarded as a complex set of interactions among Web services to achieve a defined goal. The achievement of distributed agreement among multiple-participant services is an orthogonal problem outside the scope of BPEL, so the rationality for distributed coordination of multi-business processes is an urgent issue to study. The definition of the message exchanges that take place between the process and each one of its partners lack the precise definition which is required for performing a formal analysis and reasoning. An integrated approach supporting a formal verification of multi-business interactions is proposed. This paper first examines a rigorous approach for the formalization of the execution semantics of business process in the Pi-calculus. Then transforms the Pi-calculus expressions into equivalent SMV code and verifies the system whether a process satisfies given properties automatically using the NuSMV model checker, and the approach is illustrated using a concrete case study subsequently. The approach supports creating robust multi-business processes which are distributed or span multiple vendors and platforms.