基于扩展自动机的服务组合静态与动态验证方法

针对目前Web服务组合研究中缺少对定量属性的验证以及在服务运行过程中缺乏对出现异常时的故障处理等问题,提出了一种基于扩展有限自动机的Web服务组合静态与动态验证方法。该方法首先对有限自动机进行扩展,建立了一个可以描述数据及时间等信息的Web服务组合形式化模型;基于该模型,采用计算树逻辑(CTL)描述相关属性,并利用模型检测工具UPPAAL对Web服务组合的行为属性、时间属性以及数据属性等进行了验证;最后结合所建立的诊断模型,给出了一种能够对Web服务组合运行过程中出现异常时进行有效处理的错误诊断算法。     

数据和时间感知的Web服务组合模型检测

为了验证Web服务组合中的数据属性和时间属性,提出了一种基于数据和时间感知的服务模型DTSM的Web服务组合模型检测方法。首先将I3PEL描述的Web服务组合转换为含有数据流信息和时间信息的形式化模型,然后将该模型映射至UPPAAL规约,最后应用模型检测工具UPPAAL实现了Web服务组合的正确性验证。