A Verification Approach for Web Service Compositions Based on Epistemic Model Checking

近几年Web服务组合的形式化验证逐渐成为研究热点.模型检测作为形式化验证的一种主流技术,可以克服传统软件测试用例生成不完备的不足,同时具有验证自动化的优点.该文提出并实现了一种Web服务组合的认知模型检测方法,将Web服务组合建模为多主体系统,在分析BPEL语言控制流程基础上,提出BPEL活动的形式化模型,给出活动执行语义.进而以迁移七元组为中间形式,开发从BPEL流程到迁移七元组集合以及从这些迁移七元组到MCTK(一种我们开发的多主体系统模型检测工具)输入语言的自动转换算法,最终通过MCTK进行验证.实验结果表明开发的算法不仅可以有效验证Web服务组合的时态逻辑规范,而且可以验证多主体系统特有的认知逻辑规范及其时态组合.国家"九七三"重点基础研究发展规划项目基金; 家杰出青年科学基金; 国家自然科学基金; 中国博士后科学基金; 华侨大学中央高校基本科研业务费项目; 华侨大学高层次人才科研启动费项目中文核心期刊要目总览(PKU)中国科技核心期刊(ISTIC)中国科学引文数据库(CSCD)061041-10613