| 列车安全距离控制形式化建模与验证 |
| |
| 引用本文： | 胡晓辉,肖知屹,陈 永,李 欣.列车安全距离控制形式化建模与验证[J].计算机应用,2014,34(3):851-856. |
| |
| 作者姓名： | 胡晓辉 肖知屹 陈 永 李 欣 |
| |
| 作者单位： | 1. 兰州交通大学 电子与信息工程学院，兰州730070;
2. 兰州交通大学 图书馆，兰州730070 |
| |
| 基金项目： | 国家自然科学基金资助项目 |
| |
| 摘 要： | 随着我国铁路的迅速发展，对列车运行安全性的要求越来越高。采用Event-B形式化建模方法研究了高速列车安全距离控制形式化验证问题，以Event-B形式化仿真工具Rodin为基础，通过结合多智能体理论，引入感知决策法则，实现了无线闭塞中心(RBC)与列车的车地通信，建立了多列车运行的安全距离控制模型。仿真研究了高速列车最小间隔追踪控制运行，对列车安全距离控车行为进行了形式化建模并进行了POs证明义务验证。仿真结果表明，对于CTCS列车控制系统的复杂逻辑关联行为，采用提出的Event-B和多智能体系统(MAS)结合的形式化验证方法，可进行系统规范的模型验证，对于复杂系统的逻辑验证有较强的实际意义。
|
| 关 键 词： | Event-B方法 列车控制 多智能体 形式化建模 分布式系统 |
| 收稿时间： | 2013-07-15 |
| 修稿时间： | 2013-09-06 |
Formal modeling and verification of train safety distance control |
| |
| 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. |
| |
| Authors: | HU Xiaohui XIAO Zhiqi CHEN Yong Li Xin |
| |
| Affiliation: | 1. School of Electronic and Information Engineering, Lanzhou Jiaotong University, Lanzhou Gansu 730070, China;
2. Library, Lanzhou Jiaotong University, Lanzhou Gansu 730070, China |
| |
| 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. |
| |
| Keywords: | Event-B train control muti-agent formal modeling distributed system |
| 本文献已被 CNKI 等数据库收录！ |
| 点击此处可从《计算机应用》浏览原始摘要信息 |
|
点击此处可从《计算机应用》下载全文 |
