典型文献
一种基于分离逻辑的块云存储系统验证工具
文献摘要：
云存储技术目前被广泛应用于人们的生产与生活中.验证云存储系统中管理程序的正确性,能够有效地提高整个系统的可靠性.块云存储系统(CBS)具有最接近底层的存储架构.运用交互式定理证明器Coq,实现了一种辅助验证工具,用于分析和验证CBS中管理程序的正确性.基于分离逻辑的思想,对工具中证明系统的实现主要包括:首先,将CBS抽象为两层堆结构,定义建模语言形式化表示CBS的状态和管理程序;其次,定义描述CBS状态性质的堆谓词,并说明堆谓词间的逻辑关系;最后,定义描述程序行为的CBS分离逻辑三元组,以及制定验证三元组所需的推理规则.此外,还引入了几个证明实例,以此展示工具对实际CBS管理程序表示和推理的能力.
文献关键词：
分离逻辑;交互式定理证明器;块云存储系统;形式化验证;Coq
中图分类号：
作者姓名：
张博闻;金钊;王捍贫;曹永知
作者机构：
北京大学 计算机学院, 北京 100871;高可信软件技术教育部重点实验室(北京大学), 北京 100871;广州大学 计算机科学与网络工程学院, 广东 广州 510006
文献出处：
引用格式：
[1]张博闻;金钊;王捍贫;曹永知-.一种基于分离逻辑的块云存储系统验证工具)[J].软件学报,2022(06):2264-2287
A类：
分离逻辑,块云存储系统,交互式定理证明器,Coq
B类：
系统验证,验证工具,云存储技术,管理程序,CBS,存储架构,辅助验证,两层,建模语言,语言形式,谓词,并说,三元组,推理规则,形式化验证
AB值：
0.187644
相似文献
机标中图分类号，由域田数据科技根据网络公开资料自动分析生成，仅供学习研究参考。
