中文摘要：

随着我国铁路的迅速发展,对列车运行安全性的要求越来越高.采用Event-B形式化建模方法研究了高速列车安全距离控制形式化验证问题,以Event-B形式化仿真工具Rodin为基础,通过结合多智能体理论,引入感知决策法则,实现了无线闭塞中心（RBC）与列车的车地通信,建立了多列车运行的安全距离控制模型.仿真研究了高速列车最小间隔追踪控制运行,对列车安全距离控车行为进行了形式化建模并进行了POs证明义务验证.仿真结果表明,对于CTCS列车控制系统的复杂逻辑关联行为,采用提出的Event-B和多智能体系统（MAS）结合的形式化验证方法,可进行系统规范的模型验证,对于复杂系统的逻辑验证有较强的实际意义.

英文摘要：

With the rapid development of Chinese railway, requirements for running safety of trains are more high. This paper used the Event-B formal modeling approach to research on the high-speed train safety distance control. With the support of simulation tool Rodin, combined with the multi-Agent theory, the safety distance control model of multi-train operation was constructed. The simulation researched the modeling and verification on the minimum interval tracking control for high speed train. The simulation results show that, the binding of formal verification methods of Event-B and Muhi-Agent System （MAS） is meaningful. So the method has some practical significance for the modeling and verification of complex system.