随着列控系统的不断发展,以“车载设备为核心”的新型列控系统,将传统地面进路控制和移动授权计算等功能集成到车载设备上,并采用全IP和车-车通信等技术,成为研究热点。新型列控系统作为典型的安全苛求系统,在运营过程中一旦出现故障,将给人类生命、财产和环境造成重大甚至是灾难性的损失。因此,针对新型列控系统的安全性验证分析具有重要意义。然而,在新型列控系统中,一方面,车载设备承担了更多的地面设备功能,系统内部的故障模式耦合度更高;另一方面,引入全IP和车-车通信后,系统外部通信故障难以识别,如何自动验证系统的安全性并进行分析至关重要。针对新型列控系统的安全性特征,论文提出了一种基于统计模型检验(Statistical Model Checking,SMC)的安全性分析方法,将新型列控系统的行为抽象成价格时间自动机网络(Network of Priced Timed Automata,NPTA)模型,通过“模型仿真”生成系统安全性分析的统计样本数据,并结合统计模型检验算法进行安全性的定性和定量分析。在此基础上,选取典型运营场景,对方法进行了有效性验证。论文主要工作为:(1)围绕新型列控系统的安全性进行研究。分析了新型列控系统的结构和功能,重点研究了新型列控系统的一般运营场景。通过比较不同的列控系统安全性分析方法,提出应用统计模型检验方法进行新型列控系统安全性分析。(2)提出了一套基于统计模型检验的新型列控系统安全性分析框架。首先,重点分析了新型列控系统的运营场景,针对系统的接口层和功能层进行危险与可操作性分析(Hazard and Operability Study,HAZOP),得到危险源列表;然后,结合危险源列表,建立新型列控系统运营场景行为的NPTA模型,通过“模型仿真”生成系统安全性分析的样本数据,并利用统计模型检验算法(假设检验和概率估计),从定性和定量两方面对新型列控系统进行安全性分析;最后,以运营场景的NPTA模型为基础,导出系统NPTA模型的仿真数据进行深入挖掘。(3)针对新型列控系统典型运营场景进行系统安全性分析实例研究。围绕新型列控系统接车作业和区间追踪运营场景的安全性进行分析,基于HAZOP对新型列控系统顶层需求的危险源进行识别,根据危险源及其概率分布引入子系统故障识别模型和通信故障识别模型,构建基于NPTA的运营场景模型,并基于此模型从定性和定量两方面分析验证了新型列控系统的安全性。(4)开发了新型列控系统统计模型检验自动分析工具。利用该工具定量分析了接车作业和区间追踪运营场景的数据特征和概率分布,并基于随机森林回归数据分析模型实现了指定时间点输出正常和输出故障的概率预测,为新型列控系统的进一步研究提供了参考。论文研究结果表明,基于统计模型检验的新型列控系统安全性分析框架,能够较好的模拟系统运营场景中各模块间的信息交互及状态变迁,通过模型仿真获得系统输出故障和输出正常的概率指标,实现新型列控系统的定性和定量安全性分析。图79幅,表30个,参考文献85篇