上期，我們對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)的一部分，旨在取代幾乎所有歐洲國家遺留的列車控制系統，統一歐洲鐵路網，允許列車運營商使用配備單一信號系統的鐵路車輛在整個歐洲運行。

圖表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車輛成本降低到至少與傳統列車保護系統相當的水平?；诘聡F路公司十多年來在自由許可和開源軟件下發布軟件的經驗，他們提出了一個相應的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項目中來。

圖表3: 截止到2015年OpenETCS項目的31個合作方

確切的來說，OpenETCS是一個項目，而不是一個組織。該項目的目標是為歐洲列車控制系統提供“開放的證明”(Open Proof)，證明可以：

• 將開源許可原則應用于鐵路安全(ETCS)和鐵路自動化應用中的關鍵軟件組件，特別是在車輛方面，實現合作伙伴之間的共享發展，避免運營商與供應商之間的鎖定情況，形成版本開放自由軟件服務生態系統

• 提供了一個平臺，會員可以在該平臺上交流經驗，并基于開源和開放創新，共同發起和實施列車控制、列車自動化和鐵路應用通用數字化領域的項目

• 在所有層面上采用“開放標準”，包括硬件和軟件規范、接口定義、設計工具、驗證和確認程序，以及重要的嵌入式控制軟件。通過應用這些技術和相關的業務概念，力求將最終車載產品的成本大幅降低，甚至低于傳統的高性能信號系統

• 形成一個涵蓋建模、設計、驗證和測試的集成框架，以利用ETCS的成本效益和可靠性實現

• 該框架將在ETCS軟件的整個開發過程中提供一個完整的工具鏈。

• 采用形式化方法，以克服現有互操作性問題，將繁瑣沉重的驗證和確認活動從軌道現場轉移到實驗室，加速ERTM的遷移和ERTM部署計劃，節省寶貴的資源。OpenETCS方法通過對系統需求的形式化規范和驗證、自動和ETCS兼容的代碼生成和驗證、基于模型的測試用例生成和測試執行，使最先進的工具系統能夠經濟高效、可靠地實現ETCS

• OpenETCS生成的代碼用于ETCS的車載單元(OBU)

2011年底以來，OpenETCS項目開發已作為ITEA的項目獲得了公共資助。

2015年12月，耗資近1900萬歐元，耗費達156人年的工作量的OpenETCS項目的開源內容開發結束。其開源內容可在ITEA或github上查閱。

OpenETCS的第一個成功商業應用是德國的柏林-慕尼黑高速鐵路的ICE列車上實施的ETCS。根據ITEA發布的報告，OpenETCS的成果包括但不限于：

• 德國鐵路ICE城際特快列車401型，403型, 411型, 415型的OBU

• 德國LEA/Railergy公司的OpenETCS mobile simulation box

圖表4: 德國LEA/Railergy公司的OpenETCS項目成果

• 德國羅斯托克大學的“nanoETCS” simulation model train

• 法國All4Tech公司的開源安全驗證工具ESF “Eclipse Safety Framework”

• 比利時的形式化歐洲鐵路交通管理系統“ERTMS Formal Specs”

• 法國的歐洲軌道軟件應用公司(ERSA:European Rail Software Applications)的OpenETCS仿真包TC-SIM (Train Control Simulator)

• 向歐洲鐵路局(ERA: European Railway Agency)規范組提供的大量信息輸入，這些信息輸入主要涉及通過授權歐洲鐵路共同體(CER: Community of European Railway)和ERTM用戶組(EUG:ERTMS Users Group)為ERTM提供的各種問題。

OpenETCS開發成果將延伸至后續的Horizon 2020項目，ASTRail的Shift2Rail項目等，將其形成的技術、標準與協作模式推向更深和更高的層次。絕大部分項目的成果都可以在相關網站上訪問。

圖表5: OpenETCS項目成果的后續演進

2019年2月，瑞士鐵路公司 (SBB)宣布加入OpenETCS。SBB已經通過SmartRail 4.0和” RCA計劃” 與其他鐵路和基礎設施管理人員合作，正致力于開發下一代列車控制和交通管理系統 (Reference CCS Architecture) 。SBB希望通過與OpenETCS成員的密切合作，有助于開發和驗證其系統。

OpenETCS項目分為4大塊7個工作包(WP: Work Package)及工業用戶測試案例，分別是：

• 項目管理和外聯：工作包1(項目管理)和工作包6(宣傳、實用、標準化)

• 架構、用戶案例和確認：工作包2(需求的開放證明)和工作包4(驗證和確認)

• 技術開發的開放證明：工作包3(模型框架)、工作包5(演示)和工作包7(語言和工具選型)

圖表6: OpenETCS項目的工作包

EN 50129的系統生命周期和EN 50128的軟件開發生命周期流程的兩個最重要的要素是將生命周期劃分為若干個定義明確的階段，并專注于編寫和記錄開發過程的文檔。這有助于促進安全、驗證、確認和評估活動，并提升用戶利用最佳的實踐來開發關鍵系統的信心。為了實現這一目標，必須按照CENELEC標準提供的約束條件，為OpenETCS定義適當的生命周期，并為參與者分配適當的角色和職責。OpenETCS的工作流如圖示

