中文摘要：

服务协同环境是以服务协同中间件为底层平台,面向企业级BPM、EAI和B2B应用的软件环境。文章基于进程代数方法研究了服务协同环境中服务基本活动建模、控制模式建模和业务过程的建模等问题。提出一种从用户设计界面有向图到服务过程表达式的生成算法。同时,文中还研究了如何用μ演算描述流程性质,并使用验证工具研究了流程正确性验证问题。

英文摘要：

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.