论文部分内容阅读
内存管理系统位于操作系统内核的最底层,为上层提供内存分配和回收机制.在航天器这类安全攸关的关键系统中,其可靠性和安全性至关重要,必须要考虑到强实时性、有限空间限制、高分配效率以及各种边界条件约束.因此,系统通常采用较为复杂的数据结构和算法来管理内存空间,同时需要采用非常严格的形式化方法来保证航天器这类安全攸关系统的高可信性.对复杂内存管理系统的形式化验证也会比之前的验证工作带来更多难题,主要体现在:内存管理模块中的复杂数据结构的形式化描述,操作的规范语义,行为的建模,内部函数的规范及断言定义与循环不变式的定义,实时性验证等方面.针对这些问题,深入分析实际的航天器操作系统内存管理系统的特性;探索基于分层迭代的语义描述与验证的一般性方法与理论,并应用这些理论方法来验证一个具有实际应用的航天嵌入式操作系统的内存管理系统.该研究成果有望直接应用于我国新一代的航天器系统.
The memory management system is located at the very bottom of the operating system kernel, providing memory allocation and recovery mechanisms for the upper layers.In reliability and security of critical systems critical to safety such as spacecraft, reliability and security are paramount and must be considered with strong real-time , Limited space constraints, high allocation efficiency and a variety of boundary conditions constraints.So, the system usually uses more complex data structures and algorithms to manage memory space, at the same time require a very strict formal method to ensure that such spacecraft safety-related System’s high reliability.The formal verification of complex memory management system will bring more problems than the previous verification work, mainly reflected in: the formal description of the complex data structure in the memory management module, the normative semantics of the operation , The modeling of behavior, the specification of internal function, the definition of assertion and the definition of circular invariant and the verification of real-time etc.Aiming at these problems, this paper deeply analyzes the characteristics of the actual spacecraft operating system memory management system, Semantic description and verification of the general methods and theories, and application of these theoretical methods to verify a practical application Day embedded operating system’s memory management system. The research results are expected to be directly applied to the new generation of spacecraft systems.