基于分离逻辑的云存储系统验证

摘要：

数据的快速增长限制了传统存储技术存储和管理数据的能力,云存储系统应运而生.云存储系统最重要的特征是数据以块的形式存储,且每个块被视为一个独立的存储单元.因此,云存储系统通常包含两种存储单元:原始地址和块地址,这使得云存储系统与传统内存系统相比有着显著的不同.从而,如何保证云存储系统的可靠性成为了有待解决的难题.本文基于分离逻辑提出了一种系统方法来验证云存储系统管理程序的正确性.主要贡献包括:(1)提出了一种建模语言来描述云存储管理;(2)扩展了分离逻辑的断言语言来描述云存储系统中有关块的属性;(3)在上述两个语言的基础上,提出了一套霍尔型的规范规则对云存储系统进行推理.规范的前置和后置条件都以断言对的形式给出.运用这些方法,能够验证云存储管理程序的正确性.

关键词：分离逻辑、霍尔逻辑、云存储系统、建模语言、形式验证

所属期刊栏目：43

分类号：TP311(计算技术、计算机技术)

资助基金：本课题得到国家自然科学基金;国家科技攻关计划

在线出版日期：2020-12-23（万方平台首次上网日期，不代表论文的发表时间）

页数：共14页

页码：2227-2240