%0 Journal Article
%T 列车安全距离控制形式化建模与验证
%A 胡晓辉
%A 肖知屹
%A 陈永
%A 李欣
%J 计算机应用
%D 2014
%X ？随着我国铁路的迅速发展，对列车运行安全性的要求越来越高。采用event-b形式化建模方法研究了高速列车安全距离控制形式化验证问题，以event-b形式化仿真工具rodin为基础，通过结合多智能体理论，引入感知决策法则，实现了无线闭塞中心(rbc)与列车的车地通信，建立了多列车运行的安全距离控制模型。仿真研究了高速列车最小间隔追踪控制运行，对列车安全距离控车行为进行了形式化建模并进行了pos证明义务验证。仿真结果表明，对于ctcs列车控制系统的复杂逻辑关联行为，采用提出的event-b和多智能体系统(mas)结合的形式化验证方法，可进行系统规范的模型验证，对于复杂系统的逻辑验证有较强的实际意义。
%K event-b方法
%K 列车控制
%K 多智能体
%K 形式化建模
%K 分布式系统
%U http://www.joca.cn/CN/abstract/abstract17119.shtml