基于Verics的组合Web服务有界模型检测  

Bounded Model Checking Web Services Composition via Verics

作　　者：骆翔宇[1,2] 轩爱成[3] 沙宗鲁[3] 

机构地区：[1]华侨大学计算机科学与技术学院,福建厦门361024 [2]清华大学软件学院,北京100084 [3]桂林电子科技大学计算机与控制学院,广西桂林541004

出　　处：《小型微型计算机系统》2011年第3期412-415,共4页Journal of Chinese Computer Systems

基　　金：国家自然科学基金项目(9071803960763004)资助;中国博士后科学基金项目(20090450389)资助;广西青年科学基金项目(桂科青0728090)资助;广西研究生教育创新计划项目(2008105950812M424)资助

摘　　要：传统的模型检测技术无法描述系统的认知逻辑特性,而在分布式系统领域,系统和协议的规范适合用多智能体时态认知逻辑来描述.组合Web服务是典型的分布式系统.为了保证组合Web服务运行的正确性,把组合Web服务看成多智能体系统,将其建模成一组相互通信的时间自动机.采用时态认知逻辑模型检测工具Verics对该组合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.

关 键 词：有界模型检测 时态认知逻辑 WEB服务 时间自动机 Verics 

分 类 号：TP393[自动化与计算机技术—计算机应用技术]