基于时态认知逻辑的Web服务模型检测  

Model Checking Web Services Based on Temporal Logic of Knowledge

作　　者：骆翔宇[1] 陈艳[1] 古天龙[1] 董荣胜[1] 

机构地区：[1]桂林电子科技大学计算机与控制学院,桂林541004

出　　处：《计算机科学》2009年第8期153-157,共5页Computer Science

基　　金：国家自然科学基金(60763004);广西青年科学基金(桂科青0728090);广西研究生教育创新计划项目(2007105950811m19)资助

摘　　要：传统模型检测技术主要采用时态逻辑描述被验证的规范,人们较少注意多智能体认知逻辑的模型检测问题。而在分布式系统领域,系统和协议的规范很适合用认知逻辑来描述。Web服务是一个典型的分布式系统。把Web服务组合建模为多智能体系统,并成功采用我们实现的时态认知逻辑符号模型检测工具MCTK验证了SAS股票分析服务实例。同时采用WSAT,WS-Engineer和SPIN 3个模型检测工具在相同实验环境下验证了该实例,实验结果表明我们的Web服务模型检测方法不仅比这3个模型检测工具更高效,而且支持认知逻辑规范的验证,这是这3个模型检测工具所不具备的。Model checking has being used mainly to check if a system satisfies the specifications expressed in temporal logic. People pay little attention to the model checking problem for multi-agent logics of knowledge. However, in the distributed systems community, the desirable specifications of systems and protocols have been expressed widely in logics of knowledge. A Web service is an abstract notion that must be implemented by a concrete agent. The agent is the concrete piece of software or hardware that sends and receives messages. Thus a Web services composition can be viewed as a multi-agent system. We applied our model checker MCTK for temporal logic of knowledge to verified the Web services example of the SAS protocol. We also verified the example with three model checkers WSAT,WS-Engineer and SPIN. The experimental results show that the performance of our model checking method for verifying Web services is higher than these three model checkers.

关 键 词：模型检测 时态认知逻辑 多智能体系统 WEB服务 

分 类 号：TP301[自动化与计算机技术—计算机系统结构]