中文摘要：

近几年Web服务组合的形式化验证逐渐成为研究热点．模型检测作为形式化验证的一种主流技术，可以克服传统软件测试用例生成不完备的不足，同时具有验证自动化的优点．该文提出并实现了一种Web服务组合的认知模型检测方法，将Web服务组合建模为多主体系统，在分析BPEL语言控制流程基础上，提出BPEL活动的形式化模型，给出活动执行语义．进而以迁移七元组为中间形式，开发从BPEL流程到迁移七元组集合以及从这些迁移七元组到MCTK（一种我们开发的多主体系统模型检测工具）输入语言的自动转换算法，最终通过MCTK进行验证．实验结果表明开发的算法不仅可以有效验证Web服务组合的时态逻辑规范，而且可以验证多主体系统特有的认知逻辑规范及其时态组合．

英文摘要：

In recent years, the formal verification of Web service compositions is gradually becoming a hot research area. As a mainstream technique for formal verification, model checking is able to not only overcome the shortcoming of traditional software test techniques that they cannot generate the complete set of test cases, but also automatizes the verification process. In this paper, the authors propose and implement an epistemic model checking approach for the verification of Web service compositions by modeling them as multi-agent systems. After analyzing the BPEL control flow, the authors first propose a formal model for the BPEL activities and give the semantics of the implementation of the BPEL activities. By taking the so-call transition seven-tuple as the intermediate form, the authors further develop two automatic transform algorithms, one converts the BPEL process to the set of seven-tuples and the other converts this set of seven-tuples to the input language of MCTK （a model checker for multi-agent systems developed by the authors）, such that can finally implement the verification by MCTK. The experimental results show that the proposed algorithms can effectively verify not only the temporal logical specifica- tions, but also the temporal epistemic logical specifications, which are proper to multi-agent systems.