面向安全关键内存管理系统分层验证方法
作者:
作者单位:

作者简介:

李少峰(1992-),男,博士生,主要研究领域为嵌入式操作系统,内存管理,文件系统,形式化验证;张锦坤(1993-),男,硕士,CCF专业会员,主要研究领域为嵌入式操作系统,任务管理,形式化验证;乔磊(1982-),男,博士,研究员,CCF高级会员,主要研究操作系统模型设计,任务调度策略,存储管理;马智(1994-),男,博士生,主要研究领域为嵌入式操作系统,中断管理,形式化验证;杨孟飞(1962-),男,博士,研究员,CCF高级会员,主要研究领域为空间飞行器嵌入式系统,控制系统,总体技术;刘洪标(1995-),男,博士生,主要研究领域为嵌入式操作系统,任务调度,形式化验证

通讯作者:

乔磊,E-mail:fly2moon@aliyun.com

中图分类号:

TP311

基金项目:

国家自然科学基金(61632005,62032004,61802017);中国科学院软件研究所计算机科学国家重点实验室开放课题基金(SYSKF1804)


Verification Method of Hierarchical for Safety-critical Memory Management Systems
Author:
Affiliation:

Fund Project:

  • 摘要
  • |
  • 图/表
  • |
  • 访问统计
  • |
  • 参考文献
  • |
  • 相似文献
  • |
  • 引证文献
  • |
  • 资源附件
  • |
  • 文章评论
    摘要:

    安全关键系统的失败会造成很严重的后果,确保其正确性非常重要.空间嵌入式操作系统是一个典型的安全关键系统,在其内存管理的设计上,必须保障其高效的分配与回收,同时对系统资源的占用降到最低.在传统的软件开发过程中,通常是在整个软件开发结束后再进行集中测试及验证,这样势必会造成开发进展的不确定性.因此,将形式化验证方法和软件工程领域内的“需求-设计-实现”的3层开发框架相结合,通过性质分层传递验证的方法,保证了各个层次间的一致性.首先,从需求层面的需求分析开始,引入形式化证明的思路,证明对需求层逻辑的正确性,从而可以更好地指导程序的设计.其次,在设计层面的验证可以极大地减少开发代码的错误率,证明设计算法和需要实现的函数之间调用逻辑的正确性.最后,在实现层,证明所实现代码与函数设计的一致性,并且证明代码实现的正确性.使用交互式定理证明辅助工具Coq,以某一国产空间嵌入式操作系统的内存管理模块为例,证明了其内存管理算法的正确性以及需求、设计、实现的一致性.

    Abstract:

    The failure of a safety-critical system can cause serious consequences, and it is very important to ensure its correctness. The space embedded operating system is a typical safety-critical system. In the design of its memory management, it must ensure its efficient allocation and deallocation, and the occupancy of system resources is minimizedat the same time. In the traditional software development process, centralized testing and verification are usually carried out after the entire software development is completed, which will inevitably cause uncertaindevelopment. Therefore, this study combines the formal verification method with the three-tier development framework of "demand-design-implementation" in the field of software engineering, and ensures the consistency of each level through the method of layered transfer verification. First, starting from the demand analysis of the demand level, the idea of formal proof is introduced to prove the correctness of the logic of the demand level, which can better guide the design of the program. Second, verification at the design level can greatly reduce the error rate of the development code, and prove the correctness of the call logic between the design algorithm and the function that needs to be implemented. Third, at the code level, it is needed to prove the consistency of the implemented code and the functional design, and prove the correctness of code. Using the interactive theorem proving auxiliary tool Coq, this study takes the memory management module of a domestic space embedded operating system as an example, to prove the correctness of the memory management algorithm and the consistency of demand, design, and code.

    参考文献
    相似文献
    引证文献
引用本文

李少峰,乔磊,杨孟飞,张锦坤,马智,刘洪标.面向安全关键内存管理系统分层验证方法.软件学报,2022,33(6):2312-2330

复制
分享
文章指标
  • 点击次数:
  • 下载次数:
  • HTML阅读次数:
  • 引用次数:
历史
  • 收稿日期:2021-06-06
  • 最后修改日期:2021-11-28
  • 录用日期:
  • 在线发布日期: 2022-01-28
  • 出版日期: 2022-06-06
您是第位访问者
版权所有:中国科学院软件研究所 京ICP备05046678号-3
地址:北京市海淀区中关村南四街4号,邮政编码:100190
电话:010-62562563 传真:010-62562533 Email:jos@iscas.ac.cn
技术支持:北京勤云科技发展有限公司

京公网安备 11040202500063号