面向形式化驗證的聯鎖翻譯器軟件設計

王紹新，王燕芩，閆連山

（1.卡斯柯信號（成都）有限公司，成都 610083；2．卡斯柯信號有限公司，上海 200071；3．西南交通大學信息科學與技術學院，成都 611756）

形式化證明是用數學方法去證明電子或者計算機系統是完備的、無漏洞的，在電子硬件設計和航天基建領域比較常用。鐵路信號的根本功能是保障列車運行安全、提高運輸效率，聯鎖系統是鐵路信號的核心技術裝備，它通過對信號機、道岔和進路的控制來指揮行車、防止列車沖突。在地鐵調度領域，由巴黎地鐵信號系統開始，在北美、歐洲、亞洲及南美洲的部分國家的地鐵系統開發中，形式化證明方法已經被廣泛使用。隨著計算機聯鎖系統的應用推廣，聯鎖系統對軟件的依賴性越來越強，如何提高聯鎖軟件的質量、確保系統安全是近年來軌道交通領域研究的熱點問題。

1 聯鎖系統形式化驗證

1.1 形式化在軌道交通領域的應用現狀

形式化方法起源于20世紀60年代，在學術界已有很多成果，同時也發展出多個分支。由于其研發有一定的技術難度，前期的投入也比較大，因此在工業界的應用時間并不長。但是國外已經有一些完全使用形式化方法開發出的鐵路信號系統，如巴黎地鐵14號線的自動駕駛系統就是采用形式化方法開發的，至今未發現缺陷。

隨著形式化方法的發展，各國鐵路業主和信號廠商都已經開始關注并積極研究形式化方法應用于信號系統的開發或驗證。國外業主方已經逐步將使用形式化方法開發或驗證鐵路信號系統作為一個強制的要求，如巴黎地鐵(RATP)和紐約公共運輸局（NYTC）、加太鐵路（Canadian Pacific）、斯德哥爾摩地鐵（Stockholm Metro）、比利時國家鐵路（Infrabel）、瑞典鐵路（Trafikverket）、英國的鐵路網公司（Network Rail）等，在多個不同的項目中應用了形式化方法。

形式化方法進行安全軟件的開發和驗證是目前的一個趨勢，同時也是EN50128中高度推薦的方法。由于聯鎖邏輯本身的特點，十分適合進行形式化開發和驗證。使用形式化方法進行聯鎖系統開發和驗證，可以證明系統的內在邏輯上滿足既定的安全需求,在未來的市場競爭中具有很強的優勢。目前國內也有幾家信號廠商在不同的安全系統中使用形式化開發方法，并取得了一定的效果。

1.2 聯鎖系統的形式化驗證流程

卡斯柯信號有限公司通過引進國外Prover公司的形式化驗證方法和工具iLock，以聯鎖系統通用車站為測試站場，構造站場中各類信號機、道岔、區段的狀態屬性，依據各信號設備之間的聯鎖關系，自動生成站場中的所有進路。根據聯鎖系統需求，設計聯鎖通用車站的需求驗證模型，對站場內所有進路在建立過程中涉及的聯鎖邏輯安全進行驗證。

本項目是基于形式化方法對聯鎖系統進行證明，采用形式化高級開發語言，對聯鎖系統的安全需求開展通用安全需求（General Safety Specification，GSS），建立車站信號設備的對象模型（OM），開發接口文件、站場文件（.TLE文件）和布爾邏輯文件(.VTL文件)的轉換器，生成形式化驗證所需要的LCF/SEIF文件，使用形式化驗證工具，驗證聯鎖數據是否滿足系統安全屬性要求。

驗證流程如圖 1所示。

圖1 形式化驗證流程Fig.1 Flow chart of formal verification

翻譯器軟件Translator由卡斯柯信號有限公司進行雙鏈開發，其中1鏈采用的語言是具有安全特性的函數式編程語言OCaml。

2 翻譯器軟件設計

聯鎖數據的形式化驗證過程中的輸入文件包含VTL文件、TLE文件和車站信息表（Excel表格，含聯鎖系統與外部系統的接口文件信息），這些文件需要由翻譯器軟件Translator來進行翻譯轉換，其中，VTL文件轉換為SEIF文件，TLE文件轉換為LCF文件，車站信息表格轉換LCF文件。

翻譯器軟件Translator的數據處理流程如圖 2所示。

圖2 翻譯器軟件的數據處理流程Fig.2 Data process flow chart of translator software

