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