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

J4 ›› 2011, Vol. 33 ›› Issue (9): 76-80.

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

陈国彬1，任〓强2,张广泉2,3

（1．重庆工商大学融智学院，重庆 400033；2.苏州大学计算机科学与技术学院，江苏苏州 215006； 3.中国科学院计算机科学国家重点实验室，北京 100080）

收稿日期:2011-05-20 修回日期:2011-07-28 出版日期:2011-09-25 发布日期:2011-09-25
作者简介:陈国彬（1982），男，江苏建湖人，硕士,助教，研究方向为软件体系结构、Web服务与形式化方法。
基金资助:
江苏省自然科学基金项目(BK2011152);中国科学院计算机科学国家重点实验室开放课题（CSYSKF0908）

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

CHEN Guobin1,REN Qiang2,ZHANG Guangquan2,3

(1.Rongzhi College,Chongqing Technology and Business University,Chongqing 400033;2.School of Computer Science and Technology,Soochow University,Suzhou 215006;3.State Key Laboratory of Computer Science,Chinese Academy of Sciences,Beijing 100080,China)

Received:2011-05-20 Revised:2011-07-28 Online:2011-09-25 Published:2011-09-25

摘要/Abstract

摘要：

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

关键词: Web服务组合, 模型检测, 谓词抽象, 精化技术

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.

Key words: Web services combination;model checking;predicate abstraction;refinement technique

陈国彬1，任〓强2,张广泉2,3. 一种基于抽象与精化技术的Web服务组合验证方法[J]. J4, 2011, 33(9): 76-80.

CHEN Guobin1,REN Qiang2,ZHANG Guangquan2,3. A Verification Method for Web Services Combination Based on Abstract and Refinement Techniques[J]. J4, 2011, 33(9): 76-80.

[1]	刘子源, 马占有, 李霞, 高滢囡, 何娜娜, 黄瑞祺. 基于模糊测度的模糊分支时态逻辑模型检测[J]. 计算机工程与科学, 2024, 46(04): 676-683.
[2]	李召恺, 马占有, 李健祥, 郭昊. 基于模糊决策过程的模糊计算树逻辑模型检测[J]. 计算机工程与科学, 2022, 44(02): 266-275.
[3]	郑小宇, 刘冬梅, 杜益宁, 周子健, 邱玫媚, 朱鸿. 模式驱动的系统安全性设计的验证[J]. 计算机工程与科学, 2020, 42(07): 1197-1207.
[4]	刘婷1,2,杨秋翔1. 基于混沌机制与Levy变异烟花算法的服务组合优化[J]. 计算机工程与科学, 2019, 41(09): 1618-1626.
[5]	袁申,魏杰林,李永明. 具有多值决策过程的广义可能性计算树逻辑模型检测[J]. 计算机工程与科学, 2019, 41(01): 88-97.
[6]	钟小妹，肖美华，李伟，谌佳，李娅楠. RFID超轻量级认证协议RCIA形式化分析与改进[J]. 计算机工程与科学, 2018, 40(12): 2183-2192.
[7]	王亚鹏，雷丽晖. 基于CTL模型检测的胃腺癌核心路径形式化验证[J]. 计算机工程与科学, 2018, 40(12): 2280-2286.
[8]	雷丽晖，郭越，张延波. 可能性测度下的CTL符号化模型检测[J]. 计算机工程与科学, 2018, 40(11): 2008-2014.
[9]	郭雪1，李铮2，张贺3，荣国平3，文俊浩1. Web服务组合策略研究及组合决策平台实现[J]. 计算机工程与科学, 2018, 40(08): 1358-1365.
[10]	肖美华1，梅映天1,2，李伟1，李娅楠1，钟小妹1，宋子繁1. 基于时间戳私钥签名技术的Nayak-T协议安全性分析[J]. 计算机工程与科学, 2017, 39(12): 2252-2259.
[11]	袁红娟1,2,马艳芳3,潘海玉1,2. 模糊交互时态逻辑的模型检测[J]. 计算机工程与科学, 2017, 39(12): 2290-2296.
[12]	吴格格，庄雷，张坤丽，王国卿. 移动支付协议PCMS的形式化分析和验证[J]. 计算机工程与科学, 2017, 39(01): 67-73.
[13]	程道雷,肖美华,刘欣倩,梅映天,李伟. 运用SPIN对开放授权协议OAuth 2.0的分析与验证[J]. J4, 2015, 37(11): 2121-2127.
[14]	马占有1，2，李永明1. 广义可能性决策过程的计算树逻辑模型检测[J]. J4, 2015, 37(11): 2162-2168.
[15]	刘姣，雷丽晖. 一种基于扩展不完全Kripke结构的三值逻辑模型检测方法[J]. J4, 2015, 37(10): 1884-1889.