面向安全关键内存管理系统分层验证方法

安全关键系统的失败会造成很严重的后果,确保其正确性非常重要.空间嵌入式操作系统是一个典型的安全关键系统,在其内存管理的设计上,必须保障其高效的分配与回收,同时对系统资源的占用降到最低.在传统的软件开发过程中,通常是在整个软件开发结束后再进行集中测试及验证,这样势必会造成开发进展的不确定性.因此,将形式化验证方法和软件工程领域内的“需求-设计-实现”的3层开发框架相结合,通过性质分层传递验证的方法,保证了各个层次间的一致性.首先,从需求层面的需求分析开始,引入形式化证明的思路,证明对需求层逻辑的正确性,从而可以更好地指导程序的设计.其次,在设计层面的验证可以极大地减少开发代码的错误率,证明设计算法和需要实现的函数之间调用逻辑的正确性.最后,在实现层,证明所实现代码与函数设计的一致性,并且证明代码实现的正确性.使用交互式定理证明辅助工具Coq,以某一国产空间嵌入式操作系统的内存管理模块为例,证明了其内存管理算法的正确性以及需求、设计、实现的一致性.

Verification Method of Hierarchical for Safety-critical Memory Management Systems

The failure of a safety-critical system can cause serious consequences, and it is very important to ensure its correctness. The space embedded operating system is a typical safety-critical system. In the design of its memory management, it must ensure its efficient allocation and deallocation, and the occupancy of system resources is minimizedat the same time. In the traditional software development process, centralized testing and verification are usually carried out after the entire software development is completed, which will inevitably cause uncertaindevelopment. Therefore, this study combines the formal verification method with the three-tier development framework of "demand-design-implementation" in the field of software engineering, and ensures the consistency of each level through the method of layered transfer verification. First, starting from the demand analysis of the demand level, the idea of formal proof is introduced to prove the correctness of the logic of the demand level, which can better guide the design of the program. Second, verification at the design level can greatly reduce the error rate of the development code, and prove the correctness of the call logic between the design algorithm and the function that needs to be implemented. Third, at the code level, it is needed to prove the consistency of the implemented code and the functional design, and prove the correctness of code. Using the interactive theorem proving auxiliary tool Coq, this study takes the memory management module of a domestic space embedded operating system as an example, to prove the correctness of the memory management algorithm and the consistency of demand, design, and code.