| 基于UPPAAL的城市轨道交通CBTC区域控制子系统建模与验证 |
| |
| 引用本文： | 吕继东,唐涛,燕飞,徐天华.基于UPPAAL的城市轨道交通CBTC区域控制子系统建模与验证[J].铁道学报,2009,31(3). |
| |
| 作者姓名： | 吕继东 唐涛 燕飞 徐天华 |
| |
| 作者单位： | 北京交通大学,轨道交通控制与安全国家重点实验室,北京,100044 |
| |
| 摘 要： | CBTC(Communication Based Train Control)系统可有效提高轨道交通的列车运营效率,降低系统建设和维护费用.在系统研发过程中需对系统进行建模、仿真和验证,发现系统设计缺陷,以保证系统的安全性.CBTC区域控制子系统是一实时控制系统,它要求控制时间的精确性和控制过程的准确性.本文通过分析城市轨道交通CBTC区域控制子系统的结构,给出满足该子系统安全性的功能和性能要求,并结合时间自动机理论方法提出包含列车、速度距离控制器、区域控制器和多车控制队列的时间自动机网络模型.同时,应用UPPAAL验证工具对CBTC区域控制子系统进行仿真建模,并验证该子系统功能和性能要求,从而保证了系统模型的安全性和受限活性.
|
| 关 键 词： | 区域控制子系统 时间自动机 自动验证 |
UPPAAL-based Simulation and Verification of CBTC Zone Control Subsystem in Rail Transportation |
| |
| Lü Ji-Dong,TANG Tao,YAN Fei,XU Tian-hua.UPPAAL-based Simulation and Verification of CBTC Zone Control Subsystem in Rail Transportation[J].Journal of the China railway Society,2009,31(3). |
| |
| Authors: | Lü Ji-Dong TANG Tao YAN Fei XU Tian-hua |
| |
| Abstract: | |
| |
| Keywords: | UPPAAL |
| 本文献已被 维普 万方数据 等数据库收录！ |
|
