中文摘要：

传统的模型检测技术无法描述系统的认知逻辑特性，而在分布式系统领域，系统和协议的规范适合用多智能体时态认知逻辑来描述．组合Web服务是典型的分布式系统．为了保证组合Web服务运行的正确性，把组合Web服务看成多智能体系统。将其建模成一组相互通信的时间自动机．采用时态认知逻辑模型检测工具Vedcs对该组合Web服务的可用性、可靠性和时效性的时态认知逻辑特性进行检测．本文以旅游预订系统组合Web服务为例，阐述了上述过程．

英文摘要：

The traditional model checking techniques cart not describe the epistemic logic for systems. However, for distributed systems, the multi-agent temporal epistemic logics are suitable to express the desired properties of systems and protocols. The Web services composition is a typical kind of distributed systems. In order to guarantee the correctness of Web services, we first regard a Web services composition as a multi-agent system and translate the system description into a network of timed automata. We then apply Verics, a model checker for timed and multi-agent systems, to the verification of the usability, reliability and time-efficiency of Web services compositions, via temporal epistemic logic. To illustrate the effectiveness of the proposed method, we model a particular case study of a travel reservation system and check the related properties.