近年来我国铁路事业不断发展,在运输运营方面作用不可忽视,确保列车的运营安全成为重要课题。目前,我国对于时速超过250km/h的铁路采用的都是CTCS-3（China Train Control System level 3）级列车运行控制系统,也是高铁上运用最多的列车运行控制系统。对于CTCS-3级列车运行控制系统来说,它的核心设备是车载设备,承担着列车运行的主要控制功能,车载设备一旦出现故障会对列控系统造成严重影响,因此需要验证车载设备安全性。而根据车载设备的结构和功能,安全计算机完成大部分工作,它根据从其他模块收到的消息完成对列车的控制,必要时对列车实施制动命令。与车载设备进行信息交互的模块主要有RBC、司机、应答器和列车,对这些模块也要验证其正确性。传统的模型构建方法已经不能满足复杂系统的功能需求分析,形式化建模验证方法成为主要趋势。本文的主要研究内容是将CTCS-3级列控车载设备作为研究对象,对其进行建模与验证,并分析系统的安全性。首先根据对车载设备的结构、功能以及运营场景的分析构建车载设备的UML用例图、静态结构类图和动态行为状态图,这样可以直观的展示出车载设备的分析对象和对象的转换状态,为车载设备CPN模型的构建打下基础。然后根据已有的系统需求规范文件（SRS）标准的要求构建出车载设备间的信息交互CPN模型,工作模式转换的顶层CPN模型和子页CPN模型,还有与车载设备进行信息交互的几个外围环境模块（RBC、司机、应答器、列车）的CPN模型。从两个方面验证CPN模型的正确性。动态属性验证是通过模型的状态空间分析得到动态属性验证报告,分析系统的特性。系统性验证是用ASK-CTL分支时序逻辑公式来描述系统的性质,例如系统的自循环终端特性、死锁特性等来证明系统模型是否可执行。验证结果表明对车载设备的建模符合系统需求规范标准,各组件之间的交互符合规范流程。系统的建模和验证都是在系统正常工作状态下,然而在系统某些组分没有正常工作时也要确保安全性,因此最后采用故障注入技术的算法,把故障注入到正常系统中来分析系统的安全性。分析结果表明系统的安全性能满足安全需求,为以后列控系统的形式化建模与安全分析提供了参考意义。