[转载]嵌入式系统 | Ansys SCADE在轨交列车控制系统中的应用

Y">;2Pt;  
原创 Ansys中国 沈轶烨 &p$SFH?s  
&xqr&(o  
U;:,$]+  
上期，我们对Ansys SCADE在航空电传飞控系统中的应用做了详细分享。本期，将进一步拓展Ansys SCADE在轨交列车控制系统中的应用，全文通过首先介绍OpenETCS项目的背景及发展，然后描述OpenETCS项目中工作包的划分和工作流的概况，进而解释SCADE为什么能在OpenETCS项目的工具选型中脱颖而出。最后介绍Systerel公司是如何使用S3(Systerel Smart Solver)引擎对SCADE进行形式化验证的。 2JYt.HN  
ngN_,x7yc  
过去150年来，欧洲铁路分别在各个国界内各自发展，形成了各种不同的信号和列车控制系统，这严重阻碍了跨境交通。欧盟决定改善铁路部门的互操作性，因此提出了欧洲列车控制系统(ETCS：European Train Control System)，它作为欧洲铁路交通管理系统(ERTM: European Rail Traffic Management System)的一部分，旨在取代几乎所有欧洲国家遗留的列车控制系统，统一欧洲铁路网，允许列车运营商使用配备单一信号系统的铁路车辆在整个欧洲运行。 2;`"B|-T  
a4}2^K  
b_ |  
HH|&$C|64  
]4>[y?k34  
ETCS由基础设施组件和车载单元 (OBU: On board Unit) 组成。其系统需求规范 (SRS: System Requirements Specification) 主要由6个主要欧洲铁路信号制造商合作制定。这些公司成立了一个名为UNISIG的协会，与欧盟委员会和铁路运营商机构密切合作，管理和协调这些活动。然而，在开发ETCS过程中面临了不少挑战，由于解释标准中的差异，ETCS与轨旁设备间的互操作性 (Interoperability)尚未实现。此外，从各国铁路系统转换到ETCS的成本也很高。尽管不同欧洲铁路技术标准的多样性可能会给完全统一的ETCS带来难以逾越的障碍，但建立高水平的互操作性是可行的。 otO6<%/m  
z,oqYU\:  
41TB  
+B@NSEy/+  
当考虑到ETCS概念的真正核心，即其统一的软件时，软件解决方案的作用是决定性的。创建统一软件的关键在于开放的解决方案，使得所有参与者都可以自由访问该解决方案。这是产生OpenETCS思想的前提。 K/u`Wz~A  
D4r5wc%  
2009年，德国铁路公司 (Deutsche Bahn) 启动了一个项目，目标是将ETCS车辆成本降低到至少与传统列车保护系统相当的水平。基于德国铁路公司十多年来在自由许可和开源软件下发布软件的经验，他们提出了一个相应的ETCS解决方案的想法，即OpenETCS。 ?WX&,ew~  
t=]&q.  
很快，英国铁路公司(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项目中来。 _ QM  
hoihdVjv  
)gCHwu  
#7U,kTj9  
gH0B[w ]  
确切的来说，OpenETCS是一个项目，而不是一个组织。该项目的目标是为欧洲列车控制系统提供“开放的证明”(Open Proof)，证明可以： '.@R_sj
  
