基于分离逻辑的云存储管理程序正确性验证方法

Cloud computing is a new computing model, which represents the future of computer program development. As a foundation of cloud computing, cloud storage has many obvious advantages comparing with the traditional storage system, and is rapidly developing in recent years. In order to improve the reliability and safety of cloud storage service, the correctness of the cloud storage management program needs to be verified, which is an urgent problem to solve. While the special characteristics of the cloud storage system make the problem challenging. The main research work of this project includes: firstly, Modeling existed cloud storage architecture. Secondly, based on the above model, an abstract management language is defined, and its semantic definition is raised. Thirdly, propose a method (assertion formula) to describe the property of cloud storage management system and its semantics. Lastly, in joint work with the management language and assertion formulas, the Hoare triple deduction system is constructed, and the correctness of the cloud storage management program is verified. The research can promote the standardization of cloud storage technology, improve the quality of cloud storage service, save the cost of cloud storage research and development, and encourage the development of formal method research. It is important significance for the academic progress, as well as the national economic and social development.

云计算作为一种新兴的计算模型，代表了计算领域未来的发展方向。而云存储作为云计算的基础之一，与传统存储系统相比有着显而易见的优势，在近年来得到了迅速的发展。为提高云存储服务的可靠性和安全性，需要对云存储系统管理程序进行正确性验证，这是一个亟待解决的问题，云存储系统的特殊特点也导致该问题具有挑战性。本项目拟主要研究：1.对现有的云存储系统架构进行抽象建模；2.在上述模型基础上构造抽象管理语言，并研究其语义定义方法；3.管理系统的性质描述方法（断言公式）及其语义；4.结合上述管理语言和断言公式，构建出Hoare型三元组推导系统，最终实现对云存储系统管理程序进行正确性验证。研究云存储管理语言的正确性验证，可以促进云存储技术的标准化，提升云存储服务的质量，节约云存储研发成本，并可以促进形式化方法的研究发展，对学术的进步及国民经济和社会的发展都有着重要意义。

随着云存储系统在众多领域上的作用越来越重要，人们有必要对云存储系统的管理程序进行相应的正确性验证，以提高云存储系统相关数据服务的可靠性。本项目基于分离逻辑为理论基础，针对待证目标构建出了一个新的形式化逻辑系统，其中包含了以下几方面的工作：1. 抽象云存储系统的架构，提炼出以数据块为基本单位对文件内容进行拆分，将每个数据块独立地存放在数据节点中，进而实现对超大规模数据集的部署方式；2. 建立一种描述云存储系统管理的形式化建模语言，包含对文件和数据块在内的数据结构及相应的操作命令给出语法规则，并对云存储系统管理程序的状态进行定义；3. 构造一种能够同时处理原始地址和块地址的断言语言，包含对之前逻辑系统中断言的扩展，用以描述原始地址属性，并且新定义用于描述数据块属性的块断言，这两种断言能够分别描述云存储系统的一些性质，但是彼此之间又是相互独立的，本项目通过将上述两种断言以恰当的方式进行组合，形成了一个用于描述云存储系统完整属性的全局断言；4. 定义用于形式推理云存储系统的规范规则，通过采用与分离逻辑类似的方式，即霍尔三元组的形式，将全局断言限定在前置条件与后置条件中，本项目以此制定了相应的公理以及规则；5. 初步验证云存储系统管理程序的正确性，包括按照逻辑系统制定的语法编写出相应的模拟程序，运用断言语言定义系统所需要满足的属性，以及运用规则来证明该程序的终止性与正确性，以此体现了逻辑系统的实用价值。本项目从形式化验证的角度对云存储可靠性所做的相关研究，较好地完成了项目合同规定的研究任务，对提高云存储系统中数据管理的可靠性，保证数据处理过程中的正确性有一定的参考价值。本项目完成论文发表和研究生培养的目标，其中几篇发表在包含Information and Computation、ICALP等国际一流的会议或期刊上。