基于Event-B的航天器内存管理系统形式化验证
作者:
作者单位:

作者简介:

通讯作者:

中图分类号:

基金项目:

国家自然科学基金(61502031,61632005)


Formal Verification of Memory Management System in Spacecraft Using Event-B
Author:
Affiliation:

Fund Project:

National Natural Science Foundation of China (61502031, 61632005)

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

    内存管理系统位于操作系统内核的最底层,为上层提供内存分配和回收机制.在航天器这类安全攸关的关键系统中,其可靠性和安全性至关重要,必须要考虑到强实时性、有限空间限制、高分配效率以及各种边界条件约束.因此,系统通常采用较为复杂的数据结构和算法来管理内存空间,同时需要采用非常严格的形式化方法来保证航天器这类安全攸关系统的高可信性.对复杂内存管理系统的形式化验证也会比之前的验证工作带来更多难题,主要体现在:内存管理模块中的复杂数据结构的形式化描述,操作的规范语义,行为的建模,内部函数的规范及断言定义与循环不变式的定义,实时性验证等方面.针对这些问题,深入分析实际的航天器操作系统内存管理系统的特性;探索基于分层迭代的语义描述与验证的一般性方法与理论,并应用这些理论方法来验证一个具有实际应用的航天嵌入式操作系统的内存管理系统.该研究成果有望直接应用于我国新一代的航天器系统.

    Abstract:

    In the safety-critical system of spacecraft, memory management system is the essential part of operating system kernels to provide allocation and cleanup mechanism at the lowest level and is obviously critical to the reliability and safety of spacecraft computer systems. The memory management system should satisfy strict constraints such as real-time response, space usage limit, allocation efficiency and many boundary conditions. It has to use very complex data structures and algorithm to manage the whole memory space. In order to make the complex memory management system of spacecraft highly reliable, the formal verification of the system also becomes much more complicated as it embodies formal verification of complex data structures such as two level segregated double linked list with two level bitmaps, specification of operations, modeling on behavior, assertion definition of inner function, loop invariant definition and real-time verification. This paper provides an in-depth analysis on these problems and characteristics of spacecraft memory management system to find certain general method and theory based on hierarchical iteration for verifying a concrete operating system used on spacecraft. The results of this study offer potential benefits in improving the reliability of the spacecrafts of China.

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

乔磊,杨孟飞,谭彦亮,蒲戈光,杨桦.基于Event-B的航天器内存管理系统形式化验证.软件学报,2017,28(5):1204-1220

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

京公网安备 11040202500063号