列车运行控制系统的形式化研究进展与趋势

doi:10.3981/j.issn.2097-0781.2023.01.008

前瞻科技 ›› 2023, Vol. 2 ›› Issue (1): 106-117.DOI: 10.3981/j.issn.2097-0781.2023.01.008

列车运行控制系统的形式化研究进展与趋势

吕继东¹(), 卢万里¹, 唐涛²^,^†(), 罗正伟¹

1.北京交通大学轨道交通运行控制系统国家工程研究中心，北京 100044
2.北京交通大学轨道交通控制与安全国家重点实验室，北京 100044

收稿日期:2022-12-26 修回日期:2023-02-01 出版日期:2023-03-20 发布日期:2023-03-27
通讯作者: ^†
作者简介:吕继东，教授，博士研究生导师。主要从事列控系统形式化建模、安全验证与测试的基础理论与实际应用等研究。先后主持和参与国家重点基础研究发展计划、国家自然科学基金重点面上项目、国家重点研发计划、北京市自然科学基金等国家级、省部级科研项目20余项。出版专著2部，发表论文60余篇，获授权发明专利10项，获软件著作权10项。获中国铁道学会科学技术奖一等奖1项。电子信箱：jdlv@bjtu.edu.cn。
唐涛，教授，博士研究生导师。北京交通大学轨道交通控制与安全国家重点实验室主任，北京市开放实验室“城市轨道交通自动化与控制实验室”主任。主要从事轨道交通列车运行控制等研究。入选新世纪百千万人才工程国家级人才。担任“交通信息工程及控制”国家级重点学科带头人、教育部自动化专业教学指导委员会委员、中国铁道学会理事。获教育部新世纪优秀人才支持计划、铁道部有突出贡献中青年专家、茅以升铁道科技奖和“北京市优秀教师”等荣誉称号。先后主持国家高技术研究发展计划、国家自然科学基金重点、国际合作项目等60余项。出版专著5部，发表论文200余篇，获授权发明专利9项，参与制定国家标准2项、行业规范14项。获国家科学技术进步奖二等奖2项、中国铁道学会科学技术奖一等奖2项、教育部自然科学奖一等奖1项、北京市科学技术进步奖一等奖2项、詹天佑铁道科学技术奖成就奖。电子信箱：ttang@bjtu.edu.cn。
基金资助:
国家自然科学基金(52272329);北京市自然科学基金(L201004)

Research Progress and Trend of Formal Methods for Train Control System

LÜ Jidong¹(), LU Wanli¹, TANG Tao²^,^†(), LUO Zhengwei¹

1. National Engineering Research Center of Rail Transportation Operation and Control System, Beijing Jiaotong University, Beijing 100044, China
2. State Key Laboratory of Rail Traffic Control and Safety, Beijing Jiaotong University, Beijing 100044, China

Received:2022-12-26 Revised:2023-02-01 Online:2023-03-20 Published:2023-03-27
Contact: ^†

摘要/Abstract

摘要：

列车运行控制系统是保障列车安全与高效运行的核心。目前中国列车运行控制技术整体已步入世界先进水平，正在向智能化、智慧化方向发展，迫切需要以自主化工具平台支撑的正向研发设计方法。形式化方法是保障列车运行控制系统功能正确实现的关键。文章首先回顾了列车运行控制系统的发展过程，分析了计算机时代列车运行控制系统的特点;总结了国内外列车运行控制领域形式化的应用研究、取得的进展和趋势，并对比了国内外列车运行控制领域形式化研究的差异;最后提出了采用基于模型的系统工程方法进行列车运行控制系统正向设计的发展方向，并从系统正向顶层设计、形式化技术自主化和人才队伍培养方面给出了发展建议，力求实现功能强大、覆盖全面、性能先进的列车运行控制系统。

关键词: 列车运行控制系统, 形式化方法, 基于模型的开发, 需求规范, 建模验证

Abstract:

The train control system is the core for safe and efficient train operation. China’s current train control technology as a whole has reached the world’s advanced level and is developing toward intelligent and smart technologies. There is an urgent need for forward research and development and design methods supported by independent tool platforms. The formal method is the key to ensuring the correct implementation of the train control system’s functions. This paper first reviews the development process of the train control system and analyzes its characteristics in the computer era. Then, this paper summarizes the application research, progress, and trend of formal methods in train control both in and outside China and compares the differences in research on formal methods for train control. Finally, the development direction of the forward design of the train control system using model-based systems engineering (MBSE) is proposed, and development suggestions are given from the aspects of the system’s forward top-level design, formal technology independence, and talent team training. The efforts are dedicated to obtaining a train control system with powerful functions, comprehensive coverage, and advanced performance.

