前瞻科技

软件开发活动	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方法，实现需求的形式化和验证

项目名称	立项年份	资助机构	涉及研究对象	列控相关研究内容
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方法，实现需求的形式化和验证

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

PDF下载

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

前瞻科技 | 综述与述评 2023,2(1): 106-117

收起

前瞻科技 | 综述与述评 2023, 2(1): 106-117

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

全屏

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

作者信息

1.北京交通大学轨道交通运行控制系统国家工程研究中心，北京 100044

2.北京交通大学轨道交通控制与安全国家重点实验室，北京 100044

吕继东，教授，博士研究生导师。主要从事列控系统形式化建模、安全验证与测试的基础理论与实际应用等研究。先后主持和参与国家重点基础研究发展计划、国家自然科学基金重点面上项目、国家重点研发计划、北京市自然科学基金等国家级、省部级科研项目20余项。出版专著2部，发表论文60余篇，获授权发明专利10项，获软件著作权10项。获中国铁道学会科学技术奖一等奖1项。电子信箱：jdlv@bjtu.edu.cn。

唐涛，教授，博士研究生导师。北京交通大学轨道交通控制与安全国家重点实验室主任，北京市开放实验室“城市轨道交通自动化与控制实验室”主任。主要从事轨道交通列车运行控制等研究。入选新世纪百千万人才工程国家级人才。担任“交通信息工程及控制”国家级重点学科带头人、教育部自动化专业教学指导委员会委员、中国铁道学会理事。获教育部新世纪优秀人才支持计划、铁道部有突出贡献中青年专家、茅以升铁道科技奖和“北京市优秀教师”等荣誉称号。先后主持国家高技术研究发展计划、国家自然科学基金重点、国际合作项目等60余项。出版专著5部，发表论文200余篇，获授权发明专利9项，参与制定国家标准2项、行业规范14项。获国家科学技术进步奖二等奖2项、中国铁道学会科学技术奖一等奖2项、教育部自然科学奖一等奖1项、北京市科学技术进步奖一等奖2项、詹天佑铁道科学技术奖成就奖。电子信箱：ttang@bjtu.edu.cn。

通信作者:

^†

Research Progress and Trend of Formal Methods for Train Control System

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

Affiliations

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

出版时间: 2023-03-20 doi: 10.3981/j.issn.2097-0781.2023.01.008

文章导航

摘要

收起

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

关键词

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

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

引用本文

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

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

正文

收起

列车运行控制系统（简称列控系统）是通过技术手段控制列车运行速度，保证列车安全和高效运行的控制系统。随着计算机、通信、自动化等先进技术的广泛应用，列车运行控制系统已发展成为铁路运输系统的大脑和神经中枢，有效保证了列车高速、高密度的运行安全。

随着技术的发展，列控系统的功能和性能不断增强，系统结构与逻辑越来越复杂，设计缺陷易导致严重的灾难、事故和损失。作为一个典型的复杂安全苛求系统，寻找错误和安全隐患也比较困难，如何全方位、全角度地对系统的功能和特性进行验证、确认，从而确保系统的安全性，成为亟待解决的问题。

形式化方法以严密的数学理论和相关推理为基础，通过保证各开发活动的一致性的精化关系达到系统安全性保证的核心目标。在列控系统的开发过程中，可以在不同的阶段，以不同的形式和程度应用形式化方法。采用形式化方法的思想和技术发展起来的基于模型的正向设计方法已成为列控系统设计开发的重要手段^[1]。

经过多年的努力，中国列控技术整体已处于国际先进水平，有效保障了高速铁路、城市轨道交通的安全运行。为进一步提升轨道交通的安全和效率，列车运行控制技术正在向智能化、智慧化方向发展，欧洲已投入大量经费开展系统性研究，并提出与中国竞争技术前沿。中国亟须提升列控系统的正向研发能力，占据新一代列控技术前沿，避免未来被“卡脖子”。同时，随着列控系统的发展，不同学科、不同专业、不同背景的技术人员参与了列控系统研发，但如何统筹各方协作，准确无隐患地实现系统功能是亟须解决的难题，而国内形式化方法在轨道交通列控等领域的研究起步较晚，适用于列控领域的自主化建模语言和工具尚处空白。

基于以上问题，回顾分析国内外列控领域形式化方法的研究与应用现状，对比国内外形式化发展异同，给出适合中国列控系统形式化研究的发展建议，以期为中国列控领域和形式化领域的研究提供参考。

