摘要
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.
源语言 | 英语 |
---|---|
页(从-至) | 591-596 |
页数 | 6 |
期刊 | Xibei Gongye Daxue Xuebao/Journal of Northwestern Polytechnical University |
卷 | 28 |
期 | 4 |
出版状态 | 已出版 - 8月 2010 |