面向空间飞行器的文件系统需求层验证

由于系统资源的有限性,目前空间飞行器中的嵌入式操作系统并没有文件系统模块.系统任务通过直接调用I/O接口,完成外部存储设备的读与写.但是,随着空间飞行任务复杂化,数据大量涌现,空间嵌入式操作系统需要文件系统来完成数据处理,因此安全可靠的文件系统的开发是空间嵌入式操作系统亟待解决的问题.空间嵌入式操作系统是典型的安全关键的系统,集成在系统中的每一个模块都需要经过严格的测试,保证其不会在运行期间产生故障.采用形式化验证的技术可以从数学上严格保证验证对象的正确性.因此,本文采用形式化技术,针对面向空间飞行器文件系统的需求,验证其内部逻辑的正确性.