基于高效I/O模型检测的大规模Web服务验证研究

Large-scale Web service is one of the most extensive and important applications of Internet.The verification for large-scale Web service is a new and important research area in computer security. The aim of the project is to investigate I/O efficient model checking technique for large-scale systems and thus provide an efficient approach for large-scale Web service verification. The main content is as follows: (1) Propose a new temporal logic of knowledge system which can more accurately describe the security specification of large-scale Web service; (2) Investigate the method to build model of large-scale Web service; (3) Research I/O efficient model checking techniques based on Depth-First Search and Breadth-First Search to solve the problem that model checking can not proceed because of state space explosion and memory shortage. Based on this, propose the approaches and techniques for large-scale Web service verification; (4) Based on above approaches and techniques, design and implement the tool of large-scale Web service verification by extending the famous model checking tools SPIN etc., and verify some representative large-scale Web service systems.

大规模Web服务是Internet最广泛最重要的应用之一，对大规模Web服务的验证是计算机安全方面一个非常重要的新研究领域。本项目的研究目标是研究大规模系统高效I/O模型检测技术，为大规模Web 服务的安全验证提供高效的途径。具体内容主要包括以下几方面：(1) 提出新的时态认知逻辑体系，这种逻辑体系能更加准确地描述大规模Web服务的安全属性；(2) 研究大规模Web服务的模型化方法；(3) 研究动态和静态内存管理技术, 将深度优先和宽度优先搜索技术从内存扩展到外存, 提出高效I/O模型检测技术，解决因状态空间爆炸和内存不足导致的模型检测无法进行的问题，以此为基础，形成大规模Web服务安全验证的方法和技术；(4) 以上述方法和技术为基础，通过扩展SPIN等著名模型检测工具,设计和实现大规模Web服务验证工具,并对具有代表性的大规模Web服务系统进行安全性验证。

大规模Web服务是Internet最广泛最重要的应用之一，对大规模Web服务的验证是计算机安全方面一个非常重要的新研究领域。.本项目的研究内容主要包括以下几方面：(1) 提出新的时态认知逻辑体系，这种逻辑体系能更加准确地描述大规模Web服务的安全属性；(2) 研究大规模Web服务的模型化方法；(3) 研究动态和静态内存管理技术, 提出高效I/O模型检测技术 (4)设计和实现大规模Web服务验证工具。.该项目已取得了较好的成果，共发表论文18篇，其中顶级期刊IEEE Transactions on Software Engineering (TSE)上1篇；顶级期刊Artificial Intelligence上2篇；顶级期刊IEEE Transactions on Computers上2篇；著名期刊IEEE Transactions on Very Large Scale Integration Systems、Journal of Artificial Intelligence Research和IEEE Transactions on Cybernetics上5篇；顶级会议AAAI和IJCAI上3篇。具体如下：（1）提出层次多智能体系统中完备可靠的一阶知识、信念和肯定性逻辑系统，为大规模Web服务的安全属性描述提供了更加准确的方法。（2）提出了一种大规模系统I/O高效模型检测技术。我们算法的速度大约是国际上最好的三个算法DAC, MAP和 IDDFS的三倍。为Web服务的验证提供了更加高效的方法，相关成果发表在著名刊物《IEEE Transactions on Very Large Scale Integration Systems》等期刊上。（3）首次提出基于I/O模型检测技术查找所有反例(或多反例)的高效方法。这种方法对模型检测技术以及大规模Web服务验证等方面都有重要的理论价值和应用前景。相关成果发表在顶级刊物《IEEE Transactions on Software Engineering》等期刊上。（4）在大规模Web服务验证的其他算法方面，我们已经提出了多种快速的搜索算法， 相关成果发表在顶级期刊《Artificial Intelligence》 等刊物上。