翻譯器軟件按功能可分為VTL、QDZ、HDW等7大子模塊，分別實現各類接口文件的翻譯及輸出。以其中的站場圖翻譯子模塊為例，接口數據翻譯流程說明如圖 3所示。

圖3 站場圖數據翻譯流程Fig.3 Flow chart of translation of station/yard data

3 形式化翻譯器軟件的OCaml實現

3.1 函數式編程語言OCaml簡介

1985年，法國高等師范學院（ENS）發布了范疇論抽象機器語言（Categorical Abstract Machine Language，Caml），之后主要由法國國立計算機及自動化研究院（INRIA）負責維護。1996年，函數式編程語言（OCaml）發布了第一個版本，其在Caml的基礎上支持了面向對象編程。

ML（Meta Language）語言是OCaml的祖先，設計之初的種種特性都是為了便于開發其他語言的編譯器。OCaml作為繼承者，在開發其他編程語言方面也是碩果累累，如形式化證明的經典工具Coq、金融量化交易軟件、Microsoft的OCaml方言F#等。

OCaml是一種多范式的編程語言，可以進行命令式編程，同時OCaml也支持面向對象程序設計（Object Oriented Programming，OOP）。然而OCaml最提倡的還是函數式編程。其實現了代數類型系統、類型推導、高階函數、尾遞歸、模式匹配、詞法作用域、參數化模塊等特性，自誕生之日起一直是主流的函數式編程語言。OCaml默認是嚴格求值的（也支持惰性求值），與用戶的習慣接近，使程序的行為更容易預測。合理使用OCaml提供的基礎設計，可以得到非常簡潔有效的代碼。

OCaml語言主要有如下優點。

1）Ocaml是一種功能強大的類型系統，具有參數多態性及類型推理。

2）提供用戶可定義的代數數據類型和模式匹配。新的代數數據類型可以定義為記錄和總和的組合，通過模式匹配（match）定義在此類數據結構上運行的函數，它提供了一種同時檢查和命名數據的方式。

3）具有自動內存管理功能，這歸功于一個快速、不顯眼的增量垃圾回收器。

4）具有獨立應用程序的單獨編譯功能。

綜上所述，OCaml適合編寫高性能、專門性強、結構復雜、正確度高、安全性好的軟件，目前一般用于編譯器、程序分析、金融交易、虛擬機等方面的軟件開發。

3.2 輸入文件參數與結構定義

TLE文件中設備的基本數據結構包含元素列表、標簽名稱及屬性列表等，如圖 4所示。

圖4 TLE數據結構定義Fig.4 Definition of TLE data structure

讀取TLE數據時，每類設備的結構均有所定義，如道岔、信號機、區段等，最終整體上采用哈希表來表示所采集提取到的設備集合，如圖 5所示。

圖5 設備結構定義Fig.5 Definition of equipment structure

3.3 翻譯邏輯的OCaml實現

OCaml代碼通過使用列表、哈希表，充分利用了OCaml語言的類型推斷、模式匹配、參數化模塊和高階函數等特性，使程序變得非常簡潔且安全可靠。

針對TLE文件，read_elem函數依次讀取數據中的元素，具體實現如圖 6所示。該函數中應用rec關鍵字來實現遞歸函數，同時應用match with語句來實現所有字符串的正則表達式匹配，通過“|”來實現簡潔的模式匹配，如果遇到未匹配情況，會給出相應的提示信息。

圖6 讀取數據元素Fig.6 Read the data element

3.4 翻譯結果的數據處理

翻譯后的結果數據通過打包、存儲等過程，存入相應的LCF文件中，用作Prover iLock軟件的驗證輸入。

LCF文件的結構體定義如圖 7所示。

圖7 LCF文件結構體定義Fig.7 Definition of LCF file structure

對數據進行翻譯轉換，函數定義和實現如圖 8所示。

圖8 翻譯轉換函數Fig.8 Translation conversion function

打包的數據集通過emit_tables函數輸出到指定文件，結果如圖 9所示。

圖9 翻譯結果LCF文件格式與內容Fig.9 Format and content of LCF file

4 結束語

本文通過函數式編程語言OCaml開發的形式化驗證翻譯器軟件，利用其獨有的安全特性，將聯鎖系統的TLE、VTL等輸入文件翻譯為LCF/SEIF文件等，用作Prover公司形式化軟件iLock的驗證輸入，在處理流程上保障了數據的可靠性，從而提升了聯鎖系統形式化驗證的安全性和完備性。