一种基于分离逻辑的块云存储系统验证工具

作者：张博闻; 金钊; 王捍贫^*; 曹永知

来源：软件学报, 2022, 33(06): 2264-2287.

DOI：10.13328/j.cnki.jos.006581

• 分离逻辑
• 交互式定理证明器
• 块云存储系统
• 形式化验证
• Coq

云存储技术目前被广泛应用于人们的生产与生活中.验证云存储系统中管理程序的正确性,能够有效地提高整个系统的可靠性.块云存储系统(CBS)具有最接近底层的存储架构.运用交互式定理证明器Coq,实现了一种辅助验证工具,用于分析和验证CBS中管理程序的正确性.基于分离逻辑的思想,对工具中证明系统的实现主要包括:首先,将CBS抽象为两层堆结构,定义建模语言形式化表示CBS的状态和管理程序;其次,定义描述CBS状态性质的堆谓词,并说明堆谓词间的逻辑关系;最后,定义描述程序行为的CBS分离逻辑三元组,以及制定验证三元组所需的推理规则.此外,还引入了几个证明实例,以此展示工具对实际CBS管理程序表示和推理的能力.

• 单位
  广州大学; 北京大学