1 列控系统的发展

收起

1.1 发展历程及趋势

一般地，列控系统应包含车载设备、地面设备、通信设备等，其基本功能如下。

（1）将列车运行进路包含的道岔锁闭、轨道区段占用和信号机开放等相互制约的条件联系起来，在避免列车脱轨、相撞、追尾等安全约束下，通过排列进路和控制信号显示对列车的运行进行控制。

（2）通过给司机显示允许列车运行的信号、允许的最大速度、与目标点的距离，自动对列车的速度实施控制，一旦列车速度超过允许速度应自动实施制动控制，使列车减速乃至停车，防止与同一轨道运行的列车相撞或追尾，实现列车自动防护。

（3）替代司机实现自动驾驶、无人驾驶，利用自主感知前方障碍信息，利用线路信息、列车参数等实现对列车牵引、制动等自动控制，使列车始终处于最佳运行状态，提高乘客的乘坐舒适度和列车的准点率，节省能源。

（4）实时监控辖区内的列控相关设备和列车运行状态，及时调整列车运行计划，实现对列车运行的实时监督和调度指挥。

为适应铁路的发展，列控技术已先后经历了地面人工信号、地面自动信号、机车信号、自动停车装置、列车自动防护系统等阶段^[2]，从由信号显示传递行车命令，发展到以车载设备控制列车运行，进而逐步替代司机实现列车自动控制（Automatic Train Control, ATC）。这标志着列控技术由以重力机械型手动信号为主的机械阶段、以重力继电器为核心的自动信号电气阶段走向以计算机为核心的列车运行控制计算机阶段，如图1所示。

列控技术的发展愿景是以终端用户为中心，采用安全、可靠、韧性的轨道交通网络，运用智能感知、万物互联的通信、人工智能、云计算等颠覆技术，开发时空间隔防护、智能驾驶、超视距环境和障碍态势感知、危及行车安全的列车和设备设施状态监测等技术，构成智能化调度系统协调指挥下，智能化列车自主安全驾驶的新一代运行控制系统。

1.2 计算机时代列控系统的特点

在现代列控系统中，计算机已经成为承载安全关键功能的重要组件。与传统列控系统相比，计算机时代列控系统的特点如下。

1）具备混成特性的复杂分布式系统

列控系统应用了先进的计算机技术和通信技术使得系统本身趋于集成化、模块化、专业化、分布自治化。依靠高效的嵌入式处理器和软件应用，系统设备不断朝小型化、集成化发展。即使是最简单的计算机系统也包含数以万计的元器件和复杂的行为状态。模块化使得系统中各设备或单元的功能更加明确、专一，并且系统在组合、分解、更换单元时更为简捷方便，这也造成了系统中的模块数量增加，模块间接口增多，不仅交互关系更加复杂，而且模块间的兼容性问题凸显。此外，由于先进的车载控制系统的出现，列控系统由之前的轨道区段占用状态、信号机显示灯离散状态迁移系统转变为结合了列车速度及位置等连续变化与系统离散控制命令的混成系统。

2）安全攸关与故障-安全原则

列控系统是典型的安全攸关系统，自动列车防护（Automatic Train Protection, ATP）和车站计算机联锁（Computer Interlocking, CI）等核心设备（系统）需要达到最高安全完整性等级（Safety Integrity Level, SIL）4级。传统电气化列控设备利用设备故障时电气化参数不对称的特点，在故障时导向安全侧，具有本质故障-安全的特征。而列控系统强烈依赖于计算机设备，硬件构成决定了其不具有故障不对称的特点，无法实现本质故障-安全。目前，列控系统主要采用冗余技术及主动控制的方式来实现本质故障-安全。主动控制是指通过主动识别故障，并在发现故障后主动采取措施应对以保障安全。

3）软件在系统功能实现中占据重要角色

计算机系统的功能实现是在通用设备的基础上直接以指令或流程的形式“书写”设计思想（即专门软件实现），而不需要每次都针对特定应用需求从零开始，通过一个个机械或电气组件逐步搭建。显然，作为典型的计算机系统，现有列控系统比以往列控系统更具备可移植性、扩展性、通用性。同时，在列控系统中，计算机软件越来越多地参与系统的控制和管理，承担了列车运行控制安全逻辑的计算等关键功能，并且在系统功能中的比重逐步上升。