Key words: train control system, formal methods, model-based development, requirements specification, modeling and verification

吕继东, 卢万里, 唐涛, 罗正伟. 列车运行控制系统的形式化研究进展与趋势[J]. 前瞻科技, 2023, 2(1): 106-117.

LÜ Jidong, LU Wanli, TANG Tao, LUO Zhengwei. Research Progress and Trend of Formal Methods for Train Control System[J]. Science and Technology Foresight, 2023, 2(1): 106-117.

图/表 7

参考文献 32

[1]	Ferrari A, ter Beek M H. Formal methods in railways: A systematic mapping study[J]. ACM Computing Surveys, 2023, 55(4): 1-37.
[2]	唐涛. 列车运行控制系统[M]. 北京: 中国铁道出版社, 2012.
[3]	IEEE Vehicular Technology Society.IEEE 1474.3-2008 IEEE recommended practice for Communication-Based Train Control (CBTC) system design and functional allocations[S]. Piscataway: IEEE Press, 2008.
[4]	CENELEC,. EN 50128-2001 Railway application-com-munications, signaling and processing systems-software for railway control and protection systems[S]. Brussels: CENELEC, 2001.
[5]	Di Claudio M, Fantechi A, Martelli G, et al. Model-based development of an automatic train operation component for communication based train control[C]// Proceedings of the 17th International IEEE Conference on Intelligent Transportation Systems (ITSC). Piscataway:IEEE Press, 2014: 1015-1020.
[6]	蒋立国, 宋春景, 李响. MBSE在核工程设计中的应用[J]. 科技导报, 2019, 37(7): 62-67.
[7]	薛威, 贾超群, 李雯, 等. 基于MBSE在航空电子通信系统中的应用[J]. 电子科技, 2016, 29(5): 45-48.
[8]	Abrial J R, Hoare A. The B-book: Assigning programs to meanings[M]. Cambridge: Cambridge University Press, 1996.
[9]	Fantechi A. Twenty-five years of formal methods and railways: What next?[C]// Counsell S, Núñez M. Proceedings of the 11th International Conference on Software Engineering and Formal Methods, SEFM 2013. Cham: Springer, 2014: 167-183.
[10]	DaSilva C, Dehbonei B, Mejia F. Formal specification in the development of industrial applications: Subway speed control system[C]// Proceedings of the IFIP TC6/WG6.1 Fifth International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols, FORTE ’92. North-Holland: DBLP, 1992: 199-213.
[11]	CENELEC,. EN 50128-1998 Railway applications: Software for railway control and protection systems[S]. Brussels: CENELEC, 1998.
[12]	Bjørner D. New results and trends in formal techniques for the development of software for transportation systems[J]. Journal of Non-Crystalline Solids, 2003, 303(2): 253-261. DOI URL
[13]	Laporte C Y, Houde R, Marvin J. 6.4.2 systems engineering international standards and support tools for very small enterprises[J]. INCOSE International Symposium, 2014, 24(1): 551-569. DOI URL
[14]	吕继东, 李开成, 唐涛, 等. 基于混合通信顺序进程的高速铁路列控系统形式化建模与验证方法[J]. 中国铁道科学, 2012, 33(5): 91-97.
[15]	Zou L, Lü J D, Wang S L, et al. Verifying Chinese train control system under a combined scenario by theorem proving[C]//Cohen E, Rybalchenko A. Proceedings of the Working Conference on Verified Software:Theories, Tools, and Experiments. Berlin, Heidelberg: Springer, 2014: 262-280.
[16]	北京交通大学轨道交通领域主要成果[J]. 铁道学报, 2019, 41(9): 128.
[17]	Chen X H, Zhong Z W, Jin Z, et al. Automating consistency verification of safety requirements for railway interlocking systems[C]// Proceedings of the 2019 IEEE 27th International Requirements Engineering Conference (RE 2019). Piscataway:IEEE Press, 2019: 308-318.
[18]	刘筱珊, 袁正恒, 陈小红, 等. 区域控制器的安全需求建模与自动验证[J]. 软件学报, 2020, 31(5): 1374-1391.
[19]	李雷. 基于SCADE的CBTC区域控制器软件测试方法研究[D]. 北京: 北京交通大学, 2011.
[20]	Wang H F, Ning B, Chen T, et al. Route safety verification of train control system by FTA modeling in SCADE[C]// Proceedings of the 2018 21st International Conference on Intelligent Transportation Systems (ITSC). Piscataway:IEEE Press, 2018: 2718-2723.
[21]	Zhang Y, Wang H F, Chai M, et al. Novel graph-based train control data verification method for Chinese train control system[J]. IEEE Intelligent Transportation Systems Magazine, 2021, 13(3): 45-57.
[22]	王倩倩, 张勇. UML建模技术在轨道交通CTCS-3级列车控制系统测试案例生成中的应用[J]. 城市轨道交通研究, 2012, 15(3): 41-44.
[23]	吕继东, 朱晓琳, 李开成, 等. 基于模型的CTCS-3级列控系统测试案例自动生成方法[J]. 西南交通大学学报, 2015, 50(5): 917-927.
[24]	赵显琼, 郑伟, 唐涛. 一种基于模型的形式化测试序列自动生成方法及在ETCS-2中的应用[J]. 铁道学报, 2012, 34(5): 70-80.
[25]	刘雨, 唐涛, 李开成, 等. CTCS-3级列控车载设备实验室互联互通测试方法[J]. 铁道通信信号, 2011, 47(12): 4-7.
[26]	Zhang Y, Tang T, Li K P, et al. Formal verification of safety protocol in train control system[J]. Science China Technological Sciences, 2011, 54(11): 3078-3090. DOI URL
[27]	梁茨, 郑伟, 李开成, 等. 基于路径优化算法的测试序列自动生成及验证[J]. 铁道学报, 2013, 35(6): 53-58.
[28]	陈鑫, 姜鹏, 张一帆, 等. 一种面向列车控制系统中安全攸关场景的测试用例自动生成方法[J]. 软件学报, 2015, 26(2): 269-278.
[29]	吕继东, 朱晓琳, 王海峰, 等. 基于UPPAAL-TRON的高速铁路列控系统非确定性时延一致性测试研究[J]. 铁道学报, 2016, 38(1): 54-64.
[30]	郭昊男. 新型列控系统车载ATP安全功能在线测试研究[D]. 北京: 北京交通大学, 2019.
[31]	魏柏全, 吕继东, 陈柯行, 等. 基于TAIO变异的CTCS-3列控系统测试案例生成方法[J]. 西南交通大学学报, 2020, 55(5): 937-945.
[32]	Gao J J, Lü J D, Chai M, et al. Train resources conflict detection of NGTC based on probabilistic timed automata[C]// Proceedings of the 2021 IEEE International Intelligent Transportation Systems Conference (ITSC). Piscataway:IEEE Press, 2021: 3951-3956.

