摘要
数据的快速增长限制了传统存储技术存储和管理数据的能力,云存储系统应运而生.云存储系统最重要的特征是数据以块的形式存储,且每个块被视为一个独立的存储单元.因此,云存储系统通常包含两种存储单元:原始地址和块地址,这使得云存储系统与传统内存系统相比有着显著的不同.从而,如何保证云存储系统的可靠性成为了有待解决的难题.本文基于分离逻辑提出了一种系统方法来验证云存储系统管理程序的正确性.主要贡献包括:(1)提出了一种建模语言来描述云存储管理;(2)扩展了分离逻辑的断言语言来描述云存储系统中有关块的属性;(3)在上述两个语言的基础上,提出了一套霍尔型的规范规则对云存储系统进行推理.规范的前置和后置条件都以断言对的形式给出.运用这些方法,能够验证云存储管理程序的正确性.
The rapid growth of data has restricted the capability of traditional storage technologies to store and manage data.Massive growth in big data generated through Cloud Storage Systems(CSSs)has been observed.Compared with traditional storage systems,CSSs have lots of advantages,such as higher capacity,lower cost,and easier scalability.An important feature of CSSs is that data files are stored in a way of block.That is,the storage resources of CSSs consist of small block spaces with a fixed size.When storing a data file,the system may fist cut the file into some segments,and then put these segments into proper blocks,taking every segment as a whole.Hence,CSSs usually have two kinds of storage units:ordinary locations and block locations.At first glance,the above procedure of saving a file into blocks in a CSS looks similar to that of saving values into memory cells in a memory management system.But there are still some substantial differences.When user submit their data file to CSSs,the file of user uploaded is divided into lots of 128 MB segments firstly(the last segment may be less than the others).Then the system allocate those segments to the blocks one by one,and the size of each block is also 128 MB.Finally,the system will generate a file table to record the block addresses and the relation between file segments and blocks.These characteristics make the properties of CSS management very different from those of traditional memory management.Although the concept of block storage has been proposed for many years,it becomes more complicated in CSSs.In order to improve the reliability and safety of cloud storage service,the correctness of the cloud storage management problem needs to be verified,which is an urgent problem to solve.While the special characteristics of the cloud storage system make the problem challenging.Then how do we appeal formal methods to model,describe and reason about CSSs?Separation Logic(SL),which is a Hoare-style logic,has a strong theoretical and practical significance.By using SL,some ve
作者
金钊
王捍贫
张博闻
张磊
曹永知
JIN Zhao;WANG Han-Pin;ZHANG Bo-Wen;ZHANG Lei;CAO Yong-Zhi(Department of Computer Science and Technology,Peking University,Beijing 100871;School of Computer Science and Cyber Engineering,Guangzhou University,Guangzhou 510006;Key Laboratory of High Confidence Software Technologies(MOE),Peking University,Beijing 100871)
出处
《计算机学报》
EI
CSCD
北大核心
2020年第12期2227-2240,共14页
Chinese Journal of Computers
基金
国家自然科学基金(61772035,61972005,61932001)
国家科技攻关计划(2018YFB1003904,2018YFC1314200)资助.
关键词
分离逻辑
霍尔逻辑
云存储系统
建模语言
形式验证
separation logic
Hoare logic
cloud storage systems
modeling language
formal verification