4）系统功能的正确性依赖于特定的数据^[3]

计算机软件的介入使得列控系统软件功能出现了一般通用控制逻辑与具体线路配置数据相分离的设计。列控系统是一个典型的数据驱动控制系统，其根据接收到的移动授权（Movement Authority, MA），使用静态数据、动态数据等实时计算控制列车的模式曲线，监控列车速度，确保列车安全高效行驶。如果列控数据不正确，则会直接导致整个模式曲线计算不准确。在该曲线的指引下，可能会造成列车异常制动、停车，严重时还会导致追尾、脱轨等事故发生。

1.3 列控系统形式化研究的必要性

从系统实现的角度来看，列控系统的控制逻辑、控制算法依赖于软件实现，控制软件的故障会直接造成列控系统的功能失效。形式化方法可以精确定义列控系统的结构、组成、功能、安全属性，使得所有人员对系统的理解达成一致，排除自然语言所带来的二义性问题。同时，形式化方法可以严谨地分析系统的安全性、可靠性等性能，保证设计规范和程序代码的一致性。

2001年，欧洲电工标准化委员会（European Committee for Electrotechnical Standardization, CENELEC）推出的研发标准EN 50128推荐在列控系统全生命周期研发中使用形式化方法^[4]。EN 50128采用SIL表示列控软件功能失效的概率。根据不同的功能失效概率由高到低，EN 50128将铁路信号系统软件划分为SIL 0~SIL 4共5个安全完整性等级。如表1所示，EN 50128强烈推荐在SIL 3级或者SIL 4级系统的研发过程中，使用形式化方法进行描述和分析。

随着列控系统功能结构的发展，开发周期延长，成本消耗加大。基于形式化模型的开发依据模型来验证软件系统的需求及设计方案，产生和调试软件程序代码的方法，简洁高效，提升开发效率，降低开发成本，已在列控^[5]、核电^[6]、航空航天^[7]等安全攸关领域获得成功应用。因此，需要在既有开发方式基础上，更加注重以形式化模型驱动的列控系统全生命周期的开发方法，在保证系统安全性和正确性的同时，更有利于列控技术创新突破。

2 国外列控领域形式化研究进展

收起

2.1 形式化方法早期应用

早在20世纪80年代，法国就将B语言应用于列控系统开发^[8]。1988年，巴黎公共交通运营商RATP、阿尔斯通和MATRA Transport采用B语言研发了列车自动防护系统SACEM，由21000行Modula-2代码组成，其中63%被视为安全关键代码，并且也经过B语言形式规范描述和验证，是B语言的第一个广受好评的工业应用^[9-10]。

1998年，由西门子公司采用B语言开发的基于通信的列车自动控制系统（Communication based Train Control System, CBTC）被应用于巴黎14号线。这种使用形式化方法进行开发的安全性在补充测试阶段（验证测试、集成测试等）得到了确认，结果在这个系统上没有发现任何故障，因此奠定了在CBTC的研发中应该使用形式化方法的趋势。B语言的成功应用影响了CENELEC发布的EN 50128指南的制定，在列控领域产生了重大影响^[11]。

2.2 形式化方法的应用现状

经过多年形式化方法在列控领域的研究，大量的形式化语言和工具被应用于列控系统开发，一方面推进了列控系统的研发水平，另一方面也促进了形式化方法的发展^[12]。

列控领域形式化研究主要针对架构、详细设计、需求、测试等系统开发阶段^[1]。由于不同开发环境和开发阶段对形式化应用的需求，催生了不同的形式化语言、多种形式化工具和大量形式化相关技术的应用。

1）形式化语言

形式化语言的应用通常分为两种：一种是根据现有的语言特性，选取合适的应用与列控领域，如有限状态机（Finite-State Machine, FSM）和通信顺序进程（Communicating Sequential Processes, CSP）的应用;另一种是针对列控领域特点开发专用语言。基于此，欧盟Shift2rail项目对形式化方法1989—2020年在列控领域的应用进行了系统分析研究^[1]。

如图2所示，从调研的形式化语言来看，总体应用最多的是基于统一建模语言（Unified Modeling Language, UML），其次是B语言和Petri网，其他语言包含SMV等30余种语言。此外，Ferrari等^[1]发现工程应用中主要采用的是B语言，这与B语言在列控工程的成功应用有很大关系。

