一种基于Mealy机的BPEL程序验证模型研究

作     者：闻晓 

作者单位：西南大学 

学位级别：硕士

导师姓名：张为群

授予年度：2009年

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

主      题：BPEL 模型检测 Web服务 Web服务编制 

摘      要：BPEL作为描述Web服务编制的语言之一,在商业流程中被用来描述活动和对活动的控制。BPEL具有类似程序设计语言的语法结构,如顺序、分支和循环等,能表达对业务流程的控制。BPEL语法中还有专为商业流程设计的结构,兼顾了IT和商业两个领域的需求。但是这给BPEL程序验证带来了难题。BPEL不是一种可执行的程序语言,往往冗长而复杂,仍然存在二义性、不一致性和不完备性。为了提高Web服务中BPEL应用程序的健壮性,有必要改进程序验证的方法。 本文对现有基于模型检测技术的BPEL程序验证方法进行了研究,提出了一种基于Mealy机的验证模型BVM（BPEL Verification Machine）,并利用该模型建立了一个验证BPEL程序性质的方法。本文通过已知BPEL程序源码找出验证程序需要的BVM模型M和通过用户需求说明书找出待验证的性质P,设计并实现了一个在模型检测器NuSMV中验证M是否满足P的引擎。实验显示该方法能够验证包括补偿的BPEL程序,弥补了现有方法在这方面的不足。