圖表7: OpenETCS項目的工作流

圖表7中描述了OpenETCS過程主要的階段和活動。項目的輸入要素為黃色，規范和設計活動為藍色，驗證和確認活動為紅色，安全相關的活動為綠色。其中

如下方圖表8所示的深藍色階段的活動需要大量建模，因此需要選擇合適的平臺和工具進行開發。平臺選用Eclipse沒有太大爭議。而開發工具方面選擇面較多，OpenETCS進行了多輪評審才有結果。

圖表8: OpenETCS項目工作流中需要大量建模的4個部分

下圖是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設計的系統功能

• 基于SysML的文檔生成

• 基于SysML的模型規則檢查

• 基于SysML的模型比對

• 與Reqtify等工具進行橋接，實現追蹤管理等功能

• 與SCADE Suite進行橋接，一鍵同步系統層的架構、接口、數據流、數據類型等到軟件層。

在軟件設計階段，使用SCADE進行形式化建模和后續驗證，其中可以用到如下模塊：

• SCADE Suite Editor 支持圖形或文本建模

• SCADE Requirements Gateway Integration 支持模型級追蹤管理

• SCADE Model Check 支持語法語義檢查

• SCADE Model Diff 支持模型比對

• SCADE Simulator 支持模型級仿真、調試；支持自動化定制

• SCADE Rapid Prototype 支持快速設計仿真界面進行交互式測試

• SCADE Code Generator KCG 支持認證級C或Ada代碼生成

• SCADE Reporter 支持文檔生成

• SCADE Model Test Coverage MTC: 支持模型級和代碼級的覆蓋分析；支持自動化定制

• SCADE Design Verifier: 橋接Prover公司工具，支持形式化分析

• SCADE Timing Verifier: 橋接AbsInt公司工具，支持最壞運行時間和堆棧分析

• RT-Tester:  橋接目標機測試工具，支持將模型級測試用例轉換為選用工具的測試用例

OpenETCS項目是開源的，各合作方可以選用特定的驗證工具對設計完畢的SCADE模型等文件進行分析和驗證。在OpenETCS項目的驗證和確認總結報告中，綜述了6個階段的結果，分別是

1. 計劃階段 (Planning Phase) 的驗證和確認

2. 系統設計階段(System Design Phase)的驗證和確認

3. 軟件設計階段(SW Design Phase)的驗證和確認

4. 軟件組件階段(SW Component Phase)的驗證和確認

5. 軟件集成階段(SW Integration Phase)的驗證和確認

6. 軟件驗證階段 (SW Validation Phase) 的評審和確認

階段3~階段6和SCADE工具有關聯，負責這方面工作的包括德國羅斯托克大學(University of Rostock)，德國航天中心(DLR)，法國Systerel公司，德國Fraunhofer FOCUS公司和意大利通用電氣交通(GE Transportation)。本節主要介紹下法國Systerel公司是如何使用形式化工具S3(Systerel Smart Solver)對軟件組件的兩個功能進行模型檢查的（有關模型檢查的介紹，詳見往期：嵌入式系統 | 基于SCADE模型的形式化方法），其工作流如圖表17

圖表17: OpenETCS項目中Systerel公司S3引形式化分析引擎工作流

第一個輸入是SCADE模型，將會被轉換為HLL模型，第二個輸入是由HLL語言描述的安全屬性和環境假設或約束。兩個輸入合并為一個HLL文件后傳給S3引擎，通過BMC策略在指定的深度分析后，得出結果。如果結果失敗，輸出反例；如果結果正確，安全屬性得證。

首先可使用S3引擎內置的屬性檢查(proof obligations)快速查找的SCADE模型中的錯誤，以評估HLL模型的定義是否正確：內置的屬性檢查包括

• 數組的索引越界檢查

• 定義范圍的檢查

• 除0檢查

• 算術表達式的溢出檢查

• 輸出和約束的初始化檢查

此外，從一種語言到HLL的轉換本身，也可以生成要由S3分析的安全屬性，以檢查代碼對于源語言有無未定義的行為。例如，C轉換器添加了一些安全屬性，以確保與C99標準的一致性。

圖表18: OpenETCS項目中Systerel公司產品應用的5個案例

Systerel共對5個案例進行了形式化分析，本文抽取其中兩個來介紹。

圖表19: isolate操作符的SCADE模型功能

轉換為HLL后的對S3引擎的輸入如圖表20，內容可通過直接閱讀綠色的文本注釋獲取。

圖表20: isolate操作符轉換為HLL后的對S3引擎的輸入

經S3引擎分析，Isolate mode的屬性得證

圖表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模型之間的等價性，步驟如下:

1. 將“SCADE模型圖”中的模型轉換為HLL模型

2. 對HLL模型進行場景說明

