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

摘要：

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

关键词：CTCS、时间自动机、RBC、UPPAAL、实时系统

所属期刊栏目：32

分类号：TP393;U283(计算技术、计算机技术)

资助基金：国家自然科学基金60634010;北京交通大学科技基金项目2007XM004;轨道交通控制与安全国家重点实验室自主研究题目RCS2008ZZ005

在线出版日期：2011-03-17（万方平台首次上网日期，不代表论文的发表时间）

页数：共9页

页码：34-42