论文部分内容阅读
如今Web服务广泛分布于互联网中,它们通过彼此之间的交互实现对问题的协作求解。然而,在交互过程中,一些非预期、“不正常”的信息交互时有发生,严重影响了系统的质量及健壮性,有可能使用户得不到正确结果。因此,模型检测Web服务组合的时态认知性质,保障Web服务的正确运行就成为了模型检测领域的热门研究方向。目前,国内外针对Web服务组合的形式化验证正处于起步阶段,整个验证过程的自动化程度很低,各个技术环节都需要大量的人工操作。为了提高Web服务流程验证的自动化程度,本文提出将Web服务组合的BPEL流程自动转化为模型检测工具MCTK输入代码的一系列转换算法。最后利用这些算法在MCTK环境下对VTA协议和STS协议进行了形式化验证,并自动构建了贷款服务协议的状态转换图。取得的研究成果有:(1)针对Web服务描述语言BPEL,给出相关活动语义。引入迁移七元组概念,基于活动语义,建立BPEL活动与能够反映系统状态迁移关系的迁移七元组的一一对应,为实现流程的自动化验证打下基础;(2)分别提出将BPEL控制流、数据流转化为迁移七元组集合的转换算法B2T和F2T。这些算法自动将BPEL流程转化为迁移七元组集合,实现了将组合业务流程自动转化为多分支状态转换图的功能;(3)提出根据迁移七元组集合自动生成MCTK代码的转换算法T2M。为了实现控制流的全自动检测,T2M算法根据迁移七元组集合中各元组的相互关系,结合MCTK语言自身特点,自动生成用来描述流程的MCTK代码,避免了繁琐的人工编码工作,实现控制流的自动化检测;(4)运用模型检测工具MCTK验证VTA的时态认知规范以及STS中存在的特征交互问题,说明了论文提出方法的正确性及有效性,同时,利用F2T算法自动构建了贷款服务协议的状态转换图,为下一步验证做好了准备。