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

doi:10.11772/j.issn.1001-9081.2014.03.0851

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

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

胡晓辉¹,肖知屹¹,陈永¹,李欣²

1. 兰州交通大学电子与信息工程学院，兰州730070;
2. 兰州交通大学图书馆，兰州730070

收稿日期:2013-07-15 修回日期:2013-09-06 发布日期:2014-04-01 出版日期:2014-03-01
通讯作者: 肖知屹
作者简介:胡晓辉（1963-），男，甘肃庆阳人，教授，博士，主要研究方向:智能信息处理、分布计算；肖知屹（1987-），男，河北唐山人，硕士研究生，主要研究方向：智能计算；陈永（1979-），男，甘肃武威人，讲师，博士研究生，主要研究方向:软件形式化；李欣（1981-），男，河南沁阳人，讲师，硕士，主要研究方向:分布式计算。
基金资助:
国家自然科学基金资助项目

Formal modeling and verification of train safety distance control

HU Xiaohui¹,XIAO Zhiqi¹,CHEN Yong¹,Li Xin²

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-04-01 Published:2014-03-01
Contact: XIAO Zhiqi

摘要/Abstract

摘要：

随着我国铁路的迅速发展，对列车运行安全性的要求越来越高。采用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

中图分类号:

TP301.2

胡晓辉肖知屹陈永李欣. 列车安全距离控制形式化建模与验证[J]. 计算机应用, 2014, 34(3): 851-856.

HU Xiaohui XIAO Zhiqi CHEN Yong Li Xin. Formal modeling and verification of train safety distance control[J]. Journal of Computer Applications, 2014, 34(3): 851-856.

[1]	刘晓芳, 张军. 概率驱动的动态多目标多智能体协同调度进化优化[J]. 《计算机应用》唯一官方网站, 2024, 44(5): 1372-1377.
[2]	姚洪磊, 刘吉强, 童恩栋, 牛温佳. 基于 α-截集三角模糊数和攻击树的CTCS网络安全风险评估方法[J]. 《计算机应用》唯一官方网站, 2024, 44(4): 1018-1026.
[3]	唐朝君, 夏梅妍, 张华, 谢挺. 动态事件触发下多智能体系统固定时间一致性[J]. 《计算机应用》唯一官方网站, 2024, 44(3): 960-965.
[4]	邓辅秦, 谭朝恩, 黎俊炜, 钟家铭, 付兰慧, 张建民, 王宏民, 李楠楠, 姜炳春, 林天麟. 面向大型仓储环境的基于冲突搜索算法[J]. 《计算机应用》唯一官方网站, 2024, 44(12): 3854-3860.
[5]	王昱, 关智慧, 李远鹏. 基于轨迹预测和分布式MADDPG的无人机集群追击决策[J]. 《计算机应用》唯一官方网站, 2024, 44(11): 3623-3628.
[6]	孙安泰, 刘烨, 徐冬梅. 多智能体系统的动态面渐近补偿算法[J]. 《计算机应用》唯一官方网站, 2024, 44(10): 3151-3157.
[7]	黄晓辉, 杨凯铭, 凌嘉壕. 基于共享注意力的多智能体强化学习订单派送[J]. 《计算机应用》唯一官方网站, 2023, 43(5): 1620-1624.
[8]	赵琳, 吕科, 郭靖, 宏晨, 向贤财, 薛健, 王泳. 基于深度强化学习的无人机集群协同作战决策方法[J]. 《计算机应用》唯一官方网站, 2023, 43(11): 3641-3646.
[9]	高安安, 胡爱花, 江正仙. 事件触发脉冲控制多智能体系统的安全一致[J]. 《计算机应用》唯一官方网站, 2023, 43(1): 140-146.
[10]	邓晖奕, 李勇振, 尹奇跃. 引入通信与探索的多智能体强化学习QMIX算法[J]. 《计算机应用》唯一官方网站, 2023, 43(1): 202-208.
[11]	陈浩杰, 范江亭, 刘勇. 深度强化学习解决动态旅行商问题[J]. 《计算机应用》唯一官方网站, 2022, 42(4): 1194-1200.
[12]	臧嵘, 王莉, 史腾飞. 基于注意力消息共享的多智能体强化学习[J]. 《计算机应用》唯一官方网站, 2022, 42(11): 3346-3353.
[13]	王云燕, 胡爱花. 网络攻击下双层结构多智能体系统一致性[J]. 计算机应用, 2021, 41(5): 1399-1405.
[14]	姚兴虎, 谭晓阳. 基于奖励高速路网络的多智能体强化学习中的全局信用分配算法[J]. 计算机应用, 2021, 41(1): 1-7.
[15]	吴志军, 王航. 基于订阅/发布服务的广域信息管理系统应急响应机制[J]. 计算机应用, 2020, 40(5): 1340-1347.

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

Formal modeling and verification of train safety distance control

PDF

可视化

摘要/Abstract

引用本文

使用本文

参考文献

相关文章 15

编辑推荐

Metrics