Research on Method of Formal Design and Verification of Memory Management Based on Microkernel Architecture

QIAN Zhen-jiang; LIU Yong-jun; YAO Yu-feng; TANG Li; HUANG Hao; SONG Fang-min

doi:10.3969/j.issn.0372-2112.2017.01.035

您当前的位置：

首页 >

文章列表页 >

Research on Method of Formal Design and Verification of Memory Management Based on Microkernel Architecture

更新时间：2025-07-16

- Research on Method of Formal Design and Verification of Memory Management Based on Microkernel Architecture
- Acta Electronica Sinica Vol. 45, Issue 1, Pages: 251-256(2017)
- 作者机构：
  
  1. 南京大学计算机科学与技术系,江苏,南京,210023
  2. 常熟理工学院计算机科学与工程学院,江苏,苏州,215500
  3. 南京大学计算机科学与技术系,江苏,南京,210023
  4. 常熟理工学院计算机科学与工程学院,江苏,苏州,215500
- 作者简介：
- 基金信息：
- DOI：10.3969/j.issn.0372-2112.2017.01.035
  CLC： TP316
- Published Online：25 January 2017，
  
  Published：2017
- 稿件说明：
移动端阅览
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：

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

Views

602

下载量

CSCD

Alert me when the article has been cited

提交

Tools

Publicity Resources

VMFS: A Unified Persistent Memory Management System

Algorithms for Deriving Minimum Unsatisfiable Boolean Subformulae

Property Generation Method for Model Checking on Clock Domain Crossing Design

Model Checking on Clock Domain Crossing Design of System-on-Chip

A Multi-Protection Domains Process Model and Its Implementation

Related Author

HU Ze-rui

ZHAO Sheng

SHI Wen-jie

WANG Gang

LIU Xiao-guang

ZHANG Jia-chen

LI Si-kun

SHEN Sheng-yu

Related Institution

College of Computer Science, Nankai University

Tianjin Key Laboratory of Network and Data Security Technology

School of Computer Science,National University of Defense Technology

Micro-Processor Research and Development Center,Peking University

State Key Laboratory for Novel Software TechnologyNanjing UniversityNanjingJiangsu 210093China

⁰