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

【Abstract】 In the research of Web service compositions,it was lack of the verification of quantitative property and the fault handling method for exceptions from runtime services.A method for formal verification of Web service compositions based on the extended finite automata was presented.First the finite automata was extended and presented a formal model of Web service which can describe the data and time information;Based on the model,CTL was used to describe related properties,and model checking tool—UPPAAL was used to verify the behavior property,timed property and data related property.At last,based on the diagnosis model established,a diagnosis algorithm that can handle exceptions from runtime Web service compositions was presented.更多还原