[#td  
5b[:B~J  
*将开源许可原则应用于铁路安全(ETCS)和铁路自动化应用中的关键软件组件，特别是在车辆方面，实现合作伙伴之间的共享发展，避免运营商与供应商之间的锁定情况，形成版本开放自由软件服务生态系统 R6Cm:4m}I  
*提供了一个平台，会员可以在该平台上交流经验，并基于开源和开放创新，共同发起和实施列车控制、列车自动化和铁路应用通用数字化领域的项目 6Bp{FOj:Ss  
*在所有层面上采用“开放标准”，包括硬件和软件规范、接口定义、设计工具、验证和确认程序，以及重要的嵌入式控制软件。通过应用这些技术和相关的业务概念，力求将最终车载产品的成本大幅降低，甚至低于传统的高性能信号系统 E `)p,{T  
*形成一个涵盖建模、设计、验证和测试的集成框架，以利用ETCS的成本效益和可靠性实现 OR^Wd  
*该框架将在ETCS软件的整个开发过程中提供一个完整的工具链。 AAdRuO{l1  
- 工具链将支持ETCS系统需求的形式化规范和验证 v) q6  
- 符合ETCS的代码自动生成和验证 Sh]x`3 ).  
- 基于模型的测试用例生成和执行 !DCJ2h%E[_  
*采用形式化方法，以克服现有互操作性问题，将繁琐沉重的验证和确认活动从轨道现场转移到实验室，加速ERTM的迁移和ERTM部署计划，节省宝贵的资源。OpenETCS方法通过对系统需求的形式化规范和验证、自动和ETCS兼容的代码生成和验证、基于模型的测试用例生成和测试执行，使最先进的工具系统能够经济高效、可靠地实现ETCS ~&~%qu  
*OpenETCS生成的代码用于ETCS的车载单元(OBU) +2w54X%?M  
<P5;8  
zHB{I(q  
2011年底以来，OpenETCS项目开发已作为ITEA的项目获得了公共资助。 lq_W;L  
* ITEA是一个软件创新领域的跨国和行业驱动的研发与创新项目，使一个由大型工业、中小企业、初创企业、学术界和客户组织组成的全球性知识社区能够在资助的项目中进行合作，这些项目将创新理念转化为新的业务、工作、经济增长和社会效益。由于ITEA是一个EUREKA集群，该共同体基于EUREKA原则在欧洲成立，并向全世界的参与者开放。 43-%")bH  
** 尤里卡计划 (EUREKA) 是欧盟的一个研究组织，成立于1985年。尤里卡计划的宗旨着重于市场导向的产业技术研究发展，其他领域例如军事，则不会涉入，目前每年约新增一百多个子计划。 9hT^Y,c0  
7`tnoTUv  
2015年12月，耗资近1900万欧元，耗费达156人年的工作量的OpenETCS项目的开源内容开发结束。其开源内容可在ITEA或github上查阅。 H9w*U  
2`vCQV  
/)de`k"  
OpenETCS的第一个成功商业应用是德国的柏林-慕尼黑高速铁路的ICE列车上实施的ETCS。根据ITEA发布的报告，OpenETCS的成果包括但不限于： 7-ba-[t#A  
xIrpGLPSh  
德国铁路ICE城际特快列车401型，403型, 411型, 415型的OBU B<[;rk  
德国LEA/Railergy公司的OpenETCS mobile simulation box fT8Id\6js  
\sC
0om,  
2ezuP F  
tb0XXEE  
q'2PG@  
德国罗斯托克大学的“nanoETCS” simulation model train uPV,-rm[F_  
R\:C|/6f  
*法国All4Tech公司的开源安全验证工具ESF “Eclipse Safety Framework” #Y}Hh7.<  
*比利时的形式化欧洲铁路交通管理系统“ERTMS Formal Specs” 1qUdj[Bj  
*法国的欧洲轨道软件应用公司(ERSA:European Rail Software Applications)的OpenETCS仿真包TC-SIM (Train Control Simulator) Ytx+7OLe  
*向欧洲铁路局(ERA: European Railway Agency)规范组提供的大量信息输入，这些信息输入主要涉及通过授权欧洲铁路共同体(CER: Community of European Railway)和ERTM用户组(EUG:ERTMS Users Group)为ERTM提供的各种问题。 B:z-?u#B  
J6[x(T  
OpenETCS开发成果将延伸至后续的Horizon 2020项目，ASTRail的Shift2Rail项目等，将其形成的技术、标准与协作模式推向更深和更高的层次。绝大部分项目的成果都可以在相关网站上访问。 {zUc*9  
GKY:"q&h  
#fGb M!3p  
0 \LkJ*i  
#s
#z@F  
;^DUtr ;  
2019年2月，瑞士铁路公司 (SBB)宣布加入OpenETCS。SBB已经通过SmartRail 4.0和” RCA计划” 与其他铁路和基础设施管理人员合作，正致力于开发下一代列车控制和交通管理系统 (Reference CCS Architecture) 。SBB希望通过与OpenETCS成员的密切合作，有助于开发和验证其系统。 %T6#c7U_  
\MtiLaI"  
* SmartRail4.0是一个行业计划，它根据整个系统优先安排和集中资源。合作的目的是共同开发各铁路相关公司支持的解决方案，致力于铁路生产的广泛数字化和自动化。 ~~zw[#'  
+ZE&]
BO{  
U&3*c+B4  
OpenETCS项目分为4大块7个工作包(WP: Work Package)及工业用户测试案例，分别是： @mJN  
*项目管理和外联：工作包1(项目管理)和工作包6(宣传、实用、标准化) yK?~XV:  
*架构、用户案例和确认：工作包2(需求的开放证明)和工作包4(验证和确认) \Zf&&7v  
*技术开发的开放证明：工作包3(模型框架)、工作包5(演示)和工作包7(语言和工具选型) R/^JyL  
q 8=u.T  
R~w(]  
/"CKVQ  
EN 50129的系统生命周期和EN 50128的软件开发生命周期流程的两个最重要的要素是将生命周期划分为若干个定义明确的阶段，并专注于编写和记录开发过程的文档。这有助于促进安全、验证、确认和评估活动，并提升用户利用最佳的实践来开发关键系统的信心。为了实现这一目标，必须按照CENELEC标准提供的约束条件，为OpenETCS定义适当的生命周期，并为参与者分配适当的角色和职责。OpenETCS的工作流如图示 k #*|-?  
g-p OO/|  
4!k={Pd  
N`Bt|#R
  
图表7中描述了OpenETCS过程主要的阶段和活动。项目的输入要素为黄色，规范和设计活动为蓝色，验证和确认活动为红色，安全相关的活动为绿色。其中 \ @N>38M  
D?\K~U* >  
% C 3jxt  
DJQ]NY|  
如下方图表8所示的深蓝色阶段的活动需要大量建模，因此需要选择合适的平台和工具进行开发。平台选用Eclipse没有太大争议。而开发工具方面选择面较多，OpenETCS进行了多轮评审才有结果。 6eDIS|/  
DhZtiqL#_  
`8dE8:#Y  
HqXo;`Yy}  
qfSo
F|  
Xb^\{s?b  
@IiT8B  
下图是EN50128的标准软件开发流程 M+hc,;6  
zW0AB8l  
8nnkv,wa  
4(aesZ8h  
针对EN50128的标准软件开发流程，OpenETCS对下列开发工具进行了初步筛选，蓝色代表入选的系统设计工具，绿色代表入选的软件设计工具，黄色代表入选的代码设计工具或语言，白色代表落选的工具。各个工具对每列所标识出的功能进行评估，+号表示完全满足(即该工具可用)，o标识部分满足，-号表示不满足(即该工具不可用)。T表示文本型工具，M表示支持数学符号，G表示支持图形建模。 ^2kWD8c*  
Jl]]nOBQ/  
{my=Li<_H  
下图是针对EN50128的传统验证流程 Ab2g),;c  
o~-X7)]  
5GJ0EZ'X  
B?0{=u  
而OpenETCS更强调使用形式化的方法，EN50128改进的以形式化方法为主的验证流程如图表11-2 V
e8!  

@i{JqHU"  
"DlCvjc  
.v" lY2:N  
k9Sqp:l,  
针对EN50128的以形式化方法为主的验证流程，OpenETCS对下列工具进行了初步筛选，蓝色代表入选的支持形式化的系统设计工具，绿色代表入选的支持形式化的软件设计工具，黄色代表入选的支持形式化的代码设计工具或语言，白色代表落选的工具。其中对每列名称所对应的功能，+号表示完全满足(即该工具可用)，o标识部分满足。 gs8L/veP  
/a$+EQ$  
_).'SU)>  
Yip9K[  
经过几轮的筛选，共有13款(种)软件入围，进入下一轮工具选型评审 2 !;4mij,  
L|q<Bpz  
:):Y6)giBD  
'o7PIhD"  
+1)C&:  
剩余的软件进入最终评审，从下图可以看到SCADE是剩余的唯一的可以大幅度跨越子系统设计、软件设计和软件代码生成三个阶段的形式化工具，覆盖面广，适用性高。 34oLl#q*  
l#~FeD  
KV5lpN PC  
@Qs-A^.  
经过参与方Benchmarking，Assessment，Decision Meeting和Composition of Toolchains四轮活动，最终选择Papyrus和SCADE两款软件共同作为OpenETCS的开发工具。工具的评估内容可以通过链接查阅 T?\CAk>  
https://github.com/OpenETCS/model-evaluation/tree/master/model 4o*V12_r'4  
y2+a2  
工具选型结束后，OpenETCS定义的开发和验证工具链平台如图表16 *c AoE l  
-YuvEm#f  
li%-9Jd  
<{) 4gvH  
]JD$f
S=_  
其中，需求及需求管理工具是黄色的，Eclipse平台是深蓝色的，验证工具是桔色的。使用SCADE的RM-Gatway工具进行需求管理。使用Papyrus进行系统设计，由于SCADE System具有Eclipse接口和Papyrus接口，通过SCADE自带的如下功能，可以增强Papyrus设计的系统功能 EkL\~^  
基于SysML的文档生成 CD&m4^X5D  
基于SysML的模型规则检查 "qj[[LQ  
基于SysML的模型比对 *2AQ'%U~  
与Reqtify等工具进行桥接，实现追踪管理等功能 .d"+M{I  
与SCADE Suite进行桥接，一键同步系统层的架构、接口、数据流、数据类型等到软件层。 pt4xUu{  
%UQ{'JW?K  
在软件设计阶段，使用SCADE进行形式化建模和后续验证，其中可以用到如下模块： okcl-q  
SCADE Suite Editor 支持图形或文本建模 \9}5}X_x.  
SCADE Requirements Gateway Integration 支持模型级追踪管理 + kF[Oh#  
SCADE Model Check 支持语法语义检查 NdNfai  
SCADE Model Diff 支持模型比对 KvD$`"L/CT  
SCADE Simulator 支持模型级仿真、调试；支持自动化定制 llleo8  
SCADE Rapid Prototype 支持快速设计仿真界面进行交互式测试 q9 ;\B&  
SCADE Code Generator KCG 支持认证级C或Ada代码生成 *.*:(7`  
SCADE Reporter 支持文档生成 wi9|  
SCADE Model Test Coverage MTC: 支持模型级和代码级的覆盖分析；支持自动化定制 lXPn]iLJ  
SCADE Design Verifier: 桥接Prover公司工具，支持形式化分析 'u3+k.  
SCADE Timing Verifier: 桥接AbsInt公司工具，支持最坏运行时间和堆栈分析 ltrSTH,kL  
RT-Tester:  桥接目标机测试工具，支持将模型级测试用例转换为选用工具的测试用例 $1?X%8V  
t3GK{X  
!X8UP{J)L  
OpenETCS项目是开源的，各合作方可以选用特定的验证工具对设计完毕的SCADE模型等文件进行分析和验证。在OpenETCS项目的验证和确认总结报告中，综述了6个阶段的结果，分别是 +E [bLz^  
1、计划阶段 (Planning Phase) 的验证和确认 DrEtnt  
2、系统设计阶段(System Design Phase)的验证和确认 7P`1)juA9  
3、软件设计阶段(SW Design Phase)的验证和确认 epbp9[`  
4、软件组件阶段(SW Component Phase)的验证和确认 +zD'r5  
5、软件集成阶段(SW Integration Phase)的验证和确认 &!a2%%1#N  
6、软件验证阶段 (SW Validation Phase) 的评审和确认 s =5H.q%PV  
6g"<i}_|  
阶段3~阶段6和SCADE工具有关联，负责这方面工作的包括德国罗斯托克大学(University of Rostock)，德国航天中心(DLR)，法国Systerel公司，德国Fraunhofer FOCUS公司和意大利通用电气交通(GE Transportation)。本节主要介绍下法国Systerel公司是如何使用形式化工具S3(Systerel Smart Solver)对软件组件的两个功能进行模型检查的（有关模型检查的介绍，详见往期：嵌入式系统 | 基于SCADE模型的形式化方法），其工作流如图表17 ]T51;j'48  
Q'a N|^w"f  
gr?pvf!I  
第一个输入是SCADE模型，将会被转换为HLL模型，第二个输入是由HLL语言描述的安全属性和环境假设或约束。两个输入合并为一个HLL文件后传给S3引擎，通过BMC策略在指定的深度分析后，得出结果。如果结果失败，输出反例；如果结果正确，安全属性得证。 J:lwq@u  
u W|x)g11a  
首先可使用S3引擎内置的属性检查(proof obligations)快速查找的SCADE模型中的错误，以评估HLL模型的定义是否正确：内置的属性检查包括 Q$vr`yV#=6  
数组的索引越界检查 !p&'so^-W  
定义范围的检查 if}]8
  
除0检查 pHvE`s"Ea  
算术表达式的溢出检查 Q*C4
q`  
输出和约束的初始化检查 8QN8bGxK   
O<h#|g1  
此外，从一种语言到HLL的转换本身，也可以生成要由S3分析的安全属性，以检查代码对于源语言有无未定义的行为。例如，C转换器添加了一些安全属性，以确保与C99标准的一致性。 o3yqG#dA  
-{*V)J_Co  
Uu X"AFy~\  
^d9
raYE`'  
Systerel共对5个案例进行了形式化分析，本文抽取其中两个来介绍。 i/J NG  
'&QT}B  
9Bk}g50$#  
6.1、Systerel进行形式化分析案例1：isolate操作符 8e@JvAaa$  
\!QF9dP4  
YgiGI <U  
:b;1P@W<  
转换为HLL后的对S3引擎的输入如图表20，内容可通过直接阅读绿色的文本注释获取。 Tqa4~|6  
x!~OK::o8  
Mdrv/x{  
J3x7i8  
经S3引擎分析，Isolate mode的属性得证 H ZLOn  
v,+l xY  
6.2、Systerel进行形式化分析案例2：验证非形式化规约（例如流程图） X{xJ*T y'  
1Kh?JH  
|I}+!DDuv  
例如，当刚开始执行任务时，列车处于静止状态，车载系统处于待机模式(SB：Stand-by mode)，列车数据(识别号、长度等)得到验证。一旦司机下启动指令按钮，车载系统就向司机发送确认信息请求，然后等待接收到此确认消息，以切换到适当的模式。在图表21中，当选择0级时，车载系统应切换到不适合模式（UN: Unfitted mode）。预期的过程如图表22所示。 B%@!\D#  
'r n;|K  
zzQH@D1  
iFCH$!  
9`v:$(I  
对于这种复杂情况，要验证的SCADE模型不能被视为黑盒(black box)，应分析内部状态，明确定义SCADE和HLL模型之间的等价性，步骤如下: ptv4v[gQ  
将“SCADE模型图”中的模型转换为HLL模型 $M`;."
 
对HLL模型进行场景说明 <e&QTyb  
对HLL中的状态与SCADE模型的状态的等价性进行说明（例如，“SCADE模型图”中的状态“level_0”应与“简化的操作流程图”中的状态“S2”相对应） 0:Y`#0qK  
用S3工具证明其等价性并分析反例(如果有的话) 1:!rw,Jzl`  
H27Oq8  
#=H}6!18  
c2\vG  
_A|\.(t  
值得一提的是，反 .. otSPi7|k  
tMZ(s  

未注册仅能浏览部分内容，查看全部内容及附件请先 登录 或 注册