服务协同环境中的业务过程建模与验证  

Business Process Modeling and Verification under Service Cooperation Environment

作　　者：符宁[1,2] 周兴社[1] 詹涛[1] 

机构地区：[1]西北工业大学计算机学院,陕西西安710072 [2]解放军西安政治学院,陕西西安710068

出　　处：《西北工业大学学报》2010年第4期591-596,共6页Journal of Northwestern Polytechnical University

基　　金：国家"863"高技术研究发展计划重大专项基金(2009AA010308);国家"863"高技术研究发展计划基金(2006AA01Z162);"核高基"重大专项基金;国家发展与改革委员会项目(20052139)资助

摘　　要：服务协同环境是以服务协同中间件为底层平台,面向企业级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.

关 键 词：服务协同环境 服务协同中间件 业务过程管理 PI演算 

分 类 号：TP31[自动化与计算机技术—计算机软件与理论]