航天器嵌入式操作系统内存管理系统的形式化建模及验证研究

In the safety-critical system of spacecraft, memory management system is the essential part of operating system kernels which provides the allocation and free mechanism at the lowest level and is obviously critical to the reliability and safety of the spacecraft computer systems.The memory management system should satisfy hard real-time,limited space usage,efficient allocation and many boundary condition constraints。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 high reliable,the formal verification will also be much more complicated which is embodded in the formal verification of complex data structures like 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 research will deeply analyze these problems and characteristics of spacecraft memory management system to find some general method and theory based on hierachical iteration for verifying a concrete operating system used on spacecraft. The achievements of this research is believed to improve the reliability of the spacecrafts of China.

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

在航天器这类安全攸关的关键系统中，内存管理系统位于操作系统内核的最底层，为上层提供内存分配和回收机制。其可靠性和安全性至关重要，必须要考虑到强实时性、有限空间限制、高分配效率以及各种边界条件约束。因此，系统通常采用较为复杂的数据结构和算法来管理内存空间，同时需要采用非常严格的形式化方法来保证航天器这类安全攸关系统的高可信性。针对基于TLSF算法的动态内存管理系统形式化验证中复杂数据结构的形式化描述，操作的规范语义，行为的建模，内部函数的规范及断言定义与循环不变式的定义，实时性验证等方面的问题开展形式化验证工作：.1）内存管理的分阶段、分层次、自上而下的形式化建模; .2）内存管理模块的正确性要求及性质的形式化描述;.3）内存管理模块的内部不变式的形式化描述;.4）内存管理模块设计与实现的验证方法;.主要成果如下：.1）以国家航天重大专项需求为背景，深入分析实际的航天器操作系统TLSF内存管理系统的特性；探索基于分层迭代的语义描述与验证的一般性方法与理论；.2）提出了分阶段、分层次、自上而下循环迭代的操作系统形式化验证方法。在需求、设计和代码等不同抽象层次构造内存管理系统行为模型，形式化定义系统规范和关键性质；.3）利用该方法基于EventB开展了SpaceOS内存管理的形式化验证，解决了内存管理系统对强实时性、有限空间限制、高分配效率以及各种边界条件约束问题，验证了实际航天器系统中应用的SpaceOS内存管理系统在需求、设计和实现三个阶段的正确性和一致性；并在Rodin 平台对模型进行形式化推理和证明，确认需求的正确性。验证发现了3个内存错误。 . 本项目是从验证理论和方法的角度探索保障航天器操作系统可信性的新机制，从而从根本上提高系统可靠性，相关成果可为我国航天器的研制提供重要技术储备和支撑。本课题研究成果有望被直接应用于我国新一代的航天器控制系统上。