软件开发活动	SIL 0	SIL 1	SIL 2	SIL 3	SIL 4
软件需求规范	R	R	R	HR	HR
软件架构	—	R	R	HR	HR
软件设计与实现	R	HR	HR	HR	HR
软件验证与测试	—	R	R	HR	HR
软件确认	R	R	R	R	R

软件开发活动	SIL 0	SIL 1	SIL 2	SIL 3	SIL 4
软件需求规范	R	R	R	HR	HR
软件架构	—	R	R	HR	HR
软件设计与实现	R	HR	HR	HR	HR
软件验证与测试	—	R	R	HR	HR
软件确认	R	R	R	R	R

应用	功能	ProB	NuSMV	UPPAAL	CPN	Atelier B	SPIN	Simulink
开发功能	规范/建模方式	文本	文本	图形	图形	文本	文本	图形
	自动代码生成	否	否	否	否	是	否	是
	文档/报告生成	部分	否	部分	否	部分	部分	是
	需求可追溯性	否	否	否	否	否	否	是
	项目管理	是	否	否	是	是	否	是
验证功能	仿真	文本/图形	文本	图形	图形	否	文本	图形
	形式化验证方法	多种	多种	多种	多种	一种	一种	一种
	基于模型的测试	是	否	是	否	否	否	是
语言表达能力	并发性	无	同步	同步	异步	无	异步	无
	时序性	否	是	是	是	否	否	是
	概率性/随机性	否	否	是	否	否	否	否
	浮点数支持	否	是	是	否	否	否	是

