王紹新，王燕芩，閆連山

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

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

1 聯(lián)鎖系統(tǒng)形式化驗證

1.1 形式化在軌道交通領域的應用現(xiàn)狀

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

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

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

1.2 聯(lián)鎖系統(tǒng)的形式化驗證流程

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

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

驗證流程如圖 1所示。

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

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

2 翻譯器軟件設計

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

翻譯器軟件Translator的數(shù)據(jù)處理流程如圖 2所示。

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

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

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

3 形式化翻譯器軟件的OCaml實現(xiàn)

3.1 函數(shù)式編程語言OCaml簡介

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

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

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

OCaml語言主要有如下優(yōu)點。

1）Ocaml是一種功能強大的類型系統(tǒng)，具有參數(shù)多態(tài)性及類型推理。

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

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

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

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

3.2 輸入文件參數(shù)與結構定義

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

圖4 TLE數(shù)據(jù)結構定義Fig.4 Definition of TLE data structure

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

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

3.3 翻譯邏輯的OCaml實現(xiàn)

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

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

圖6 讀取數(shù)據(jù)元素Fig.6 Read the data element

3.4 翻譯結果的數(shù)據(jù)處理

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

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

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

對數(shù)據(jù)進行翻譯轉換，函數(shù)定義和實現(xiàn)如圖 8所示。

圖8 翻譯轉換函數(shù)Fig.8 Translation conversion function

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

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

4 結束語

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