计算机工程与科学2011，Vol.33Issue(9)：76-80,5.DOI:10.3969/j.issn.1007-130X.2011.09.014
一种基于抽象与精化技术的Web服务组合验证方法
A Verification Method for Web Services Combination Based on Abstract and Refinement Techniques
摘要
Abstract
Model checking has been widely used to verify the compatibility of Web services composition 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.关键词
Web服务组合/模型检测/谓词抽象/精化技术Key words
Web services combination/ model checking/ predicate abstraction refinement technique分类
信息技术与安全科学引用本文复制引用
陈国彬,任强,张广泉..一种基于抽象与精化技术的Web服务组合验证方法[J].计算机工程与科学,2011,33(9):76-80,5.基金项目
江苏省自然科学基金项目(BK2011152) （BK2011152）
中国科学院计算机科学国家重点实验室开放课题(CSYSKF0908) （CSYSKF0908）
