基于π-演算的WS-BPEL建模与实现

作     者：于鹏伟 

作者单位：西北大学 

学位级别：硕士

导师姓名：侯红

授予年度：2009年

学科分类：08[工学] 0835[工学-软件工程] 081202[工学-计算机软件与理论] 0812[工学-计算机科学与技术（可授工学、理学学位）] 

主      题：业务流程 BPMV WS-BPEL π-演算 MWB 

摘      要：业务流程的设计和验证是所有工作流产品的一个主要功能。为了能够尽早发现流程建模中死锁、缺少同步等问题,大部分工作流产品都需要提供基于形式化分析和建模的功能。由于WS-BPEL(Web Services Business Process Execution Language)描述业务流程是半形式化的,不易检测与验证,也没有相应形式化工具支持,这使得Web服务组合的正确性难以保证,其业务流程也无法在较抽象的层次上进行跟踪。 本文结合实验室承担的国家863科研攻关项目,针对业务流程内部逻辑的正确性问题展开研究,探索利用进程代数π-演算作为形式化工具,对WS-BPEL描述的业务流程进行建模和验证。主要进行的工作如下: 1.本文提出了业务流程建模与验证的体系结构BPMV(Business Process Modeling andVerfication)、说明了本文要解决问题及所采取的步骤,分析了基于Petri网、自动机理论、进程代数对WS-BPEL活动进行建模的方法和成果。 2.本文分析了国内外基于π-演算对WS-BPEL活动建模的相关研究现状。说明了π-演算适合对WS-BPEL活动进行建模的原因,完善了π-演算对WS-BPEL活动的建模,在此基础上给出了WS-BPEL到π-演算整体转换的算法描述。 3.针对业务流程中可能存在的死锁、活锁、互模拟问题,本文结合实例用π-演算对业务流程性质进行了分析、推演,并用MWB(Mobility Workbench)进行了验证。 4.基于eclipse开发环境和SWT插件,设计和实现了B2P原型工具。