3. 對HLL中的狀態與SCADE模型的狀態的等價性進行說明（例如，“SCADE模型圖”中的狀態“level_0”應與“簡化的操作流程圖”中的狀態“S2”相對應）

4. 用S3工具證明其等價性并分析反例(如果有的話)

圖表23: SCADE模型局部Start of Mission

值得一提的是，反例中包含特定的輸入值，這些值會引起正確等價性的錯誤證明。這可能是由于引擎推導出的實際中并不存在的輸入值。在這種情況下，可以在HLL模型中添加約束。在該例中，可以假設在模式管理期間，level輸入值與值“L0”保持不變，即列車數據保持不變且有效。

在驗證過程中，添加約束將引起驗證系統其余部分的新屬性。其他假設可以集成到屬性中進行驗證，當H是假設時，證明目標P被替換為證明目標H，即H=>P。只要引入其他屬性來覆蓋H為假的情況，就不再需要其他外部驗證來測試H。通常，這些假設的定義是為了消除可能的行為，而不是與原驗證主題直接相關的行為。

在本例中，我們假設在模型的輸入中不會檢測到系統故障，因此在檢查切換到不適合模式(UN: Unfitted mode)時，不考慮引起系統故障模式的所有行為。系統故障的發生已被其他形式化分析的安全屬性覆蓋。在此給定的輸入約束和假設條件下，證明了兩種狀態機的行為是等價的。內容可通過直接閱讀綠色的文本注釋獲取。

圖表24: Start of Mission模型轉換為HLL后的對S3引擎的輸入

形式化方法在諸如ETCS這樣的安全關鍵系統的驗證過程中的益處如下：

• 與傳統人工驗證方式相比，形式化方法在數學上是完備的，實踐上相當于遍歷了所有的可能情況

• 形式化方法清楚地識別出了安全需求所依賴的完整假設列表

• 該解決方案可減少測試和審查工作（只需審查通用安全規范）

在安全關鍵軟件的研發中使用形式化的方法，是對行業傳遞的重要信息，有時甚至直接就是客戶的需求。在OpenETCS項目中，這種基于SCADE模型檢查的形式化解決方案，被證明對于保證開發的軌交計算機聯鎖(CBI)系統或基于通信列車控制(CBTC)系統的安全性尤其有效。

[1] About OpenETCS[EB/OL]. http://OpenETCS.org/about/

[2] OpenETCS[EB/OL]. https://de.wikipedia.org/wiki/OpenETCS

[3] OpenETCS Open Proofs Methodology for the European Train Control Onboard System [EB/OL]. https://itea3.org/project/OpenETCS.html

[4] OpenETCS project results leaflet[EB/OL]. https://itea3.org/project/result/download/6441/OpenETCS Project results leaflet.pdf.

[5] Baseliyos Jacob, DB Netz AG. Horizon 2020 call: openETCS@ITEA2 proposal MG.2.3 – 2014: New generation of rail vehicles [EB/OL].https://github.com/openETCS/horizon2020/blob/master/openETCS_Follow_UpHorizon2020_MG_2.3_proposal.pdf Jan 16, 2014

[6] 李平，邵賽，薛蕊，等.國外鐵路數字化與智能化發展趨勢研究[J]. 中國鐵路，2019(2)：25-31.

[7] 耿樞馨，姜惠峰.歐洲的數字化鐵路發展[J]．綜合運輸，2017(10) : 31-34.

[8] 林鴻，王林美，魏艷萍. 關于歐盟Shift2Rail計劃的研究[J]. 國外鐵道車輛. 2019(1)：11-16

[9] SBB joins openETCS Foundation [EB/OL].https://www.railwaygazette.com/europe/sbb-joins-openetcs-foundation/48098.article. Feb 25,2019

[10] Jan Welte, Hansj?rg Manz. OpenETCS D2.1: Report on existing methodologies[R]. Technische Universit?t Braunschweig Institute for Traffic Safety and Automation Engineering. Nov 22,2012

[11] Michael Jastram, Marielle Petit-Doche, et al. Report on the Final Choice of the Primary Toolchain [EB/OL].https://itea3.org/project/workpackage/document/download/1469/D7.1 openETCS-Report on the final choice(s) for the primary tool chain. Nov,2014

[12] Hardi Hungar, Marc Behrens, Mirko Caspar, Michael M?nsters,Jan Peleska, et al.openETCS Final Report on Verification and Validation [EB/OL]. https://itea3.org/project/workpackage/document/download/2609/D4.4. openETCS - Final Report on Verification and Validation.pdfDec.2015

[13] Marielle Petit-Doche, Matthias G, Rom_eo C. Verication of Scade models with S3 model-checker [EB/OL]. https://github.com/openETCS/validation/blob/master/VnVUserStories/VnVUserStorySysterel/04-Results/e-Scade_S3/Scade_S3_VnV.pdf. Nov 16,2015

[14] Petit-Doche M, Breton N, Courbis R, et al. Formal verification of industrial critical software[C]//International Workshop on Formal Methods for Industrial Critical Systems. Springer, Cham, 2015: 1-11.