空间嵌入式操作系统是空间飞行器必备的基础软件,决定了空间飞行器是否能够可靠安全地完成空间飞行任务。目前已经采用多种手段来保证其可靠性和安全性,但是仍然存在一些难以发现的缺陷。形式化验证方法在一些工业领域中得到了很好的应用,被验证过的系统的可靠性和安全性都远远高于未验证的系统。因此,采用形式化方法来验证空间嵌入式操作系统势在必行,保证其正确性,从而使其更加可靠安全。存储子系统是空间嵌入式操作系统的重要组成部分,包括内存管理和文件管理。其中,内存管理是系统运行的基础,保证其可靠安全地运行是空间嵌入式操作系统的内在要求。此外,空间飞行任务产生的数据越来越多,空间嵌入式操作系统亟需文件系统来进行数据处理,因此需要开发可靠安全的面向空间应用的文件系统。本文以空间嵌入式操作系统Space OS2为对象,研究面向空间应用的嵌入式存储子系统,进行了如下三个方面的研究。（1）针对复杂软件在“需求、设计、实现”三层验证框架下具体验证的问题,首先使用数学方法证明了采用“需求-设计-实现”三层验证框架可以显著降低验证的工作量。然后分别针对每一层提出了具体的验证方法:在需求层针对需求文档中的功能需求提出了系统实例化的验证方法;在设计层针对设计流程图提出了基于全局变量性质的验证方法;在实现层针对具体的实现代码提出了面向操作的验证方法。（2）在“需求-设计-实现”三层验证框架下研究了Space OS2内存管理模块的形式化验证。在需求层针对内存状态过于庞大的问题,提出了基于归纳演绎的内存状态形式化验证方法。该方法提炼出内存状态变换过程中不变的性质,利用归纳的数学形式演算内存状态间的变化,证明内存操作的前后满足内存状态的性质,避免逐一验证所有内存状态的正确性,提高了验证效率。针对内存管理模块的设计层和实现层分别采用对应的验证方法完成了形式化验证的工作。（3）针对可靠安全文件系统的开发问题,应用“需求-设计-实现”分层验证框架,采用形式设计方法,实现了一个应用于Space OS2的空间专用闪存文件系统。此外,针对空间闪存文件系统占用内存小的需求,对文件目录提出了基于任务的细粒度文件目录索引方法,对文件数据提出了基于单链表结构的逆向链表索引方法,降低了闪存文件系统对内存的占用量,形成了面向任务的空间专用闪存文件系统。