2）形式化工具

关于形式化工具的应用，从开发功能、验证功能和语言表达能力3方面进行了总结，如表2所示。由表2分析发现，主流形式化工具缺乏对开发功能的支持，尤其存在于自动代码生成和需求可追溯性这两方面，Simulink工具在支持当前列控领域开发方面性能优良。

在验证功能方面，基于模型的测试只有部分工具支持，ProB和UPPAAL工具功能相对更完善。在语言表达能力方面，UPPAAL的性能更加优良，尤其在概率性和随机性描述方面。当前形式化工具发展已经成熟，对于铁路发展非常有利，大多数考虑的工具都是成熟和整合的产品，具有足够的行业认可度^[1]。

3）形式化相关技术

欧盟Shift2rail项目对11种应用较多的形式化相关技术进行了系统分析^[1]，如图3所示。从研究技术来看，与验证相关的技术占比最大的是模型检验，其他应用较多的技术还有基于模型的开发和仿真。与代码相关的技术（如静态分析、代码生成）应用较少。综合分析来看，技术多样性表明列控开发是大量不同技术的实践领域，但形式化方法通常应用于抽象的高级模型，只有很少研究考虑代码层级。

2.3 形式化方法在列控系统中应用的研究项目

多年来，很多研究部门和列控相关机构都在关注形式化方法的应用，资助开展了多个项目，针对包括欧洲列车运行控制系统（European Train Control System, ETCS）、CBTC、联锁子系统在内的研究对象，研究形式化方法和工具在列控中的应用。以时间顺序，对列控领域形式化方法应用研究相关项目进行了总结，如表3所示。

国外列控形式化研究主要集中在欧盟以及欧洲多个国家。通过分析发现，需求规范形式化和验证贯穿了多年的研究，是各研究机构都非常重视的方面。此外，欧盟为推动ETCS在欧洲各国的应用，在需求规范、系统设计、代码生成、测试验证等多个开发阶段都资助了相关项目，主要关注形式化相关技术应用、工具、工具链的开发构建。值得注意的是，近年来，包括RobustRail、EULYNX、X2Rail-5在内的多个项目都重点关注基于模型的开发和MBSE。

MBSE是建模方法的一种形式化表达，用以支持从概念设计阶段到开发、应用、维护等阶段，以及分析、验证和确认等活动^[13]。如图4所示，相较于传统列控系统研制模式，MBSE以形式化方法为基础，将列控系统的表达由“以文档为中心”转变为“以模型为中心”，基于UML，可以被各角色研发人员和计算机所理解，为研发组织内的高效沟通和协同奠定基础，有效解决了列控系统研发的复杂性和不确定性。

3 国内列控领域形式化研究与应用

收起

基于形式化理论的列控系统生命周期研发模型主要包含需求规范分析、系统设计实现和系统测试验证3个关键阶段。需求规范分析是根据用户需求，分析需求中要求的列控产品性能、特性、规范等，并将这些需求形式化，采用形式化方法转化为需求规范文档，获得明确细化的需求模型;系统设计实现是基于系统软件的形式化需求、架构设计、模块设计，采用形式化开发工具对系统的架构和行为等建立形式化模型，手动或者自动生成底层代码的过程;系统测试验证依据系统架构设计，采用形式化方法对系统性能进行测试，验证功能安全特性，测试运行状态和检查数据，对模型进行调试，以确保满足系统软件的需求。

3.1 需求规范分析阶段

2008—2017年，北京交通大学在国家科技支撑计划“CTCS-3级列控系统测试评估认证平台及评估测试（测试评估平台）”等项目支持下，联合中国科学院软件研究所等单位，针对列控系统规范中安全攸关的时序控制行为、实时控制行为、混成控制行为，提出了基于混合通信顺序进程理论（Hybrid Communication Sequential Process, HCSP）的高铁列控系统需求规范建模方法^[14]，建立涵盖列车运行全过程的混成形式化模型。在此基础上，利用混成霍尔逻辑（Hybrid Hoare Logic, HHL）对系统行为进行了验证，确保系统需求规范的一致性和无二义性^[15]。相关成果支持制定了适合高速铁路的中国列车运行控制系统第三级系统规范（Chinese Train Control System Level 3, CTCS-3），指导CTCS-3级列控系统设计及运用^[16]。

