客运专线CTCS-3级列控系统无线闭塞中心的建模与验证

• 作者: 吕继东 唐涛 贾昊
• 来源期刊: 铁道学报
• 学科: 交通运输
• 关键词: CTCS 时间自动机 RBC UPPAAL 实时系统
• 年，卷（期）: 2010,（6）
• 页码范围: 34-42
• 分类号: TP393|U283
• 字数: 6612字
• 语种: 中文
• DOI: 10.3969/j.issn.1001-8360.2010.06.006

摘要

本文分析客运专线CTCS-3级列控系统中无线闭塞中心(RBC)子系统软件的功能和性能约束,在此基础上采用时间自动机理论进行RBC子系统形式化语义描述,建立TER-QSR时间自动机网络模型,并应用UPPAAL验证工具对RBC子系统进行仿真分析,验证RBC的安全性(Safety)和受限活性(Bounded Liveness),同时进行RBC切换时间的优化.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	唐涛	北京交通大学轨道交通控制与安全国家重点实验室	152	2578	27.0	40.0
2	吕继东	北京交通大学轨道交通控制与安全国家重点实验室	25	310	9.0	17.0
3	贾昊	西安交通大学电子与信息工程学院	1	63	1.0	1.0