Abstract
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.
| Original language | English |
|---|---|
| Pages (from-to) | 591-596 |
| Number of pages | 6 |
| Journal | Xibei Gongye Daxue Xuebao/Journal of Northwestern Polytechnical University |
| Volume | 28 |
| Issue number | 4 |
| State | Published - Aug 2010 |
Keywords
- BPM
- Pi-calculus
- Service cooperation environment
- Service cooperation middleware