| 微内核架构文件系统的形式化设计与验证方法研究 |
| |
| 引用本文： | 钱振江,唐洪英,李康杰,黄皓,宋方敏.微内核架构文件系统的形式化设计与验证方法研究[J].小型微型计算机系统,2013,34(10). |
| |
| 作者姓名： | 钱振江 唐洪英 李康杰 黄皓 宋方敏 |
| |
| 作者单位： | 1. 常熟理工学院计算机科学与工程学院,江苏苏州215500;南京大学软件新技术国家重点实验室,南京210046;南京大学计算机科学与技术系,南京210046;伦敦大学国王学院,英国伦敦WC2R 2LS
2. 南京大学软件新技术国家重点实验室,南京210046;南京大学计算机科学与技术系,南京210046 |
| |
| 基金项目： | 国家"八六三"高技术研究发展计划项目，国家自然科学基金创新研究群体基金项目，江苏省"六大人才高峰"高层次人才项目，江苏省高校自然科学基金项目 |
| |
| 摘 要： | 文件系统作为数据存储和管理的功能模块,其正确性是操作系统安全性的重要方面.采用形式化方法对微内核架构文件系统进行设计,使用操作系统对象语义模型(OSOSM)框架提出微内核架构文件系统的状态自动机模型,并依此描述系统调用的功能语义和系统状态转换,分析和归纳文件系统的功能正确性断言.以实现的微内核安全操作系统(Verified Trusted Oper-ating System,VTOS)为例,阐述在Isabelle/HOL定理证明器环境中构建状态自动机模型的方法,并对VTOS文件系统的形式化设计和功能正确性断言进行一致性验证,结果显示,VTOS文件系统的设计和实现符合预期的正确性规格说明.
|
| 关 键 词： | 文件系统 微内核架构 形式化设计 形式化验证 正确性断言 Isabelle/HOL |
Research on Methodology of Formal Design and Verification for File System Based on Microkernel Architecture |
| |
| QIAN Zhen-jiang
,
TANG Hong-ying
,
LI Kang-jie
,
HUANG Hao
,
SONG Fang-min.Research on Methodology of Formal Design and Verification for File System Based on Microkernel Architecture[J].Mini-micro Systems,2013,34(10). |
| |
| Authors: | QIAN Zhen-jiang TANG Hong-ying LI Kang-jie HUANG Hao SONG Fang-min |
| |
| Abstract: | |
| |
| Keywords: | file system microkernel architecture formal design formal verification correctness assertion Isabelle/HOL |
| 本文献已被 万方数据 等数据库收录！ |
|
