论文部分内容阅读
目前城市轨道交通在我国大中型城市大力发展,基于通信的列控系统(CBTC)的普及与应用,既保证了城市轨道交通运营的安全性,也使得其运营效率得到了提高。CBTC系统由中心设备、地面设备、轨旁设备和车载设备共四部分组成,四者之间存在复杂繁多的信息交互,特别是地面设备和轨旁设备多,建设成本和运营成本大。在保证城市轨道交通运营安全与效率的前提下,通过功能再分配、优化系统结构,减少地面和轨旁设备,降低建设和维护成本,是列控系统的发展趋势。针对城市轨道交通线路结构和运输作业简单的特点,本文探索了一种基于车-车通信的、结构简化的列控系统方案,并通过基于模型的仿真与形式化验证相结合的方式对此方案进行仿真验证。具体工作如下:(1)设计了车-车通信在列控系车载设备中的应用方案。描述了系统结构和功能,设计了车载设备与中心设备、对象控制器三部分间的信息交互流程及控车原理。(2)设计了基于模型的仿真与形式化验证相结合的系统建模验证方法。对安全状态机建模理论增加时间概念,并给出了两种建模工具下的模型对应关系,此方法兼具仿真验证的直观具体与形式化验证的严谨全面的特点。(3)完成了基于车-车通信的列控系统车载设备部分功能模块的建模、仿真与形式化验证。在MATLAB环境下,对车载设备的车-车通信管理、行车许可生成和速度控制三个核心功能模块,进行了可视化建模仿真,并完成了基于UPPAAL的形式化验证,分析了三个核心功能模块的功能正确性。(4)在VS2015环境下进行了基于传统代码编译的基于车-车通信的列控系统仿真软件的实现。不但以可视化的方式呈现了仿真过程及结果,还与基于模型的仿真及验证的分析结果相辅相成,进一步表明系统方案的可行性。