由于 Web服务及其协同的动态性、开放多变的互联网运行环境以及松耦合的服务开发模式,所导致的开发和运行过程的不确定性,使得 Web服务组合的正确性和可靠性等可信性质难以得到保证。因此,形式化分析和验证 Web服务组合的研究也越来越受到重视。当前针对 Web服务的模型检测方法和工具还比较少,建模与验证环节均需手工处理,因此验证过程自动化程度较低;另外,Web服务组合可视为一种典型的多智能体系统,因此验证多智能体系统特有的知识与合作等性质也具有重要意义。　　为了提高Web服务组合的形式化建模的自动化程度,支持对知识、合作等Web服务认知状态及其时态演变等性质的验证,本文以多智能体系统模型检测工具MCMAS底层验证平台,设计并实现了Web服务组合的自动验证原型系统MCWS。首先,用BPEL状态迁移系统对业务流程执行语言BPEL进行形式化建模,给出基本活动、结构化活动、错误处理和补偿处理的的形式语义;然后,提出自动验证 Web服务组合的MCWS系统架构,设计并实现了BPEL向状态迁移系统自动转化的主要算法B2S,以及状态迁移系统向ISPL代码自动转换的主要算法S2I,并对BPEL中的死路删除机制进行了详细描述;最后,应用MCWS对贷款服务和雇员出差服务两个实例的时序认知及合作等性质进行了分析和验证,显示了MCWS的有效性。