2012—2019年，华东师范大学与卡斯柯公司在国家自然科学基金重大研发计划“不确定环境下可信国产城轨控制系统（iCMTCt）构造关键技术研究”等项目的支持下，针对列控核心控制软件进行了形式化方法建模、验证、测试的关键技术研究，提出了联锁系统领域语言SafeNL描述安全需求，并将其转换为时钟约束规范语言（Clock Constraint Specification Language, CCSL）来描述联锁系统强时间约束特性，进而验证需求满足性^[17]。提出了采用问题框架（Problem Frames, PF）建模和分解需求，以及自动生成高安全性的应用程序开发环境（Safety-Critical Application Development Environment, SCADE）模型的区域控制器安全需求验证方法^[18]。相关成果支持了全套TRANAVI型列控系统自主研发。相关系统产品已成功部署于上海轨道交通17号线和东非地区首条城市轻轨——埃塞俄比亚首都亚的斯亚贝巴轻轨等诸多国内外线路。

3.2 系统设计实现阶段

2010年，北京交通大学在自主研发设计的CBTC列控系统中的区域控制器（Zone Controller, ZC）子系统开发中应用了SCADE软件，基于SCADE的开发环境进行区域控制器研发和测试^[19]。

2015—2018年，北京交通大学在国家自然科学基金“本质特征驱动的高铁列控系统安全逻辑建模理论与方法”项目的支持下，围绕列控系统安全逻辑的验证问题，考虑SCADE支持基于严格语义的模型验证和能够直接生成满足EN 50128标准规范代码的优势，建立了基于SCADE的进路控制逻辑模型、列车管理和超速防护控制逻辑模型^[20]。提出了基于图论的形式化列控数据模型及混成运行时验证方法，实现了列控数据正确性自动化验证^[21]。相关成果支持了中国列控系统的设计、开发、分析验证与运行安全，有效解决了现阶段系统存在的设计型缺陷问题。

3.3 系统测试验证阶段

2009—2014年，北京交通大学在国家高技术研究发展计划（简称“863”计划）“高速铁路列车运行控制系统互联互通测试与评估技术”等项目的支持下，针对高速铁路列控系统实验室测试研究，形成了涵盖470个测试案例集的原铁道部规范《CTCS-3级列控系统测试案例》，是CTCS-3级列控系统室内仿真、现场试验及联调联试的指导性文件。研究了基于UML^[22]、时间自动机（Timed Automata, TA）^[23]、有色Petri网（Colored Petri Net, CPN）^[24]的列控系统关键设备测试案例自动生成方法，并搭建了列控系统车载设备独立第三方互联互通测试平台。受中国国家铁路集团有限公司委托，作为独立第三方测试机构已对所有列车车载设备厂家进行了互联互通测试工作，解决了影响跨线运行的问题，测试成果已在武广、广深线得到验证^[25]。

2011—2013年，华东师范大学、北京交通大学、清华大学等单位在“863”计划“面向信息-物理融合的系统平台”项目的支持下，针对轨道交通网络物理系统（Cyber Physical System, CPS）的信息物理融合及安全的关键属性，采用接口自动机（Interface Automata, IA）、进程或协议元语言（Process or Protocol Meta Language, PROMELA）模型、模型检验器SPIN构建了列车运行控制系统关键属性建模验证工具链原型系统，有效地描述安全协议，验证死锁、活锁等属性^[26]，实现了基于CPN的测试案例及序列生成工具，并将测试案例及序列成功应用于搭建的高速铁路无线闭塞中心测试平台^[27]。

2014—2018年，中国科学院软件研究所、北京交通大学、南京大学等单位在国家重点基础研究发展计划“安全攸关软件系统的构造与质量保障方法研究”项目的支持下，设计并实现了硬件在环列控安全攸关软件支撑验证平台;结合UML图形化、能表达软件设计中的动态与静态信息特点，通过扩充时间特性描述机制和事件驱动机制，建立列控安全攸关场景模型，并生成了测试用例^[28];以CTCS-3级列控系统中列车异常紧急制动的真实事件为例，建立时间自动机车载子系统需求的模型，并采用模型检验找到了系统需求中的错误，据此对系统进行修改^[29]，实现了列控关键部件运行的有效监控和列控系统失效致因准确分析。针对高速铁路列控系统非确定性时延一致性，提出结合时间自动机理论的一致性在线测试方法，并应用在无线闭塞中心子系统仿真测试，找出了测试模型与测试需求中不一致的地方^[29]。