应用	功能	ProB	NuSMV	UPPAAL	CPN	Atelier B	SPIN	Simulink
开发功能	规范/建模方式	文本	文本	图形	图形	文本	文本	图形
	自动代码生成	否	否	否	否	是	否	是
	文档/报告生成	部分	否	部分	否	部分	部分	是
	需求可追溯性	否	否	否	否	否	否	是
	项目管理	是	否	否	是	是	否	是
验证功能	仿真	文本/图形	文本	图形	图形	否	文本	图形
	形式化验证方法	多种	多种	多种	多种	一种	一种	一种
	基于模型的测试	是	否	是	否	否	否	是
语言表达能力	并发性	无	同步	同步	异步	无	异步	无
	时序性	否	是	是	是	否	否	是
	概率性/随机性	否	否	是	否	否	否	否
	浮点数支持	否	是	是	否	否	否	是

项目名称	立项年份	资助机构	涉及研究对象	列控相关研究内容
EuroInterlocking	1999	国际铁路联盟	联锁	为联锁子系统开发功能需求和标准接口，并提供形式化功能需求描述方法和关键验证方法
AVACS	2004	德国科学基金会	ETCS	ETCS的自动设计、分析和验证技术
EuRailCheck	2007	欧洲铁路局	ETCS	ETCS规范的形式化建模验证方法及工具
Deploy	2008	欧盟	CBTC	开发形式化工程方法，集成建模、分析和代码生成一体的系统级形式化工具链
INESS	2008	欧盟	联锁	定义新一代联锁子系统的完整规范，开发支持需求规范形式化验证的工具链
OpenETCS	2009	德国联邦教育及研究部等	ETCS	为ETCS规范的形式化提供集测试验证与代码生成为一体的工具链
MBAT	2011	欧盟	CBTC、联锁	结合基于形式化模型的测试和静态分析方法，实现对列控系统的验证确认
OpenCOSS	2011	欧盟	ETCS、联锁	设计横跨航空、铁路、汽车的通用认证架构模型，引入“以模型为中心”的安全认证方法，建立开源的安全认证软件工具
SafeCap	2011	英国铁路安全、标准委员会等	联锁	支持形式化验证联锁子系统安全性的建模工具
RobustRail	2012	丹麦战略研究理事会	联锁	结合领域方法和形式化方法，提供列控系统的形式化开发与验证技术和工具
PERFECT	2012	欧盟	ETCS	为全面评估ETCS规范和欧盟各国铁路信号操作规则在安全方面的一致性提供形式化方法和工具
CRYSTAL	2013	西班牙工业、能源和旅游部等	ETCS、CBTC	集成系统需求管理、设计、安全分析和测试的工具链，改善互操作性，弥合系统开发过程中基于模型的系统工程（Model-Based System Engineering, MBSE）和基于模型的安全分析（Model-Based Safety Analysis, MBSA）之间的差距
EULYNX	2014	—	联锁	提供基于MBSE方法体系的列控地面子系统的建模规范，定义和标准化未来数字列控系统中的接口
X2Rail-2	2017	欧盟	ETCS	为ETCS的需求捕获、设计、验证和确认提出形式化方法，并应用于具有标准化接口和运营场景的系统开发
4SECURail	2019	欧盟	ETCS	提供最先进的形式化方法和工具的案例，提高系统需求规范的质量
X2Rail-5	2020	欧盟	ETCS	提供可应用于系统体系级（System of System, SoS）的形式化方法和工具链，指定标准接口的MBSE方法，实现需求的形式化和验证

列车运行控制系统的形式化研究进展与趋势

Research Progress and Trend of Formal Methods for Train Control System

RichHTML

PDF

可视化

摘要/Abstract

引用本文

使用本文

图/表 7

参考文献 32

相关文章 3

编辑推荐

Metrics

访问统计

友情链接

联系我们

官方微信公众号

[1]	詹乃军, 王戟. 复杂系统规约、分析与验证发展现状与展望[J]. 前瞻科技, 2023, 2(1): 7-22.
[2]	丁浩然, 王肇国, 付明, 陈海波. 形式化方法与系统软件：实践与发展建议[J]. 前瞻科技, 2023, 2(1): 33-45.
[3]	陈厅, 吴国政, 刘哲, 蒲戈光, 赵瑞珍, 刘克. NSFC形式化方法领域基金项目申请资助情况分析[J]. 前瞻科技, 2023, 2(1): 132-140.