嵌入式体系 Ansys SCADE在轨交列车操控体系中的运用
发布时间:2022-08-03 15:51:41 | 作者:亚博网址登录

  上期,咱们对Ansys SCADE在航空电传飞控体系中的运用做了具体同享。本期,将进一步拓宽Ansys SCADE在轨交列车操控体系中的运用,全文经过首要介绍OpenETCS项意图布景及开展,然后描绘OpenETCS项目中作业包的区分和作业流的概略,从而解说SCADE为什么能在OpenETCS项意图东西选型中锋芒毕露。终究介绍Systerel公司是怎么运用S3(Systerel Smart Solver)引擎对SCADE进行形式化验证的。

  曩昔150年来,欧洲铁路分别在各个国界内各自开展,构成了各种不同的信号和列车操控体系,这严峻阻止了跨境交通。欧盟决议改进铁路部门的互操作性,因而提出了欧洲列车操控体系(ETCS:European Train Control System),它作为欧洲铁路交通办理体系(ERTM: European Rail Traffic Management System)的一部分,旨在替代简直一切欧洲国家留传的列车操控体系,一致欧洲铁路网,答应列车运营商运用装备单一信号体系的铁路车辆在整个欧洲运转。

  ETCS由基础设施组件和车载单元 (OBU: On board Unit) 组成。其体系需求规范 (SRS: System Requirements Specification) 首要由6个首要欧洲铁路信号制造商协作拟定。这些公司建立了一个名为UNISIG的协会,与欧盟委员会和铁路运营商组织密切协作,办理和协调这些活动。但是,在开发ETCS进程中面临了不少应战,因为解说规范中的差异,ETCS与轨旁设备间的互操作性 (Interoperability)没有完成。此外,从各国铁路体系转化到ETCS的本钱也很高。虽然不同欧洲铁路技能规范的多样性或许会给彻底一致的ETCS带来难以逾越的妨碍,但树立高水平的互操作性是可行的。

  当考虑到ETCS概念的真实中心,即其一致的软件时,软件解决方案的作用是决议性的。创立一致软件的要害在于敞开的解决方案,使得一切参与者都能够自在拜访该解决方案。这是产生OpenETCS思维的条件。

  2009年,德国铁路公司 (Deutsche Bahn) 发动了一个项目,方针是将ETCS车辆本钱下降到至少与传统列车维护体系恰当的水平。依据德国铁路公司十多年来在自在答应和开源软件下发布软件的经历,他们提出了一个相应的ETCS解决方案的主意,即OpenETCS。

  切当的来说,OpenETCS是一个项目,而不是一个组织。该项意图方针是为欧洲列车操控体系供给“敞开的证明”(Open Proof),证明能够:

  将开源答应准则运用于铁路安全(ETCS)和铁路主动化运用中的要害软件组件,特别是在车辆方面,完成协作伙伴之间的同享开展,防止运营商与供货商之间的确定状况,构成版别敞开自在软件服务生态体系

  供给了一个渠道,会员能够在该渠道上交流经历,并依据开源和敞开立异,一起建议和施行列车操控、列车主动化和铁路运用通用数字化范畴的项目

  在一切层面上选用“敞开规范”,包括硬件和软件规范、接口界说、规划东西、验证和承认程序,以及重要的嵌入式操控软件。经过运用这些技能和相关的事务概念,力求将终究车载产品的本钱大幅下降,乃至低于传统的高性能信号体系

  选用形式化办法,以战胜现有互操作性问题,将繁琐沉重的验证和承认活动从轨迹现场转移到实验室,加快ERTM的搬迁和ERTM布置方案,节约名贵的资源。OpenETCS办法经过对体系需求的形式化规范和验证、主动和ETCS兼容的代码生成和验证、依据模型的测验用例生成和测验履行,使最先进的东西体系能够经济高效、可靠地完成ETCS

  * ITEA是一个软件立异范畴的跨国和职业驱动的研制与立异项目,使一个由大型工业、中小企业、草创企业、学术界和客户组织组成的全球性知识社区能够在赞助的项目中进行协作,这些项目将立异理念转化为新的事务、作业、经济增加和社会效益。因为ITEA是一个EUREKA集群,该一起体依据EUREKA准则在欧洲建立,并向全世界的参与者敞开。

  ** 尤里卡方案 (EUREKA) 是欧盟的一个研讨组织,建立于1985年。尤里卡方案的主旨着重于市场导向的工业技能研讨开展,其他范畴例如军事,则不会涉入,现在每年约新增一百多个子方案。

  2015年12月,耗资近1900万欧元,消耗达156人年的作业量的OpenETCS项意图开源内容开发结束。其开源内容可在ITEA或github上查阅。

  OpenETCS的第一个成功商业运用是德国的柏林-慕尼黑高速铁路的ICE列车上施行的ETCS。依据ITEA发布的陈述,OpenETCS的效果包括但不限于:

  OpenETCS开发效果将延伸至后续的Horizon 2020项目,ASTRail的Shift2Rail项目等,将其构成的技能、规范与协作形式面向更深和更高的层次。绝大部分项意图效果都能够在相关网站上拜访。

  2019年2月,瑞士铁路公司 (SBB)宣告参加OpenETCS。SBB现已经过SmartRail 4.0和” RCA方案” 与其他铁路和基础设施办理人员协作,正致力于开发下一代列车操控和交通办理体系 (Reference CCS Architecture) 。SBB期望经过与OpenETCS成员的密切协作,有助于开发和验证其体系。

  * SmartRail4.0是一个职业方案,它依据整个体系优先组织和会集资源。协作的意图是一起开发各铁路相关公司支撑的解决方案,致力于铁路出产的广泛数字化和主动化。

  EN 50129的体系生命周期和EN 50128的软件开产生命周期流程的两个最重要的要素是将生命周期区分为若干个界说清晰的阶段,并专心于编写和记载开发进程的文档。这有助于促进安全、验证、承认和评价活动,并提高用户运用最佳的实践来开发要害体系的决心。为了完成这一方针,有必要依照CENELEC规范供给的束缚条件,为OpenETCS界说恰当的生命周期,并为参与者分配恰当的人物和责任。OpenETCS的作业流如图示

  图表7中描绘了OpenETCS进程首要的阶段和活动。项意图输入要素为黄色,规范和规划活动为蓝色,验证和承认活动为赤色,安全相关的活动为绿色。其间

  活动b:经过进程2活动b的形式化体系模型完成形式化的软件模型和架构,并将此办法运用于SSRS的一个子集,这也将是OpenETCS的终究输出

  如下方图表8所示的深蓝色阶段的活动需求很多建模,因而需求挑选适宜的渠道和东西进行开发。渠道选用Eclipse没有太大争议。而开发东西方面挑选面较多,OpenETCS进行了多轮评定才有成果。

  针对EN50128的规范软件开发流程,OpenETCS对下列开发东西进行了开始挑选,蓝色代表当选的体系规划东西,绿色代表当选的软件规划东西,黄色代表当选的代码规划东西或言语,白色代表落选的东西。各个东西对每列所标识出的功用进行评价,+号表明彻底满意(即该东西可用),o标识部分满意,-号表明不满意(即该东西不可用)。T表明文本型东西,M表明支撑数学符号,G表明支撑图形建模。

  其间,需求及需求办理东西是黄色的,Eclipse渠道是深蓝色的,验证东西是桔色的。运用SCADE的RM-Gatway东西进行需求办理。运用Papyrus进行体系规划,因为SCADE System具有Eclipse接口和Papyrus接口,经过SCADE自带的如下功用,能够增强Papyrus规划的体系功用

  OpenETCS项目是开源的,各协作方能够选用特定的验证东西对规划结束的SCADE模型等文件进行剖析和验证。在OpenETCS项意图验证和承认总结陈述中,总述了6个阶段的成果,分别是

  阶段3~阶段6和SCADE东西有相关,担任这方面作业的包括德国罗斯托克大学(University of Rostock),德国航天中心(DLR),法国Systerel公司,德国Fraunhofer FOCUS公司和意大利通用电气交通(GE Transportation)。本节首要介绍下法国Systerel公司是怎么运用形式化东西S3(Systerel Smart Solver)对软件组件的两个功用进行模型查看的(有关模型查看的介绍,详见往期:嵌入式体系 依据SCADE模型的形式化办法),其作业流如图表17

  第一个输入是SCADE模型,将会被转化为HLL模型,第二个输入是由HLL言语描绘的安全特点和环境假定或束缚。两个输入合并为一个HLL文件后传给S3引擎,经过BMC战略在指定的深度剖析后,得出成果。假如成果失利,输出反例;假如成果正确,安全特点得证。

  首要可运用S3引擎内置的特点查看(proof obligations)快速查找的SCADE模型中的过错,以评价HLL模型的界说是否正确:内置的特点查看包括

  此外,从一种言语到HLL的转化自身,也能够生成要由S3剖析的安全特点,以查看代码关于源言语有无未界说的行为。例如,C转化器增加了一些安全特点,以确保与C99规范的一致性。

  例如,当刚开始履行任务时,列车处于停止状况,车载体系处于待机形式(SB:Stand-by mode),列车数据(识别号、长度等)得到验证。一旦司机下发动指令按钮,车载体系就向司机发送承认信息恳求,然后等候接纳到此承认音讯,以切换到恰当的形式。在图表21中,当挑选0级时,车载体系应切换到不适合形式(UN: Unfitted mode)。预期的进程如图表22所示。

  关于这种复杂状况,要验证的SCADE模型不能被视为黑盒(black box),应剖析内部状况,清晰界说SCADE和HLL模型之间的等价性,进程如下:

  对HLL中的状况与SCADE模型的状况的等价性进行阐明(例如,“SCADE模型图”中的状况“level_0”应与“简化的操作流程图”中的状况“S2”相对应)

  值得一提的是,反例中包括特定的输入值,这些值会引起正确等价性的过错证明。这或许是因为引擎推导出的实践中并不存在的输入值。在这种状况下,能够在HLL模型中增加束缚。在该例中,能够假定在形式办理期间,level输入值与值“L0”坚持不变,即列车数据坚持不变且有用。

  在验证进程中,增加束缚将引起验证体系其余部分的新特点。其他假定能够集成到特点中进行验证,当H是假定时,证明方针P被替换为证明方针H,即H=P。只需引进其他特点来掩盖H为假的状况,就不再需求其他外部验证来测验H。一般,这些假定的界说是为了消除或许的行为,而不是与原验证主题直接相关的行为。

  在本例中,咱们假定在模型的输入中不会检测到体系故障,因而在查看切换到不适合形式(UN: Unfitted mode)时,不考虑引起体系故障形式的一切行为。体系故障的产生已被其他形式化剖析的安全特点掩盖。在此给定的输入束缚和假定条件下,证明了两种状况机的行为是等价的。内容可经过直接阅览绿色的文本注释获取。

  在安全要害软件的研制中运用形式化的办法,是对职业传递的重要信息,有时乃至直接便是客户的需求。在OpenETCS项目中,这种依据SCADE模型查看的形式化解决方案,被证明关于确保开发的轨交计算机联锁(CBI)体系或依据通讯列车操控(CBTC)体系的安全性特别有用。

  [6] 李平,邵赛,薛蕊,等.国外铁路数字化与智能化开展趋势研讨[J]. 我国铁路,2019(2):25-31.

上一篇:国内CRM体系哪家公司做的最好 CRM办理体系引荐 下一篇:需求办理软件哪个好
  • 电话:0351-7028907
  • 服务电话:4006026858
  • 地址:山西省太原市小店区高新街9号瑞杰科技B座8层