软件学报

作者：张博闻，金钊，王捍贫，曹永知

单位：张博闻，北京大学计算机学院, 北京 100871;高可信软件技术教育部重点实验室(北京大学), 北京 10087111,金钊，北京大学计算机学院, 北京 100871;高可信软件技术教育部重点实验室(北京大学), 北京 10087102,王捍贫，北京大学计算机学院, 北京 100871;广州大学计算机科学与网络工程学院, 广东 广州 510006;高可信软件技术教育部重点实验室(北京大学), 北京 10087103,曹永知，北京大学计算机学院, 北京 100871;高可信软件技术教育部重点实验室(北京大学), 北京 10087104

关键词：分离逻辑;交互式定理证明器;块云存储系统;形式化验证;Coq

基金：国家科技攻关计划(2018YFB1003904,2018YFC1314200);国家自然科学基金(61772035,61972005,61932001)

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

来源：2022年第6期

《软件学报》期刊编辑部

查看软件学报杂志2022年第6期