基于智能体理论的Web服务系统的建模与形式化验证研究

本项目从分布式系统设计中的规范表示及其形式化验证的需要出发，把Web服务中的各种服务（特征）以及这些软件系统中的各种角色视为自治智能体(agent)，他们在开放的环境中发生交互，形成多智能体系统(Multi-Agent System)。为了能严格地自动化验证其可靠性和安全性等特征规范，这种多智能体系统将被形式化为多智能体Kripke语义模型，本项目将在该Kripke语义模型上提出相应的规范描述逻辑及其语义框架，最后设计相应的高效的符号化模型检测算法(基于OBDDs和基于SAT)。 而且项目在研究上述符号化模型检测技术基础上，根据被验证问题的结构和被验证的规范，采用各种技术优化这些符号化模型检测算法，探索最优的布尔编码策略和组合化验证策略，提高Web服务验证的效率和规模。

项目旨在把Web服务组件形式化为多智能体系统(Multi-Agent Systems)，利用多智能体系统的模型，方法和工具来对Web服务进行建模和验证。 经过三年的研究探索，项目一方面应用了现有的著名的智能体逻辑语言和工具，如认知逻辑和BDI逻辑，直接对Web服务进行了建模验证，如对Web服务的协议的验证；另一方面也提出了新的智能体逻辑语言模型，如描述层次多智能体(Hierarchical Multi-Agent Systems)的逻辑语言，以及描述协作交互行为的新的动态协同逻辑语言。由于所有的验证算法最终归结于BDD (Binary Decision Diagram)和SAT (Satisfiability)两种符号化计算工具，因此项目的另一条主线是着重研究和开发了高效的BDD软件包和SAT求解器， 通过这些自主开发的高效符号化计算工具，从而推动整个验证规模和效率的提高。