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

被引：15

作者：

吕继东 ^{[1
]}

唐涛 ^{[1
]}

贾昊 ^{[2
]}

机构：

[1] 北京交通大学轨道交通控制与安全国家重点实验室

[2] 西安交通大学电子与信息工程学院

来源：

铁道学报 | 2010年 / 06期

关键词：

CTCS; 时间自动机; RBC; UPPAAL; 实时系统;

D O I：

暂无

中图分类号：

TP273 [自动控制、自动控制系统];

学科分类号：

080201 ; 0835 ;

摘要：

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

引用

页码：34 / 42

页数：9

共 6 条

[1] CTCS-3级列车运行控制系统综合测试平台研究 [J].

季学胜 ;

唐涛 .

铁道通信信号, 2007, (07) :1-3

[2] 基于时间自动机的道岔自动控制研究 [J].

周清雷 ;

姬莉霞 .

控制工程, 2004, (S2) :146-149

[3] 基于UPPAAL的实时系统模型验证 [J].

周清雷 ;

姬莉霞 ;

王艳梅 .

计算机应用, 2004, (09) :129-131

[4]

CTCS-3级列控系统总体技术方案[M]. 中国铁道出版社 , 张曙光, 2008

[5]

软件开发的形式化方法[M]. 高等教育出版社 , 古天龙[著], 2005

[6]

Uppaal-Present and Future. Behrmann G,David A,Larsen K G,et al. Proc.of the40thIEEE Conference on Decision and Control（CDC’2001） . 2001

← 1 →