随着信息技术的发展,对信息安全及软件可靠性的要求也愈来愈高,数据安全性成为当今计算机研究的热点话题。而文件系统作为操作系统的重要模块和硬盘数据的管理者,一个微小的错误甚至会导致系统的崩溃,甚至使硬盘数据丢失,可能会给用户带来巨大的经济损失,所以文件系统正确性是操作系统安全性的重要方面,亦是硬盘数据安全性的重要方面。鉴于微内核架构的高度模块独立性和形式化方法的数学逻辑性和无歧义性。设计实现了基于微内核架构的文件系统模块,并以形式化的方法从一定程度上论证了文件系统模块的正确性。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的正确性。