于文濤

摘要：隨著軌道交通跨越式發(fā)展，越來越多的現(xiàn)代科技、國防和國民經(jīng)濟(jì)領(lǐng)域依賴軌道交通。軌道交通的安全性和可靠性成為國家和人民關(guān)注的重點。由于軌道交通領(lǐng)域的特殊性，傳統(tǒng)的模擬和測試方法不能保證軟件和硬件的可靠性。形式化方法可以保證從軟件需求到軟件編碼全過程的邏輯一致性。最近幾年，工程和學(xué)術(shù)界廣泛使用形式化驗證來對軟件進(jìn)行建模。該文介紹了形式化驗證在軌道交通領(lǐng)域的應(yīng)用，這包括軟件需求、設(shè)計的形式化描述和軟件的形式化建模。

關(guān)鍵詞：軌道交通；形式化驗證；形式化建模；形式化方法

中圖分類號：TP301 文獻(xiàn)標(biāo)識碼：A 文章編號：1009-3044（2018）13-0263-02

1 背景

隨著一帶一路戰(zhàn)略性規(guī)劃的穩(wěn)步推進(jìn)，軌道交通作為我國國民經(jīng)濟(jì)的命脈，其發(fā)展獲得了令人矚目的成績。無論是硬件方面還是軟件方面，軌道交通的安全性和可靠性一直是工程師關(guān)注的重點。由于對軟件需求和設(shè)計的非形式化描述使軟件開發(fā)缺乏統(tǒng)一的標(biāo)準(zhǔn)，使得軌道交通領(lǐng)域的研發(fā)受到限制。近年來，無論是在硬件設(shè)計還是軟件系統(tǒng)方面，形式化驗證（Formal Verification）取得了一批有規(guī)模的實用型研究成果，其中在軌道交通領(lǐng)域也取得了巨大的進(jìn)展。該文介紹了在軌道交通領(lǐng)域如何使用形式化方法對系統(tǒng)進(jìn)行建模和分析。

2 形式化驗證的概念

形式化驗證通過對系統(tǒng)進(jìn)行窮盡搜索來進(jìn)行驗證，它以某個或某些形式的規(guī)范或?qū)傩詾橐罁?jù)，使用數(shù)學(xué)的方法證明其正確性。形式化驗證使用嚴(yán)格的數(shù)學(xué)推理來表明設(shè)計符合其全部或部分規(guī)范，這就要求使用形式化的描述來表達(dá)規(guī)范和實現(xiàn)。這些描述由符號框架給出，其形式語義明確地將數(shù)學(xué)對象與每個描述相關(guān)聯(lián)，允許這些對象在正式的數(shù)學(xué)框架中被操縱。形式化驗證可以分為三類：等價性驗證（Equivalence Checking）、模型檢驗（Model Checking）和定理證明（Theorem Prover）。

等價性驗證的基本思想是驗證兩個電路模型結(jié)構(gòu)是否等價[1]。主要用于驗證門級與門級之間、RTL級與門級之間是否一致。在時鐘樹綜合和掃描鏈重排等過程中，等價性檢驗可以確保門級網(wǎng)表的一致性。對于設(shè)計者手誤導(dǎo)致的門級網(wǎng)表錯誤，等價性驗證可以通過檢測不一致來發(fā)現(xiàn)其中的錯誤。

模型檢驗用時態(tài)邏輯來描述規(guī)范，通過生成窮盡的且有效的搜索方法來檢測系統(tǒng)是否滿足給定的規(guī)范。主要是對系統(tǒng)或模型的運行狀態(tài)創(chuàng)建一個有限自動機(jī)的抽象模型M，使用形式化語言對所要驗證的性質(zhì)創(chuàng)建描述規(guī)范說明。模型檢驗可以自動運行，不需要人工給出窮盡的測試用例來判斷模型M是否能滿足規(guī)范說明。模型檢驗?zāi)茏詣赢a(chǎn)生使命題不成立的反例，以解釋命題不成立的原因[2]。

定理證明把系統(tǒng)與規(guī)范都使用數(shù)學(xué)邏輯公式來表示，通過判斷數(shù)學(xué)公理的正確性來尋求系統(tǒng)的描述。定理證明被用來表明實現(xiàn)的是規(guī)范的一個改進(jìn)，這個實現(xiàn)在功能單元、寄存器級或門級被描述。

3 形式化建模

形式化驗證使用嚴(yán)格的數(shù)學(xué)概念和語言，根據(jù)系統(tǒng)的需求來描述軟件的定義和語義，從而對系統(tǒng)建模。從廣義上講，形式化建模是離散數(shù)學(xué)在軟件工程上的應(yīng)用，其涉及建模和分析，并具有數(shù)學(xué)上精確的符號。從狹義上講，形式化建模是一系列具有明確定義的字符串，并且?guī)в幸惶渍降囊?guī)則來定義它的語法和語義。規(guī)則可以用來分析表達(dá)式，以確定它們是否在語法上良好地描述或證明它們的屬性。目前有兩種使用比較多的形式化建模語言，分別是Petri網(wǎng)和Pi驗算。Petri網(wǎng)于20世紀(jì)60年代由Carl Adam Petri發(fā)明的。主要使用數(shù)學(xué)方式來描述離散并行系統(tǒng)，并且多用于對描述異步的、并發(fā)的系統(tǒng)進(jìn)行建模。Pi演算是Robin Milner在20世紀(jì)80年代提出的，用于描述和分析并發(fā)系統(tǒng)，并用演算來描述進(jìn)程之間的動態(tài)演化[3]。

4 軌道交通領(lǐng)域的應(yīng)用

近年來，作為國內(nèi)外熱門研究點，形式化驗證發(fā)展迅速，相對于大規(guī)模測試，它從邏輯上驗證了系統(tǒng)是否正確。形式化方法已成為確保軟硬件設(shè)計質(zhì)量和正確性的替代方法，克服了傳統(tǒng)驗證技術(shù)（如仿真和測試）的一些局限性。形式化方法在工程上的應(yīng)用涉獵廣泛，主要有兩個方面：用于指定設(shè)計所需屬性的正式框架，以及用于推導(dǎo)規(guī)范與相應(yīng)實現(xiàn)之間關(guān)系的驗證技術(shù)和工具。形式化驗證已經(jīng)被用于各種應(yīng)用程序中，包括通信協(xié)議、硬件功能、軟件功能和安全。這些應(yīng)用表明，在一定條件下，形式化驗證不受仿真指數(shù)增長率的影響，其機(jī)制保證了被證明的行為是通過物理設(shè)備的抽象模型來實現(xiàn)的。許多工程師使用形式化方法對汽車電子基礎(chǔ)軟件進(jìn)行驗證，以確保其安全性。

在軌道交通領(lǐng)域，形式化驗證被更多地用于對系統(tǒng)的需求和設(shè)計進(jìn)行形式化描述。文獻(xiàn)[4]通過使用時間自動機(jī)網(wǎng)絡(luò)模型對軌道交通運行控制系統(tǒng)進(jìn)行形式化建模和驗證，并使用時間自動機(jī)模型對系統(tǒng)的需求和設(shè)計進(jìn)行精確描述，從而大大提高了軌道交通列車運行控制系統(tǒng)的安全性和可靠性設(shè)計水平。形式化建?？梢暂o助技術(shù)人員對系統(tǒng)描述進(jìn)行建模。文獻(xiàn)[5]使用進(jìn)程代數(shù)方法對AUTOSAR存儲保護(hù)機(jī)制建立形式化模型，從而實現(xiàn)一種操作系統(tǒng)的存儲保護(hù)機(jī)制。文獻(xiàn)[6]使用層次化有色Petri網(wǎng)，依據(jù)信號聯(lián)鎖邏輯的系統(tǒng)描述，對鐵路車輛計算機(jī)聯(lián)鎖軟件進(jìn)行形式化建模。形式化驗證可以給出系統(tǒng)的安全性和可靠性分析。文獻(xiàn)[7]在高速鐵路列控中心引入安全因子概念，采用安全行為模型，對不同類型的列控中心軟件行為進(jìn)行定義，從而實現(xiàn)對高鐵列控中心的安全描述。文獻(xiàn)[8]建立隨機(jī)Petri網(wǎng)表示的CTCS無線通信機(jī)制模型，證明了Petri網(wǎng)可以輔助在移動閉塞區(qū)間對高速列車進(jìn)行形式化建模和可靠性分析，并給出了故障定位信息的描述方法。形式化驗證工具UPPAAL是用于實時驗證系統(tǒng)的工具箱。它由兩個主要部分組成：圖形用戶界面和模型檢查器引擎。用戶界面以Java實現(xiàn)，并在用戶工作站上執(zhí)行。UPPAAL在工程界被廣泛用于實現(xiàn)系統(tǒng)的仿真和分析。文獻(xiàn)[9]利用時間自動機(jī)理論對車輛與地面交互流程進(jìn)行建模，并使用形式化驗證工具UPPAAL來模擬和分析對CTCS-3級列控系統(tǒng)。

5 結(jié)束語

形式化驗證在軌道交通的各個層次都得到了應(yīng)用，包括需求、設(shè)計、建模和分析階段。相對于傳統(tǒng)的模擬和測試方法，形式化驗證不需要窮盡測試用例，更高效準(zhǔn)確地保證了軌道交通系統(tǒng)的安全性和可靠性。

參考文獻(xiàn)：

[1] 楊澤民， 范全潤. 硬件設(shè)計的形式化驗證技術(shù)[J]. 太原師范學(xué)院學(xué)報： 自然科學(xué)版， 2007， 6（2）： 54-56.

[2] 沈勝宇. 模型檢驗的反例解釋[D]. 長沙： 國防科學(xué)技術(shù)大學(xué)， 2005.

[3] 周建儒. 軟件形式化建模方法探析[J]. 河北軟件職業(yè)技術(shù)學(xué)院學(xué)報， 2016， 18（2）： 48-50.

[4] 燕飛. 軌道交通列車運行控制系統(tǒng)的形式化建模和模型檢驗方法研究[D]. 北京： 北京交通大學(xué)， 2006.

[5] 李青， 朱曉冉， 郭建. AUTOSAR OS存儲保護(hù)機(jī)制的形式化驗證框架[J]. 計算機(jī)工程， 2017， 43（1）： 79-85.

[6] 陳邦興， 吳芳美. 鐵路信號聯(lián)鎖邏輯形式化建模研究[J]. 鐵道學(xué)報， 2002， 24（6）： 50-54.

[7] 喻鋼， 劉曉文， 熊靜， 等. 高速鐵路列控中心軟件安全性需求形式化建模[J]. 鐵道學(xué)報， 2013， 35（7）： 74-79.

[8] 陳永， 王曉明， 黨建武， 等. 基于SPN的CTCS無線通信形式化建模與分析[J]. 鐵道學(xué)報， 2011， 33（8）： 63-68.

[9] 劉中田， 呂繼東， 孫偉亮. CTCS-3級列控系統(tǒng)車地交互流程形式化建模與驗證[J]. 北京交通大學(xué)學(xué)報， 2011， 35（2）： 76-81.