计算机应用 ›› 2014, Vol. 34 ›› Issue (3): 851-856.DOI: 10.11772/j.issn.1001-9081.2014.03.0851

• 计算机软件技术 • 上一篇    下一篇

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

胡晓辉1,肖知屹1,陈永1,李欣2   

  1. 1. 兰州交通大学 电子与信息工程学院,兰州730070;
    2. 兰州交通大学 图书馆,兰州730070
  • 收稿日期:2013-07-15 修回日期:2013-09-06 出版日期:2014-03-01 发布日期:2014-04-01
  • 通讯作者: 肖知屹
  • 作者简介:胡晓辉(1963-),男,甘肃庆阳人,教授,博士,主要研究方向:智能信息处理、分布计算;肖知屹(1987-),男,河北唐山人,硕士研究生,主要研究方向:智能计算;陈永(1979-),男,甘肃武威人,讲师,博士研究生,主要研究方向:软件形式化;李欣(1981-),男,河南沁阳人,讲师,硕士,主要研究方向:分布式计算。
  • 基金资助:

    国家自然科学基金资助项目

Formal modeling and verification of train safety distance control

HU Xiaohui1,XIAO Zhiqi1,CHEN Yong1,Li Xin2   

  1. 1. School of Electronic and Information Engineering, Lanzhou Jiaotong University, Lanzhou Gansu 730070, China;
    2. Library, Lanzhou Jiaotong University, Lanzhou Gansu 730070, China
  • Received:2013-07-15 Revised:2013-09-06 Online:2014-03-01 Published:2014-04-01
  • Contact: XIAO Zhiqi

摘要:

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

关键词: Event-B方法, 列车控制, 多智能体, 形式化建模, 分布式系统

Abstract:

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 Multi-Agent System (MAS) is meaningful. So the method has some practical significance for the modeling and verification of complex system.

Key words: Event-B, train control, muti-agent, formal modeling, distributed system

中图分类号: