基于锁保证条件扩展并发分离逻辑的并发文件系统形式化验证

郑新民; 李明树; 杨秋松; 李文波

doi:10.11959/j.issn.1000-436x.2025201

您当前的位置：

首页 >

文章列表页 >

基于锁保证条件扩展并发分离逻辑的并发文件系统形式化验证

学术论文 | 更新时间：2025-12-25

- 基于锁保证条件扩展并发分离逻辑的并发文件系统形式化验证
- Formal verification of a concurrent file system based on lock guarantee conditions extended concurrent separation logic
- “在文件系统领域，专家通过扩展并发分离逻辑，精确描述文件系统调用执行性质，验证了并发文件系统的正确性，提升了并发度和性能表现。”
- 通信学报 2025年46卷第11期页码：233-243
- 作者机构：
  
  1.基础软件国家工程研究中心（中国科学院软件研究所），北京 100190
  2.中国科学院大学，北京 100049
- 作者简介：
  
  [ "郑新民（1989- ），男，黑龙江齐齐哈尔人，中国科学院大学博士生，主要研究方向为操作系统、形式化验证。" ]
  [ "李明树（1966- ），男，吉林德惠人，博士，中国科学院软件研究所研究员、博士生导师，主要研究方向为操作系统深度设计、可信软件过程、基础软硬件核心技术与应用等。" ]
  [ "杨秋松（1977- ），男，河北沧州人，博士，中国科学院软件研究所研究员、博士生导师，主要研究方向为软件工程、形式化方法、模型检测、安全操作系统等。" ]
  [ "李文波（1975- ），男，内蒙古临河人，博士，中国科学院软件研究所副研究员，主要研究方向为操作系统深度设计、软硬件深度协同等。" ]
- 基金信息：
- DOI：10.11959/j.issn.1000-436x.2025201
  中图分类号： TP311
- 收稿：2025-02-25，
  
  修回：2025-11-07，
  
  录用：2025-11-10，
  
  纸质出版：2025-11-25
- 稿件说明：
移动端阅览
郑新民,李明树,杨秋松等.基于锁保证条件扩展并发分离逻辑的并发文件系统形式化验证[J].通信学报,2025,46(11):233-243.

ZHENG Xinmin,LI Mingshu,YANG Qiusong,et al.Formal verification of a concurrent file system based on lock guarantee conditions extended concurrent separation logic[J].Journal on Communications,2025,46(11):233-243.
郑新民,李明树,杨秋松等.基于锁保证条件扩展并发分离逻辑的并发文件系统形式化验证[J].通信学报,2025,46(11):233-243. DOI： 10.11959/j.issn.1000-436x.2025201.

ZHENG Xinmin,LI Mingshu,YANG Qiusong,et al.Formal verification of a concurrent file system based on lock guarantee conditions extended concurrent separation logic[J].Journal on Communications,2025,46(11):233-243. DOI： 10.11959/j.issn.1000-436x.2025201.

浏览量

下载量

CSCD

文章被引用时，请邮件提醒。

提交

工具集

关联资源

拟态路由器BGP代理的设计实现与形式化验证

安全计算机通信管理机制的形式化验证与实现

无文件系统嵌入式固件后门检测

基于锁保证条件扩展并发分离逻辑的并发文件系统形式化验证

Formal verification of a concurrent file system based on lock guarantee conditions extended concurrent separation logic

DOI：10.11959/j.issn.1000-436x.2025201