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

• 作者: 乔磊 杨孟飞 杨桦 蒲戈光 谭彦亮
• 来源期刊: 软件学报
• 学科: 工学
• 关键词: 航天器操作系统 内存管理 形式化验证
• 年，卷（期）: 2017,（5）
• 所属期刊栏目: 形式化方法与应用专题
• 页码范围: 1204-1220
• 页数: 17页
• 分类号: TP311
• 字数: 12634字
• 语种: 中文
• DOI: 10.13328/j.cnki.jos.005218

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	杨孟飞		45	222	10.0	12.0
2	谭彦亮		4	15	2.0	3.0
3	杨桦		12	34	4.0	5.0
4	乔磊		17	39	4.0	5.0
5	蒲戈光	华东师范大学计算机科学与软件工程学院	7	27	3.0	5.0