Ensuring Coordination of Multi-business Interactions

While the potential benefits of multi-business interaction automation are truly phenomenal, the complexity of business has increased dramatically, and building reliable and secure e-business application systems becomes an important issue. Industry standards for Web service composition, such as BPEL, provide the notion of LRT (Long running transaction) for the execution of business processes in Web service collaborations. Formal verification of BPEL programs and specifications has become a hot topic. However, the notion of LRT described in BPEL is purely local and occurs within a single business process instance. In this work a two-step model checking method, from simply to the complex, is proposed for multi-business process. A preliminary step is to judge business correctness on external logic transition relations amongst businesses with various simple symbolic model checking tools, and then make further checking interaction validation based on internal system behavior in multi-business coordination with model checking verification environment for mobile processes. The typical scenario is illustrated to show how model checking is applied to verify the reliability of multi-business coordination. All of these have important implications for ensuring multi-business process coordination.