随着计算机和通信技术的发展,基于通信的列车运行控制(CommunicationBased Train Control,CBTC)系统是今后轨道交通列车运行控制系统的发展趋势。车载控制器(VOBC)作为CBTC系统中的关键设备,具有复杂的功能和很高的安全性要求。因此需要记录大量的列车状态信息和运行日志,以此作为开发人员调试设备的依据,为了降低查找数据的复杂度,从而方便开发人员进行故障定位和故障重现,需要在车载数据记录器中使用文件系统对大量的记录信息进行有效的管理。根据车载数据记录器的需求,论文采用Nand Flash作为大容量存储单元,并对Nand Flash文件系统的结构和算法进行了设计。在文件管理层,借鉴ⅰ节点和日志文件系统的设计思想,设计了树形结构以及“先写后擦”的操作方式,从而保证了文件操作的快速性和数据的可靠性。在空间管理层,设计了空间管理表的索引结构,提高了查找和分配资源的效率。在垃圾回收机制中设计了dirtiest-list的方法,在垃圾回收时综合考虑回收率和擦除次数。针对cold data(长期不更新的数据)引起的磨损不平衡现象,设计了主动平衡策略,将cold data搬移到擦除次数最多的空闲块中,使擦除次数少的块能够进入到磨损循环中来。为了增强系统的可靠性,论文设计了有效的异常恢复机制,通过对状态标记和对象号(记录在页空闲区中)的判断,实现对数据的恢复。在系统设计的基础上,论文引入了形式化验证方法有色Petri网(CPN)对文件系统空间分配算法进行了建模。采用“由上而下”的思路建立了顶层模型和各个子模型,子模型包括写入、删除、垃圾回收以及磨损平衡模块。并针对写入模块进行了重点研究,利用状态空间分析的方法完成了该模型的完备性验证,为整个模型的验证提供了一种可行的方法。最后,论文通过计算机仿真的方法对垃圾回收的性能和磨损平衡的效果进行了测试和分析。通过分析,发现了垃圾回收机制中存在的问题,针对该问题提出改进的策略,并验证了改进的效果。