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

来源：软件学报杂志2017年第5期北京时间：

作者：乔磊,杨孟飞,谭彦亮,蒲戈光,杨桦

单位：乔磊，北京控制工程研究所, 北京 10019011,杨孟飞，中国空间技术研究院, 北京 10009402,谭彦亮，北京控制工程研究所, 北京 10019003,蒲戈光，华东师范大学 计算机科学与软件工程学院, 上海 20006204,杨桦，北京控制工程研究所, 北京 10019005

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

关键词：航天器操作系统;内存管理;形式化验证

基金资助：国家自然科学基金（61502031，61632005）