论文摘要
随着信息技术的发展,对信息安全及软件可靠性的要求也愈来愈高,数据安全性成为当今计算机研究的热点话题。而文件系统作为操作系统的重要模块和硬盘数据的管理者,一个微小的错误甚至会导致系统的崩溃,甚至使硬盘数据丢失,可能会给用户带来巨大的经济损失,所以文件系统正确性是操作系统安全性的重要方面,亦是硬盘数据安全性的重要方面。鉴于微内核架构的高度模块独立性和形式化方法的数学逻辑性和无歧义性。设计实现了基于微内核架构的文件系统模块,并以形式化的方法从一定程度上论证了文件系统模块的正确性。1.借鉴Minix微内核架构文件系统的设计思想,借鉴Linux缓存设计机制,摒弃Minix低效性的缓存设计,为VTOS FS设计了高效稳定的缓存管理,并增加了目录项缓存的设计。2.从访问效率、安全性角度,综合比较现今流行的磁盘文件系统类型,选择eXt3磁盘文件系统类型,作为VTOS FS的根文件系统,并设计实现VTOS FS关于根文件系统的操作。3.以系统存储的数据表示系统状态,为VTOS FS建立了形式化模型。通过为VTOS FS建模可以一定程度上保证系统实现逻辑的正确性,为了进一步保证VTOS FS的正确性,辅以Isabelle/HOL定理验证器,给出VTOS FS几个重要的函数的功能正确性的论证。VTOS以微内核架构设计实现文件系统,保证了文件系统模块的模块独立性；为VTOS FS建立形式化模型保证了VTOS FS设计的逻辑正确性；对VTOS FS重要函数功能正确性的验证进一步保证了VTOS FS的正确性。
论文目录
摘要ABSTRACT第一章 绪论1.1 引言1.2 研究背景1.2.1 微内核操作系统1.2.2 磁盘文件系统1.2.3 相关工作1.3 论文组织结构第二章 相关理论介绍2.0 VTOS操作系统介绍2.1 EXT3磁盘文件系统2.2 数理逻辑2.2.1 一阶逻辑语法及语义2.2.2 形式推理规则2.3 自动机理论2.4 ISABELLE/HOL2.4.1 Isabelle/HOL语法2.4.2 Isabelle/HOL推理策略2.5 霍尔逻辑2.6 本章小节第三章 VTOS文件系统设计思想3.1 数据结构3.2 系统调用3.3 缓存设计3.3.1 inode缓存3.3.2 dentry缓存3.3.3 buffer缓存3.4 小结第四章 VTOS FS形式化模型4.1 VTOS FS对象及其状态空间4.2 EXT3硬盘形式化模型4.2.1 树类型定义4.2.2 ext3硬盘形式化模型4.3 VTOS FS系统调用功能语义4.3.1 文件系统初始化功能语义4.3.2 系统调用open功能语义4.3.3 系统调用write功能语义4.3.4 系统调用read功能语义4.3.5 系统调用close功能语义4.4 VTOS FS状态机4.5 本章小节第五章 VTOS FS状态一致性验证5.1 不变式定义5.1.1 磁盘5.1.2 inode缓存5.1.3 dentry缓存5.1.4 buffer缓存5.2 功能函数正确性验证init正确性'>5.2.1 fsinit正确性open正确性'>5.2.2 fsopen正确性5.3 本章小节第六章 总结与展望总结展望致谢附录1附录2参考文献
相关论文文献
标签：形式化方法论文; 形式化验证论文; 文件系统论文; 正确性论文;
