基于多主体认知逻辑模型检测的Web服务组合验证

面向服务的体系架构将成为最主流的软件工程实践方法之一。由于服务及其协同的动态性、开放多变的互联网运行环境、以及松耦合的服务开发模式，使得服务的正确性、可靠性、安全性等可信性质难以得到保证。针对Web服务组合可信性质的形式化验证需求，拟开展基于多主体系统的Web服务组合形式化建模和自动模型检测技术的研发。提出新的多主体约束自动机模型，将服务抽象为主体自动机，刻画主体交互接口、主体协同机制以及组合系统的操作行为，从而将Web服务组合抽象为多主体系统。在此模型上提出新的多主体认知逻辑，融合时态、命题动态逻辑、数据流逻辑和动态认知逻辑，可对主体认知状态进行表示和推理。通过对该多主体认知逻辑的基础理论和关键技术的研究，提出基于多主体约束自动机的模型检测算法。为了大幅缓解模型检测技术的状态爆炸问题，重点考虑基于符号计算技术开发相关模型检测工具，从而在Web服务形式化建模与验证领域获得实质进展。

本项目针对Web服务组合等分布式系统的可信性质的形式化验证需求，开展了基于多智能体系统（MAS）模型检测的Web服务组合的形式建模与验证的理论、方法和工具的研究与开发。总体看，本团队已按计划完成大部分研究内容。.我们首先丰富了MAS常用的时态认知逻辑，其认知部分完整支持知识、群体知识、分布知识、公共知识、信念、愿望和意图等认知模态词的表示和推理；时态部分支持即可定性又可定量描述的实时时态逻辑RTCTL*，增强了时态表达能力；我们还将智能体联合逻辑与上述时态、认知逻辑融合起来，极大的增强了所提出逻辑的表达能力，拓宽了应用领域。.验证工具研发方面，完成了RTCTL*符号化模型检测的理论研究和工具MCTK的开发，结合前期实现的认知逻辑模型检测算法，我们实际实现了RTCTL*K的符号化模型检测工具。我们还提出了RTCTL*以及认知逻辑的图状反例表示和生成方法，提高了反例的简洁性和易读性。另外，我们还开发了一个带线性不等式和无解释函数符号的无量词一阶逻辑证明器Folp，可作为该一阶逻辑公式的SMT求解器，以及Craig插值生成器。这对提高模型检测技术的验证效率是个有效的办法。.对于Web服务的模型检测，我们提出了将多智能体系统的谓词抽象验证应用于web服务组合抽象验证与精化的方法。其中采用的验证平台是我们的MCTK。这一方法可将包含众多数据的web服务的状态空间规约到可接受的程度，大大提高验证效率。