论文部分内容阅读
内存管理是操作系统的重要组成部分,一个安全可靠的内存管理程序,对于操作系统的运行十分关键.采用传统软件开发方法开发的内存管理系统,安全性和可靠性得不到很好的保证.为此提出用形式化的B方法开发内存管理系统.首先使用B方法建立了内存管理的形式化模型,利用B工具对该阶段生成的证明义务进行证明,保证系统在初始规范说明层次上的内在一致性和设计的正确性.然后根据B方法分层构造的思想对上一阶段得到的抽象规范模型进行精化.最终得到一个可实现的内存管理模型,该模型更好地保证了系统的一致性和可靠性.