我国铁路近些年发展形势迅猛，列车的安全行驶问题同时逐渐受到人们的高度关注。列车车载自动防护系统(ATP)的核心功能是对列车的行车安全进行安全防护，最大限度地保障列车的行车安全。列车车载自动防护系统对于列车运行控制系统来说十分的重要，列车任何时间的具体位置以及列车运行的行车间隔、速度、加速度等重要信息都是由列车定位的功能来实现。现代化的列车车载自动防护系统采用了先进的信息技术，然而其系统本身由于系统化、网络化、复杂化且具有极强的实时性及其分布式设备特征以及其混合属性的特点，采用形式化方法建立其相对应的设备系统模型能够更最大程度地理解和分析列车车载自动防护系统，并可以用更小的成本尽可能的观察系统在逻辑正确性、整体一致性和功能完备性上的表现。形式化建模仿真语言Event-B是一种处于发展前言的语言，其建模仿真平台是由Rodin这款软件来提供。该语言中的Machine部分经过不断提精之后，利用计算机模拟计算其中事件的不变式能够达到模拟真实效果的系统状态的一个行为效果；该语言中的Context部分经过不断的扩展之后，模拟出来的环境可以更趋于真实的环境；与此同时，Event-B中应用的完善的数学理论具备了一般形式化理论方法中所应用的数学理论，该语言能够把系统运行过程中的各种状态通过使用数学的方法进行表述和计算，同时检查系统的逻辑正确性与完备性。所以，能够对系统的形式化建模仿真起到有效的作用。本文需要一套统一的语义理论和一致的高层构建定理来保证模型能够进行正确的转化和有效的验证，用来保证产生的模型的正确性，并且对模型的规范、精化和验证提供工具的支持。Event-B语言是基于严格数学定义的形式化方法，能够精确、清晰地描述系统结构的特性。文章采用形式化方法Event-B研究了高速列车安全距离控制形式化验证的问题，以Event-B形式化仿真工具Rodin为基础，通过结合多智能体理论，引入感知模块法则，实现了RBC与列车的车地通信，建立了多列车运行的安全距离控制模型。仿真研究了高速列车最小间隔追踪控制运行，对列车安全距离控车行为进行了形式化建模并进行了证明义务(PO)验证。仿真结果表明，对于CTCS列车控制系统的复杂逻辑关联行为，采用提出的Event-B和多智能体系统(MAS)结合的形式化验证方法，可以进行系统规范化的模型验证，对于复杂系统的逻辑验证有较强的实际意义。