2018—2021年，北京交通大学在国家重点研发计划“基于动态间隔的运能可配置列车运行控制技术”的支持下，针对新型列控系统的在线测试、完备测试案例生成、测试平台构建等理论和技术开展了深入研究，创新性地提出了基于在线一致性测试理论的新型列控系统测试方法^[30]，解决了“以车载为核心”的新型列控系统功能和性能测试全的难题。此外，还进行了基于时间自动机的变异测试^[31]与资源冲突分析^[32]。相关成果支撑了整套新型列控设备的研制、实验室测试及现场试验，形成了中国首创的具有轨旁最少化、通信多模化、车载中心化、运能适配化、维护智能化特征的动态间隔新型列控系统。

4 国内外列控领域形式化研究差异

收起

通过分析可以看出，国内外在列控领域形式化研究和应用中存在相同点，也有很多不同的地方。

国内外在列控领域对已有的大量形式化方法、工具、相关技术进行了研究并使其得以发展，对形式化在列控领域的适应作出了很大贡献。国内在列控领域形式化研究中，主要是在已有的形式化研究基础上进行适应性分析，将更适用的形式化研究应用于列控。国外除了与国内相同的适应性分析以外，针对列控领域特性，还开发了很多专用于列控的形式化语言和工具等^[12]。在项目研究方面，国内列控形式化研究项目主要以解决实际问题为主，主要针对如列控系统需求规范和测试验证等实际问题进行。国外在针对列控系统形式化研究方面，旨在开发适用于列控开发的统一形式化标准、方法或者工具。

综合分析来看，目前国内外主要将形式化方法应用于系统的需求、设计和测试，对底层代码生成的研究较少，代码生成往往还需要人的参与。国内目前只是应用形式化方法，还没有开始体系化的研究。而国外，特别是欧盟，在列控领域对形式化方法、形式化工具、形式化应用的研究较为连贯，是体系化的研究，并且基于MBSE的开发理念逐渐应用于列控领域研究中。与此相对的是，当前国内列控领域中MBSE理念的研究尚属空白。此外，在标准规范方面（如EN 50128），国外对形式化方法进行了体系化的分析和推荐，有助于列控领域的发展，目前国内在这方面还在探索阶段。

5 中国列控领域形式化发展建议

收起

综上所述，中国未来的列控系统形式化研究应以满足轨道交通发展战略的需求为指引，力求进一步提升列控领域创新能力、科技实力，实现列控领域高水平自立自强，支撑建设科技强国、交通强国。具体发展建议包括以下3方面。

1）通过加强顶层设计，推动形式化技术研究与应用

针对列控系统的发展趋势，面向列控系统由于多学科、多研发阶段、多研发人员等现状下导致的系统研发衔接困难，考虑应用场景类型多和列控系统功能需求复杂等特征。要打造系统化的列控领域形式化研究，通过加强国家铁路部门、铁路研究机构、铁路厂商等与形式化研究机构的协同合作，考虑形式化研究在列控领域的适应性以及参与人员的接受度等因素，统筹列控系统形式化研究方向，推动基于MBSE列控系统研发理念的应用。重视列控研发中形式化方法研究和形式化技术研发，降低研发和使用人员掌握列控系统形式化技术的学习成本，提高管理开发复杂列控系统工程的能力，保证系统设计完善和无歧义，缩短开发周期和降低开发成本。

2）通过强化自主创新，推动技术装备高质量发展

当前国内列控领域应用的形式化理论和方法并不是为列控研究专门进行设计或者研发的，这导致采用形式化方法的列控研究往往出现精通形式化理论研发人员不了解列控系统，了解列控系统的研发人员不精通形式化方法，为列控系统研发带来了很大的困扰。并且当前列控领域应用的形式化方法仅仅针对系统研发周期的一个或者几个阶段，支撑列控系统全生命周期研发的形式化方法工具或形式化方法工具链还未成型。因此，要增强形式化技术自主创新能力，重视形式化语言、形式化方法、形式化工具等基础性、共性的列控研究发展，构建国内列控研发形式化工具链，提升国产列控领域形式化技术在列控领域研究中的主体作用，形成列控研发技术装备的高质量发展。

3）通过体制优势，开展产学研协同人才培养

