产品
本期，将进一步拓展Ansys SCADE在轨交列车控制系统中的应用，全文通过首先介绍OpenETCS项目的背景及发展，然后描述OpenETCS项目中工作包的划分和工作流的概况，进而解释SCADE为什么能在OpenETCS项目的工具选型中脱颖而出。最后介绍Systerel公司是如何使用S3(Systerel Smart Solver)引擎对SCADE进行形式化验证的。
1OpenETCS诞生背景
过去150年来，欧洲铁路分别在各个国界内各自发展，形成了各种不同的信号和列车控制系统，这严重阻碍了跨境交通。欧盟决定改善铁路部门的互操作性，因此提出了欧洲列车控制系统(ETCS：European Train Control System)，它作为欧洲铁路交通管理系统(ERTM: European Rail Traffic Management System)的一部分，旨在取代几乎所有欧洲国家遗留的列车控制系统，统一欧洲铁路网，允许列车运营商使用配备单一信号系统的铁路车辆在整个欧洲运行。
图表1: ETCS欧洲铁路交通管理系统的现状与未来发展预期
ETCS由基础设施组件和车载单元 (OBU: On board Unit) 组成。其系统需求规范 (SRS: System Requirements Specification) 主要由6个主要欧洲铁路信号制造商合作制定。这些公司成立了一个名为UNISIG的协会，与欧盟委员会和铁路运营商机构密切合作，管理和协调这些活动。然而，在开发ETCS过程中面临了不少挑战，由于解释标准中的差异，ETCS与轨旁设备间的互操作性 (Interoperability)尚未实现。此外，从各国铁路系统转换到ETCS的成本也很高。尽管不同欧洲铁路技术标准的多样性可能会给完全统一的ETCS带来难以逾越的障碍，但建立高水平的互操作性是可行的。
图表2: ETCS中基础设施组件和车载单元的现状与未来发展预期
当考虑到ETCS概念的真正核心，即其统一的软件时，软件解决方案的作用是决定性的。创建统一软件的关键在于开放的解决方案，使得所有参与者都可以自由访问该解决方案。这是产生OpenETCS思想的前提。
2009年，德国铁路公司 (Deutsche Bahn) 启动了一个项目，目标是将ETCS车辆成本降低到至少与传统列车保护系统相当的水平。基于德国铁路公司十多年来在自由许可和开源软件下发布软件的经验，他们提出了一个相应的ETCS解决方案的想法，即OpenETCS。
很快，英国铁路公司(ATOC：Association of Train Operating Companies)，德国铁路公司(Deutsche Bahn)，荷兰铁路公司(NS: Nederlandse Spoorwegen)，法国铁路公司(SNCF：Société nationale des chemins de fer français)和意大利铁路公司(Trenitalia)这五家欧洲铁路决定共同定义和推广OpenETCS项目。截止到2015年，累有计7个国家(荷兰、比利时、英国、法国、德国、意大利和西班牙)的4个研究所，5家大学，22家企业共31个合作方宣布参与到OpenETCS项目中来。
2OpenETCS简介
确切的来说，OpenETCS是一个项目，而不是一个组织。该项目的目标是为欧洲列车控制系统提供“开放的证明”(Open Proof)，证明可以：
- 工具链将支持ETCS系统需求的 形式化规范和验证
- 符合ETCS的 代码自动生成和验证
- 基于模型的测试用例生成和执行
2011年底以来，OpenETCS项目开发已作为ITEA的项目获得了公共资助。
* ITEA是一个软件创新领域的跨国和行业驱动的研发与创新项目，使一个由大型工业、中小企业、初创企业、学术界和客户组织组成的全球性知识社区能够在资助的项目中进行合作，这些项目将创新理念转化为新的业务、工作、经济增长和社会效益。由于ITEA是一个EUREKA集群，该共同体基于EUREKA原则在欧洲成立，并向全世界的参与者开放。
** 尤里卡计划 (EUREKA) 是欧盟的一个研究组织，成立于1985年。尤里卡计划的宗旨着重于市场导向的产业技术研究发展，其他领域例如军事，则不会涉入，目前每年约新增一百多个子计划。
2015年12月，耗资近1900万欧元，耗费达156人年的工作量的OpenETCS项目的开源内容开发结束。其开源内容可在ITEA或github上查阅。
3OpenETCS项目成果及后续发展
OpenETCS的第一个成功商业应用是德国的柏林-慕尼黑高速铁路的ICE列车上实施的ETCS。根据ITEA发布的报告，OpenETCS的成果包括但不限于：
OpenETCS开发成果将延伸至后续的Horizon 2020项目，ASTRail的Shift2Rail项目等，将其形成的技术、标准与协作模式推向更深和更高的层次。绝大部分项目的成果都可以在相关网站上访问。
图表5: OpenETCS项目成果的后续演进
2019年2月，瑞士铁路公司 (SBB)宣布加入OpenETCS。SBB已经通过SmartRail 4.0和” RCA计划” 与其他铁路和基础设施管理人员合作，正致力于开发下一代列车控制和交通管理系统 (Reference CCS Architecture) 。SBB希望通过与OpenETCS成员的密切合作，有助于开发和验证其系统。
* SmartRail4.0是一个行业计划，它根据整个系统优先安排和集中资源。合作的目的是共同开发各铁路相关公司支持的解决方案，致力于铁路生产的广泛数字化和自动化。
4OpenETCS中的工作包与工作流
OpenETCS项目分为4大块7个工作包(WP: Work Package)及工业用户测试案例，分别是：
图表6: OpenETCS项目的工作包
EN 50129的系统生命周期和EN 50128的软件开发生命周期流程的两个最重要的要素是将生命周期划分为若干个定义明确的阶段，并专注于编写和记录开发过程的文档。这有助于促进安全、验证、确认和评估活动，并提升用户利用最佳的实践来开发关键系统的信心。为了实现这一目标，必须按照CENELEC标准提供的约束条件，为OpenETCS定义适当的生命周期，并为参与者分配适当的角色和职责。
项目的输入要素为黄色，规范和设计活动为蓝色，验证和确认活动为红色，安全相关的活动为绿色。其中
系统阶段分为3个步骤：
步骤0：都是需求和规范的文档输入
步骤1：系统分析
步骤2：子系统设计的形式化
软件阶段：分为2个步骤，从系统模型并行开发了两种方法。
步骤3：软件设计
步骤4：软件代码生成
如下方图表8所示的深蓝色阶段的活动需要大量建模，因此需要选择合适的平台和工具进行开发。平台选用Eclipse没有太大争议。而开发工具方面选择面较多，OpenETCS进行了多轮评审才有结果。
图表8: OpenETCS项目工作流中需要大量建模的4个部分
5OpenETCS中的工具选型
下图是EN50128的标准软件开发流程
图表9: EN50128的标准软件开发流程
针对EN50128的标准软件开发流程，OpenETCS对下列开发工具进行了初步筛选，蓝色代表入选的系统设计工具，绿色代表入选的软件设计工具，黄色代表入选的代码设计工具或语言，白色代表落选的工具。各个工具对每列所标识出的功能进行评估，+号表示完全满足(即该工具可用)，o标识部分满足，-号表示不满足(即该工具不可用)。T表示文本型工具，M表示支持数学符号，G表示支持图形建模。
图表10: OpenETCS项目开发工具的选择评估表
下图是针对EN50128的传统验证流程
图表11-1: EN50128的传统验证流程
而OpenETCS更强调使用形式化的方法，EN50128改进的以形式化方法为主的验证流程如图表11-2
图表11-2: EN50128的形式化方法的验证流程
针对EN50128的以形式化方法为主的验证流程，OpenETCS对下列工具进行了初步筛选，蓝色代表入选的支持形式化的系统设计工具，绿色代表入选的支持形式化的软件设计工具，黄色代表入选的支持形式化的代码设计工具或语言，白色代表落选的工具。其中对每列名称所对应的功能，+号表示完全满足(即该工具可用)，o标识部分满足。
图表12: OpenETCS项目验证工具的选择评估表
经过几轮的筛选，共有13款(种)软件入围，进入下一轮工具选型评审
图表13: OpenETCS项目工具初筛入选的13款工具
图表14: OpenETCS项目中8款工具被否决的原因
剩余的软件进入最终评审，从下图可以看到SCADE是剩余的唯一的可以大幅度跨越子系统设计、软件设计和软件代码生成三个阶段的形式化工具，覆盖面广，适用性高。
图表15: OpenETCS项目工具选型的6进1阶段
经过参与方Benchmarking，Assessment，Decision Meeting和Composition of Toolchains四轮活动，最终选择Papyrus和SCADE两款软件共同作为OpenETCS的开发工具。工具的评估内容可以通过链接查阅
https://github.com/OpenETCS/model-evaluation/tree/master/model
工具选型结束后，OpenETCS定义的开发和验证工具链平台如图表16
图表16: OpenETCS项目的最终工具链选择
其中，需求及需求管理工具是黄色的，Eclipse平台是深蓝色的，验证工具是桔色的。使用SCADE的RM-Gatway工具进行需求管理。使用Papyrus进行系统设计，由于SCADE System具有Eclipse接口和Papyrus接口，通过SCADE自带的如下功能，可以增强Papyrus设计的系统功能
在软件设计阶段，使用SCADE进行形式化建模和后续验证，其中可以用到如下模块：
6SCADE在OpenETCS中的形式化验证
OpenETCS项目是开源的，各合作方可以选用特定的验证工具对设计完毕的SCADE模型等文件进行分析和验证。在OpenETCS项目的验证和确认总结报告中，综述了6个阶段的结果，分别是
阶段3~阶段6和SCADE工具有关联，负责这方面工作的包括德国罗斯托克大学(University of Rostock)，德国航天中心(DLR)，法国Systerel公司，德国Fraunhofer FOCUS公司和意大利通用电气交通(GE Transportation)。本节主要介绍下法国Systerel公司是如何使用形式化工具S3(Systerel Smart Solver)对软件组件的两个功能进行模型检查的（有关模型检查的介绍，详见往期：嵌入式系统 | 基于SCADE模型的形式化方法）
第一个输入是SCADE模型，将会被转换为HLL模型，第二个输入是由HLL语言描述的安全属性和环境假设或约束。两个输入合并为一个HLL文件后传给S3引擎，通过BMC策略在指定的深度分析后，得出结果。如果结果失败，输出反例；如果结果正确，安全属性得证。
首先可使用S3引擎内置的属性检查(proof obligations)快速查找的SCADE模型中的错误，以评估HLL模型的定义是否正确：内置的属性检查包括
此外，从一种语言到HLL的转换本身，也可以生成要由S3分析的安全属性，以检查代码对于源语言有无未定义的行为。例如，C转换器添加了一些安全属性，以确保与C99标准的一致性。
Systerel共对5个案例进行了形式化分析，本文抽取其中两个来介绍。
6.1Systerel进行形式化分析案例1：isolate操作符
图表19: isolate操作符的SCADE模型功能
转换为HLL后的对S3引擎的输入如图表20，内容可通过直接阅读绿色的文本注释获取。
图表20: isolate操作符转换为HLL后的对S3引擎的输入
经S3引擎分析，Isolate mode的属性得证
6.2Systerel进行形式化分析案例2：验证非形式化规约（例如流程图）
图表21: 非形式化规约图Start of mission in Level 0 in the Subset 26 input specification
例如，当刚开始执行任务时，列车处于静止状态，车载系统处于待机模式(SB：Stand-by mode)，列车数据(识别号、长度等)得到验证。一旦司机下启动指令按钮，车载系统就向司机发送确认信息请求，然后等待接收到此确认消息，以切换到适当的模式。在图表21中，当选择0级时，车载系统应切换到不适合模式（UN: Unfitted mode）。预期的过程如图表22所示。
图表22: 简化的操作流程图:Start of mission in Level 0
对于这种复杂情况，要验证的SCADE模型不能被视为黑盒(black box)，应分析内部状态，明确定义SCADE和HLL模型之间的等价性，步骤如下:
图表23: SCADE模型局部Start of Mission
值得一提的是，反例中包含特定的输入值，这些值会引起正确等价性的错误证明。这可能是由于引擎推导出的实际中并不存在的输入值。在这种情况下，可以在HLL模型中添加约束。在该例中，可以假设在模式管理期间，level输入值与值“L0”保持不变，即列车数据保持不变且有效。
在验证过程中，添加约束将引起验证系统其余部分的新属性。其他假设可以集成到属性中进行验证，当H是假设时，证明目标P被替换为证明目标H，即H=>P。只要引入其他属性来覆盖H为假的情况，就不再需要其他外部验证来测试H。通常，这些假设的定义是为了消除可能的行为，而不是与原验证主题直接相关的行为。
在本例中，我们假设在模型的输入中不会检测到系统故障，因此在检查切换到不适合模式(UN: Unfitted mode)时，不考虑引起系统故障模式的所有行为。系统故障的发生已被其他形式化分析的安全属性覆盖。在此给定的输入约束和假设条件下，证明了两种状态机的行为是等价的。内容可通过直接阅读绿色的文本注释获取。
图表24: Start of Mission模型转换为HLL后的对S3引擎的输入
7小结
形式化方法在诸如ETCS这样的安全关键系统的验证过程中的益处如下：
在安全关键软件的研发中使用形式化的方法，是对行业传递的重要信息，有时甚至直接就是客户的需求。在OpenETCS项目中，这种基于SCADE模型检查的形式化解决方案，被证明对于保证开发的轨交计算机联锁(CBI)系统或基于通信列车控制(CBTC)系统的安全性尤其有效。
免责声明：本文系网络转载或改编，未找到原创作者，版权归原作者所有。如涉及版权，请联系删
155-2731-8020
