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

Requirement Level Verification of File System for Spacecraft

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

Due to the limitation of system resources,the embedded operating system in the spacecraft does not have the file system module.The system task completes the reading and writing of external storage devices by directly calling the I/O interface.However,with the complexity of space missions,the equipment without a file system will have a large performance bottleneck.Therefore,the development of a safe and reliable file system is an urgent issue for space embedded systems.The space embedded operating system is a typical safety-critical system,and every module integrated in the system needs to undergo rigorous testing to ensure that it will not cause malfunctions during operation.The use of formal verification technology can strictly guarantee the correctness of a certain system module mathematically.Therefore,the formal technology is used to verify the correctness of its internal logic according to the requirements of space vehicle file system in this paper.