互联网的开放性使得Web服务是分布式的,在Web服务交互过程中,一些“不正常”的消息交互会影响Web服务的质量和健壮性,降低用户满意度,甚至破坏正常的服务过程,因此,验证Web服务的安全性和可靠性很有必要。模型检测技术由于其自动化程度高,已经在Web服务的形式化验证中得到了成功的应用,模型检测技术是很好的验证Web服务可靠性和安全性的方法。传统模型检测技术主要采用时态逻辑描述被验证的规范,人们较少注意认知逻辑的模型检测问题。因而传统模型检测技术不能检测知识的相关属性,也不能有效的保证系统的可靠性和安全性;而时态认知逻辑模型检测技术可以很好的验证知识属性,并更好的保证系统的可靠性和安全性。因此,论文采用时态认知逻辑的模型检验技术来验证Web服务这一当前的研究热点问题。本文用时态认知逻辑模型检测技术对Web服务组合问题和特征交互问题进行了形式化验证。据我们所知,目前,国内外还没有用时态认知逻辑模型检测技术对Web服务的特征交互问题进行验证的相关报道。论文提出了从Web服务的描述语言BPEL到本文的模型检测工具(MCTK)的形式化验证框架,给出了从Web服务的过程描述模型(BPEL)到形式化模型(有限状态机模型)的转换框架,这将使得Web服务的形式化验证工作更加自动化。并且本论文把时态认知逻辑模型检测技术扩展应用到了安全领域,对安全协议进行了形式化验证,并发现了其中的漏洞。本文取得的一些研究成果如下:(1)提出了用时态认知逻辑模型检测技术对Web服务组合问题进行形式化验证的方法。用本文的时态认知逻辑模型检测工具MCTK对Web服务的组合问题进行了分析和验证,分析了Web服务流程的正确性,并且能够检测传统模型检测工具无法检测的知识逻辑属性,同时与其它模型检测工具进行了比较,证明了本文工具的正确性和高效性。(2)首次用时态认知逻辑模型检测技术对Web服务的特征交互问题进行了形式化验证。用MCTK对在线股票交易系统服务STS协议的特征交互问题进行了分析和验证,发现了STS协议中的特征冲突现象,验证了STS协议的特征冲突属性。(3)提出了从Web服务的描述语言BPEL到本文的模型检测工具(MCTK)的形式化验证框架。给出了从Web服务的过程描述模型(BPEL)到形式化模型(有限状态机模型)的转换框架,这将使得Web服务的形式化验证工作更加自动化。(4)用时态认知逻辑模型检测技术对安全协议进行了形式化验证。用MCTK对经典的Needham-Schroeder协议进行了分析和验证,找到了该协议的漏洞,并且与其它工具进行了比较,证明了本文工具的优越性和可扩展性。