列车安全距离控制形式化建模与验证

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