Business process modeling and verification under service cooperation environment

Service cooperation environment (SCE) is a new and agile business process management (BPM) application development platform grounded on the infrastructure of service cooperation middleware. Business process model is high-level description of business process implementation program. The runtime correctness of business process is closely related to the correctness of business process model. We used Pi-calculus to model, analyze and verify the behavior of business processes under service cooperation environment. We proposed a method for modeling basic actions, including execution action, management action and exception action in Pi-calculus. Then a method for modeling different control flows in SCE is presented. An algorithm which automatically maps business process flow chart to Pi-calculus process expression is proposed. The behavior of typical business processes is studied based on Pi-calculus theory. Automatic verification of business process properties is achieved by describing the properties in μ calculus and verifying it against a model checker. These results will help build model analysis tools based on formalized methods so as to ensure the correctness of business processes.