由于列控系统的动态发展和交通运输日益增加的需求，对应列控领域形式化方法的研究是一个适应并超前时代的持续性的过程，因此培养一批列控领域形式化研究的人才队伍是非常重要的。所以，要充分发挥中国举国体制机制优势和在轨道交通战略性需求建设方面集中力量办大事的能力，通过国家立项的宏观牵引，提高科研院所、高校、企业的联合创新能力，从而推进列控系统形式化研究的人才队伍与技术装备等的协同发展。从人才队伍建设和培养的体制机制等方面进行探索，形成列控领域形式化研究人才有序衔接、梯次配备、合理分布的格局，从而打造出一支具有形式化研究素养的列控领域研发人才队伍，助力中国列控系统发展。

6 结束语

收起

形式化方法在保证列控准确开发和安全运行、减少列控系统开发成本、提高列控系统开发效率等方面具有无法替代的作用，是列控领域的关键技术。当前，中国列控技术正在加快从自动化向智能化迈进，与此同时面临着系统动态发展挑战，亟须突破形式化等关键技术。因此，大力发展列控领域形式化方法与技术，准确把握列控形式化研究的关键趋势，采用基于模型的系统工程设计方法，实现关键技术设备自主化，显著提升应用水平，将是中国列控领域发展实现持续创新的有效途径。

基金

收起

国家自然科学基金(52272329)
北京市自然科学基金(L201004)

参考文献

收起

文献

收起

参考文献引证文献

排序方式：

[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]

Claudio M

, Fantechi

, Martelli

, 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

. The B-book: Assigning programs to meanings[M]. Cambridge: Cambridge University Press, 1996.

[9]

Fantechi

. 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

, Dehbonei

, Mejia

. 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

. 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.

https://doi.org/10.1016/S0022-3093(02)00949-3

[13]

Laporte

C Y

, Houde

, Marvin

. 6.4.2 systems engineering international standards and support tools for very small enterprises[J]. INCOSE International Symposium, 2014, 24(1): 551-569.

https://doi.org/10.1002/iis2.2014.24.issue-1

[14]

吕继东, 李开成, 唐涛, 等. 基于混合通信顺序进程的高速铁路列控系统形式化建模与验证方法[J]. 中国铁道科学, 2012, 33(5): 91-97.

[15]

Zou

, 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

, 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

, Chen

, 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

, Wang

H F

, Chai

, 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

, Tang

, Li

K P

, et al. Formal verification of safety protocol in train control system[J]. Science China Technological Sciences, 2011, 54(11): 3078-3090.

https://doi.org/10.1007/s11431-011-4562-2

[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

, 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.

2023年第2卷第1期

PDF下载

2485

1221

引用本文

BibTeX

文章信息

doi: 10.3981/j.issn.2097-0781.2023.01.008

接收时间：2022-12-26
出版时间：2023-03-20
发布时间：2023-03-27

补充材料

相关文章

文章信息

作者

出版历史

收稿日期：2022-12-26
修回日期：2023-02-01

基金

国家自然科学基金(52272329)

北京市自然科学基金(L201004)

作者信息

1.北京交通大学轨道交通运行控制系统国家工程研究中心，北京 100044

2.北京交通大学轨道交通控制与安全国家重点实验室，北京 100044

通讯作者:

^†

参考文献

分享链接

https://castjournals.cast.org.cn/joweb/qzkj/CN/10.3981/j.issn.2097-0781.2023.01.008

分享至

全文二维码

扫描看全文

引用本文

BibTeX

本文的引用情况

表12种不同金属材料的力学参数

科 Family	属数 Number of genus	种数 Number of species	占总种数比例 Percentage of total species (%)	属 Genus	种数 Number of species	占总种数比例 Percentage of total species (%)
鹅膏菌科Amanitaceae	2	11	5.26	鹅膏菌属 Amanita	10	4.78
小菇科 Mycenaceae	2	12	5.74	丝盖伞属 Inocybe	5	2.39
多孔菌科 Polyporaceae	8	14	6.70	蜡蘑属 Laccaria	5	2.39
红菇科 Russulaceae	3	23	11.00	小皮伞属 Marasmius	6	2.87
				小菇属 Mycena	11	5.26
				光柄菇属 Pluteus	5	2.39
				红菇属 Russula	17	8.13
				栓菌属 Trametes	5	2.39

关闭全屏

BibTeX
EndNote
RefWorks
TxT

访问统计

友情链接

联系我们

官方微信公众号