关于基于块的云存储系统的推理
计算机科学中的逻辑
2019-11-12 v2
摘要
由于大数据存储需求的海量增长，云存储系统（CSS）被提出以提升存储容量。与传统存储系统相比，CSS 具有诸多优势，如更高容量、更低成本以及更易扩展。但它们也具备更高的复杂性。为确保 CSS 的可靠性，有必要证明 CSS 管理程序的正确性。事实上，我们旨在验证基于块的云存储系统（BCSS），因为 BCSS 是最流行的 CSS。本文证明了 BCSS 中管理程序的正确性，并提出了一种基于分离逻辑的验证框架来完成证明过程。主要贡献如下：（1）构建了一个具有两层堆结构的新颖框架以反映 BCSS 的特征，并基于该框架定义了建模语言；（2）构造了基于分离逻辑的断言来描述 BCSS 的属性；（3）提出了 Hoare 风格的规范来对 BCSS 进行推理。结果表明，上述所提方法能够验证 BCSS 的正确性与可靠性。此外，所提规范在 BCSS 推理应用中是可靠的。
引用
@article{arxiv.1904.04442,
title = {Reasoning about Block-based Cloud Storage Systems},
author = {Zhao Jin and Hanpin Wang and Lei Zhang and Bowen Zhang and Kun Gao and Yongzhi Cao},
journal= {arXiv preprint arXiv:1904.04442},
year = {2019}
}