《计算机学报》文章摘要   全文下载
文章题目	一种基于认知模型检测的Web服务组合验证方法
作者	骆翔宇1)，2) 谭征3) 苏开乐4)，5) 吴立军6)
作者单位	1)(华侨大学计算机科学与技术学院 福建 厦门 361021) 2)(清华大学软件学院 北京 100084) 3)(中核兰州铀浓缩有限公司 兰州 730065) 4)(北京大学教育部高可信软件重点实验室 北京 100871) 5)(浙江师范大学数理信息学院 浙江 金华 321004) 6)(电子科技大学计算机科学与工程学院 成都 410073)
发表年份	2011
发表月份	6期(1041—1061)
文章摘要	摘要 近几年Web服务组合的形式化验证逐渐成为研究热点.模型检测作为形式化验证的一种主流技术，可以克服传统软件测试用例生成不完备的不足，同时具有验证自动化的优点.该文提出并实现了一种Web服务组合的认知模型检测方法，将Web服务组合建模为多主体系统，在分析BPEL语言控制流程基础上，提出BPEL活动的形式化模型，给出活动执行语义.进而以迁移七元组为中间形式，开发从BPEL流程到迁移七元组集合以及从这些迁移七元组到MCTK(一种我们开发的多主体系统模型检测工具)输入语言的自动转换算法，最终通过MCTK进行验证.实验结果表明开发的算法不仅可以有效验证Web服务组合的时态逻辑规范，而且可以验证多主体系统特有的认知逻辑规范及其时态组合. 关键词 模型检测；Web服务组合；BPEL；认知逻辑；多主体系统 中图法分类号 TP301 DOI号：10.3724/SP.J.1016.2011.01041