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

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

项目编号： No.61170028

项目类型： 面上项目

立项/批准年度： 2012

项目学科： 计算机科学学科

项目作者： 骆翔宇

作者单位： 华侨大学

项目金额： 55万元

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

中文关键词： 模型检测；多智能体系统；抽象与精化；认知逻辑；Web服务

英文摘要：

英文关键词： model checking；multi-agent systems；abstraction and refinement；epistemic logic；Web services