| 基于Event-B的航天器内存管理系统形式化验证 |
| |
| 作者姓名： | 乔磊 杨孟飞 谭彦亮 蒲戈光 杨桦 |
| |
| 作者单位： | 北京控制工程研究所, 北京 100190,中国空间技术研究院, 北京 100094,北京控制工程研究所, 北京 100190,华东师范大学, 上海 200062,北京控制工程研究所, 北京 100190 |
| |
| 基金项目： | 国家自然科学基金（61502031,61632005） |
| |
| 摘 要： | 内存管理系统位于操作系统内核的最底层,为上层提供内存分配和回收机制.在航天器这类安全攸关的关键系统中,其可靠性和安全性至关重要,必须要考虑到强实时性、有限空间限制、高分配效率以及各种边界条件约束.因此,系统通常采用较为复杂的数据结构和算法来管理内存空间,同时需要采用非常严格的形式化方法来保证航天器这类安全攸关系统的高可信性.对复杂内存管理系统的形式化验证也会较之前的验证工作带来更多难题,主要体现在：内存管理模块中的复杂数据结构的形式化描述;操作的规范语义;行为的建模;内部函数的规范及断言定义与循环不变式的定义;实时性验证等方面.本文拟针对这些问题,深入分析实际的航天器操作系统内存管理系统的特性;探索基于分层迭代的语义描述与验证的一般性方法与理论,并应用这些理论方法,来验证一个具有实际应用的航天嵌入式操作系统的内存管理系统.本文研究成果有望被直接应用于我国新一代的航天器系统上.
|
| 关 键 词： | 航天器操作系统 内存管理 形式化验证 |
| 收稿时间： | 2016-08-30 |
| 修稿时间： | 2016-09-25 |
|
| 点击此处可从《软件学报》浏览原始摘要信息 |
|
点击此处可从《软件学报》下载全文 |
|
