Building Multi-business Processes Coordination Model in Pi-Calculus

With the growth in Web services technology and more complex business applications, there is renewed interest in business process coordination, especially for multi-business processes. Industry standards for Web Service composition, such as BPEL, provide the notion of long running transaction (LRT) for the execution of business processes in Web Service collaborations. However, the notion of LRT described in BPEL is purely local and occurs within a single business process instance. The specification considered here is the tentative hold protocol (THP) which facilitates the automated coordination of multi-business interactions. This work tries to describe a formalization of multi-business processes coordination, which adds THP protocol information to the specifications of interacting services, and uses Pi-calculus to model the coordination interactions, thereby enabling formal analysis of relevant properties by model checking. All of these have important implications for implementing automatic multi-business processes coordination.