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