摘要：模型检测因其自动化程度高、能够提供反例路径等优势，被广泛应用于Web服务组合的兼容性验证。本文针对模型检测过程中存在的状态爆炸问题，在传统的模型检测方法中引入谓词抽象和精化技术，提出了一种针对Web服务组合的抽象精化验证框架。使用谓词抽象技术对原子web服务抽象建模，将各Web服务抽象模型组合成组合抽象模型；将模型检测后得到的反例在各原子web服务上做投影操作，对投影反例进行确认；对产生伪反例的web服务抽象模型进行精化，生成新的组合抽象模型，再次对性质进行验证。最后通过实例分析说明基于抽象精化技术的Web服务组合验证框架在缓解状态爆炸问题上的可行性。

关键词：web服务组合 模型检测 谓词抽象 精化技术 

单位：重庆工商大学融智学院 重庆400033 苏州大学计算机科学与技术学院 江苏苏州215006 中国科学院计算机科学国家重点实验室 北京100080