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

Model Checking Web Services Based on Temporal Logic of Knowledge

传统模型检测技术主要采用时态逻辑描述被验证的规范,人们较少注意多智能体认知逻辑的模型检测问题。而在分布式系统领域,系统和协议的规范很适合用认知逻辑来描述。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.