一种基于抽象与精化技术的Web服务组合验证方法

A Verification Method for Web Services Combination Based on Abstract and Refinement Techniques

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

Model checking has been widely used to verify the compatibility of Web services composi- tion models, since it can give counterexamples and high automation. As for the state explosion problem existing in model checking, we introduce the predicate abstraction and refinement techniques into the traditional model checking method, and propose a framework for Web services composition based on the such techniques. First, we model each Web service based on the predicate abstraction and composite the models with combination operations. Second, we project the counterexamples obtained by model checking over each Web service, and confirm the projection counterexamples. Third, the Web service abstraction model that causes spurious counterexamples is refined, and a new composition abstract model, whose properties also should be verified, is generated. Finally, we show the correctness of our proposal to relieve state explosion.