基于UPPAAL的列控系统临时限速建模与验证

宋莉; 刘伯鸿

基于UPPAAL的列控系统临时限速建模与验证

宋莉,
刘伯鸿

兰州交通大学自动化与电气工程学院, 兰州 730070

基金项目:

中国铁路总公司科技研究开发计划项目(2017X010-E)

详细信息

作者简介:
宋莉,在读硕士研究生;刘伯鸿,副教授。

中图分类号: U284.482;TP39
计量
- 文章访问数: 82
- HTML全文浏览量: 1
- PDF下载量: 11
出版历程
- 收稿日期: 2019-09-15

UPPAAL-based modeling and verification of temporary speed restriction in train control system

SONG Li,
LIU Bohong

College of Automation&Electrical Engineering, Lanzhou Jiaotong University, Lanzhou 730070, China

摘要

摘要: 临时限速系统是列控系统的重要组成部分,是符合"故障-安全"准则的安全苛求系统。文章基于临时限速技术规范和时间自动机理论,分析临时限速系统的组成结构,提取其功能和性能约束,利用UPPAAL工具对其信息交互行为进行建模仿真,验证该系统的实时性,为进一步完善临时限速系统的设计与开发提供参考。
- 建模与验证 /
- 临时限速 /
- 安全苛求系统 /
- 故障-安全准则 /
- 时间自动机 /
- UPPAAL
Abstract: As an important part of the train control system, the temporary speed restriction system is a safety-critical one that meets fail-safe criteria. Based on the technical specification on temporary speed restriction and the theory of timed automata, this paper analyzed the composition and structure of the temporary speed restriction system, extracted its function and performance constraints for modeling and simulating its data interaction behaviors by using UPPAAL tool to verify its real-time performance, offering reference for further improving the design and development of the temporary speed restriction system.
- modeling and verification /
- temporary speed restriction /
- safety-critical system /
- fail-safe criteria /
- timed automata /
- UPPAAL

HTML全文

参考文献(15)

[1]	周翔,武晓春. 基于MSC与UPPAAL的高铁跨界临时限速建模与验证[J]. 铁道标准设计, 2016(10):126-131.
[2]	张大鹏. 基于时间自动机的跨界临时限速建模与分析[J]. 铁道通信信号, 2018, 54(2):5-10.
[3]	康仁伟. 基于时间自动机的CTCS-3级列控系统建模方法与验证研究[D]. 北京:北京交通大学, 2013:40-53.
[4]	袁磊,王俊峰. CTCS-3级列控系统临时限速建模与验证[J]. 西南交通大学学报, 2013, 48(4):701-712.
[5]	曹源. 高速铁路列车运行控制系统的形式化建模与验证方法研究[D]. 北京:北京交通大学, 2011.
[6]	胡雪莲,陶彩霞. 基于MSC与UPPAAI. 的列控系统等级转换场景形式化验证[J]. 铁道标准设计, 2015(2):122-127.
[7]	Hessel A, Larsen K G, Mikucionis M. Testing real-time systems using UPPAAL[J]. Lecture Notesin Computer Science, 2008(4949):77-117.
[8]	Larsen K G, Mikucionis M, Nielsen B. Online Testing of Real time System Using UPPAAL, Formal Approaches to Software Testing-4th lnternational Workshop[J].Lecture Notes in Computer Science:(S0302-9743), 2015(3395):79-94.
[9]	万勇兵,徐中伟,梅萌. CTCS-3级列控系统临时限速服务器建模与形式化验证[J]. 系统仿真学报, 2013, 25(1):132-138.
[10]	Jackson M O. The Economics of Social Networks[M]. Cambridge, UK:Cambridge University Press, 2016:36-42.
[11]	赵荣亮,王长林. 高速铁路CTC分界口临时限速系统建模与验证[J]. 铁路计算机应用, 2014, 23(7):43-47.
[12]	甄力剑. 客运专线临时限速技术研究与应用[D]. 成都:电子科技大学, 2012.
[13]	M E J Newman, M Girvan. Finding and evaluating community structure in networks[J]. Phys. Rev. E (S 1539-3755), 2016, 69(7):126-133.
[14]	Zhou J, Liu Z H, Li B. Influence of network structure on rumor propagation[J]. Physics Letters A (S0375-9601), 2009, 368(9):458-463.
[15]	姜明华. 列控系统级间转换点临时限速区段设置探讨[J]. 铁道通信信号, 2013(4):32-33.

施引文献(10)

期刊类型引用(7)

1.	谢生智. 基于北斗的重载铁路列控系统临时限速系统方案安全性分析. 铁路通信信号工程技术. 2025(01): 44-50+140 . 百度学术
2.	周翔. 基于UML与UPPAAL的高铁列控临时限速切换场景建模与验证. 山东交通学院学报. 2024(03): 31-38 . 百度学术
3.	吴金元，王菁. CBTC系统点式模式下临时限速方案分析. 铁路通信信号工程技术. 2023(04): 73-76 . 百度学术
4.	李建雄，吉志军，罗飞豹. 基于UPPAAL的LKJ-15系统模式转换功能建模与验证研究. 铁道通信信号. 2023(05): 60-66 . 百度学术
5.	耿鹏. CBTC系统区域控制器重启后的临时限速控制方法研究. 铁道通信信号. 2022(03): 90-93 . 百度学术
6.	刘嘉诚，王梓丞，易立富，王光前. 面向全自动运行的城轨交通火灾联动方案设计与建模验证. 铁道通信信号. 2022(04): 64-74+88 . 百度学术
7.	丁源，李震，白铭，李瑞峰，周宇. 铁路智能移动减速信号牌研究. 中国安全科学学报. 2020(S1): 77-83 . 百度学术