微内核架构内存管理的形式化设计和验证方法研究

钱振江; 刘永俊; 姚宇峰; 汤力; 黄皓; 宋方敏

doi:10.3969/j.issn.0372-2112.2017.01.035

您当前的位置：

首页 >

文章列表页 >

微内核架构内存管理的形式化设计和验证方法研究

科研通信 | 更新时间：2025-07-16

- 微内核架构内存管理的形式化设计和验证方法研究
- Research on Method of Formal Design and Verification of Memory Management Based on Microkernel Architecture
- 电子学报 2017年45卷第1期页码：251-256
- 作者机构：
  
  1. 南京大学计算机科学与技术系,江苏,南京,210023
  2. 常熟理工学院计算机科学与工程学院,江苏,苏州,215500
  3. 南京大学计算机科学与技术系,江苏,南京,210023
  4. 常熟理工学院计算机科学与工程学院,江苏,苏州,215500
- 作者简介：
- 基金信息：
  
  国家自然科学基金 (No.61402057）;江苏省科技计划自然科学研究项目 (No.BK20140418）;中国博士后科学基金 (No.2015M571737）;江苏省“六大人才高峰”高层次人才项目 (No.2011-DZXX-035）;江苏省高校自然科学研究项目 (No.12KJB520001）
- DOI：10.3969/j.issn.0372-2112.2017.01.035
  中图分类号： TP316
- 网络出版：2017-01-25，
  
  纸质出版：2017
- 稿件说明：
移动端阅览
钱振江, 刘永俊, 姚宇峰, 等. 微内核架构内存管理的形式化设计和验证方法研究[J]. 电子学报, 2017,45(1):251-256.

QIAN Zhen-jiang, LIU Yong-jun, YAO Yu-feng, et al. Research on Method of Formal Design and Verification of Memory Management Based on Microkernel Architecture[J]. Acta Electronica Sinica, 2017, 45(1): 251-256.
钱振江, 刘永俊, 姚宇峰, 等. 微内核架构内存管理的形式化设计和验证方法研究[J]. 电子学报, 2017,45(1):251-256. DOI： 10.3969/j.issn.0372-2112.2017.01.035.

QIAN Zhen-jiang, LIU Yong-jun, YAO Yu-feng, et al. Research on Method of Formal Design and Verification of Memory Management Based on Microkernel Architecture[J]. Acta Electronica Sinica, 2017, 45(1): 251-256. DOI： 10.3969/j.issn.0372-2112.2017.01.035.

摘要

由于巨大的规模和复杂性，操作系统的设计和实现的正确性很难用传统的定量方法来描述.本文阐述对微内核操作系统的形式化设计和验证的方法.在汇编层利用非确定性自动机对系统进行形式化建模，并使用Hoare三元组描述模块接口函数的前后置条件，作为函数正确性的定义.以实现的VSOS（Verified Secure Operating System）内存管理模块为例，在Isabelle/HOL定理证明器环境中对建立的内存管理模型和系统行为的操作语义进行形式化描述，并对内存管理模块的设计和实现的正确性进行验证.结果表明，这一方法是可行的和高效的.

Abstract

The correctness of design and implementation of operating systems is difficult to be described with the traditional quantitative methods

because of the enormous size and complexity.This paper illustrates our method of formal design and verification of microkernel operating system.We construct the system model with the non-deterministic automaton in the assembly level

and use the Hoare triples to describe the previous and post conditions of the interface functions

as the definitions of function correctness.We take the module of memory management in the self-implemented VSOS (Verified Secure Operating System) as an example

to illustrate our formal method.Meanwhile

we formally describe the constructed memory management model and operation semantics of system behaviors in the Isabelle/HOL theorem prover

and verify the correctness of design and implementation of the memory management.The result shows that the method proposed is feasible and efficient.

关键词

Keywords

references

浏览量

602

下载量

CSCD

文章被引用时，请邮件提醒。

提交

工具集

关联资源

VMFS: 一种持久性内存统一管理系统

最小布尔不可满足子式的求解算法

面向模型检验的跨时钟域设计电路特性生成方法

面向SoC系统芯片中跨时钟域设计的模型检验方法

多保护域进程模型及其实现