形式化方法應(yīng)用于計(jì)算機(jī)聯(lián)鎖軟件的安全驗(yàn)證研究

羅 娟，王燕芩

（卡斯柯信號(hào)有限公司，上海 200071）

形式化方法應(yīng)用于計(jì)算機(jī)聯(lián)鎖軟件的安全驗(yàn)證研究

羅 娟，王燕芩

（卡斯柯信號(hào)有限公司，上海 200071）

鐵路信號(hào)系統(tǒng)中的聯(lián)鎖系統(tǒng)對(duì)安全性要求極高，僅通過普通的功能測(cè)試無法保障其安全性。采用形式化驗(yàn)證的方式可以驗(yàn)證聯(lián)鎖系統(tǒng)的應(yīng)用邏輯與安全需求的一致性。將通用安全需求結(jié)合具體的站場(chǎng)圖進(jìn)行實(shí)例化，得到具體的安全需求后輸入帶歸納功能的布爾可滿足問題（SAT）約束求解器進(jìn)行驗(yàn)證，通過覆蓋所有的實(shí)例、所有周期以及每個(gè)周期所有的狀態(tài)空間，保證了驗(yàn)證方法的完備性。

計(jì)算機(jī)聯(lián)鎖；安全需求；通用應(yīng)用；形式化驗(yàn)證

聯(lián)鎖系統(tǒng)是涉及到生命財(cái)產(chǎn)安全的高安全性系統(tǒng)，其安全性除了體現(xiàn)在冗余結(jié)構(gòu)的系統(tǒng)硬件上，還應(yīng)考慮系統(tǒng)軟件的安全性。軟件的安全性需通過系統(tǒng)邏輯設(shè)計(jì)與安全需求的一致性和特殊的安全防護(hù)措施保證。在安全需求實(shí)現(xiàn)時(shí)，若存在系統(tǒng)需求描述不準(zhǔn)確，則會(huì)造成需求設(shè)計(jì)實(shí)現(xiàn)不準(zhǔn)確，這一系列因?yàn)槿藶槭д`可能導(dǎo)致最終的系統(tǒng)功能失效，威脅行車安全。為了確保系統(tǒng)需求的正確實(shí)現(xiàn)，本文提出形式化方法對(duì)既有聯(lián)鎖系統(tǒng)應(yīng)用進(jìn)行安全驗(yàn)證，確保系統(tǒng)實(shí)現(xiàn)與安全需求要求的一致性。聯(lián)鎖系統(tǒng)是鐵路信號(hào)系統(tǒng)中的安全相關(guān)的重要系統(tǒng)，根據(jù)EN50128的要求，聯(lián)鎖系統(tǒng)的安全性需達(dá)到SIL4的安全等級(jí)，因此對(duì)其進(jìn)行安全驗(yàn)證十分必要。

1 研究背景

對(duì)于安全相關(guān)的系統(tǒng)，在正常功能性需求外，含大量安全需求。其中，功能需求描述了系統(tǒng)正常的功能總會(huì)在未來某個(gè)正確的時(shí)刻發(fā)生，而安全需求則描述了導(dǎo)致系統(tǒng)危險(xiǎn)的情況不會(huì)發(fā)生[1]。傳統(tǒng)的開發(fā)、設(shè)計(jì)和測(cè)試的方法不能保證系統(tǒng)所有安全需求均被正確實(shí)現(xiàn)。目前，系統(tǒng)的功能需求主要通過測(cè)試的方法進(jìn)行驗(yàn)證，而安全需求則主要通過危險(xiǎn)分析（HA，Hazard Analysis）及創(chuàng)建危害日志的方法，分析和記錄系統(tǒng)可能出現(xiàn)的危險(xiǎn)。采用傳統(tǒng)的開發(fā)、測(cè)試和驗(yàn)證主要存在以下幾個(gè)方面的缺點(diǎn)：

（1）使用自然語言描述需求，需求內(nèi)容不夠明確，容易產(chǎn)生二義性，設(shè)計(jì)和測(cè)試階段均可能會(huì)出現(xiàn)因?yàn)閷?duì)需求理解的偏差而造成設(shè)計(jì)錯(cuò)誤或測(cè)試錯(cuò)誤的情況；

（2）傳統(tǒng)的測(cè)試采用人工設(shè)計(jì)測(cè)試用例的方式，對(duì)于某一個(gè)功能的所有場(chǎng)景可能無法考慮全面，從而導(dǎo)致測(cè)試用例設(shè)計(jì)不完整；

（3）傳統(tǒng)的測(cè)試過程無法覆蓋系統(tǒng)在某個(gè)測(cè)試場(chǎng)景下所有的狀態(tài)空間，導(dǎo)致系統(tǒng)運(yùn)行過程中發(fā)生的危害并不能通過測(cè)試發(fā)現(xiàn)；

（4）對(duì)于安全需求的驗(yàn)證目前主要是通過追蹤需求、設(shè)計(jì)、實(shí)現(xiàn)中的對(duì)應(yīng)關(guān)系進(jìn)行，大多僅停留在文檔的層面，無法保證軟件的實(shí)現(xiàn)完全滿足安全需求。而且多采用人工分析的方式，效率較低，需要投入較多的人力資源。

2 形式化方法簡(jiǎn)介

2.1 形式化方法

形式化方法[2]是建立在嚴(yán)格數(shù)學(xué)基礎(chǔ)上、具有精確數(shù)學(xué)語義的開發(fā)方法，能夠除去用自然語言描述而造成的需求、屬性方面的模糊定義。該方法需要對(duì)被驗(yàn)證對(duì)象進(jìn)行形式化建模，也就是將一般的需求定義抽象成數(shù)學(xué)模型，將待測(cè)系統(tǒng)抽象成可被證明的數(shù)學(xué)模型。

形式化方法可分為形式化規(guī)范描述和形式化驗(yàn)證兩大類：（1）形式化規(guī)范描述使用具有嚴(yán)格數(shù)學(xué)定義的語法和語義的規(guī)范語言來描述系統(tǒng)。被描述的系統(tǒng)特性包括行為特性、時(shí)間特性、性能特性和內(nèi)部結(jié)構(gòu)等。采用形式化語言將非形式化的（Informal）需求進(jìn)行形式化（Formal）描述，從系統(tǒng)設(shè)計(jì)的開始階段就努力降低系統(tǒng)的故障率，可以節(jié)省大量后期調(diào)試、修改成本。（2）形式化驗(yàn)證是通過數(shù)學(xué)證明的方式，自動(dòng)化的驗(yàn)證系統(tǒng)在一定的前提條件下滿足各種靜態(tài)和動(dòng)態(tài)性質(zhì)。

2.2 形式化驗(yàn)證主要技術(shù)

形式化驗(yàn)證的主要技術(shù)包括模型檢驗(yàn)和定理證明：（1）模型檢驗(yàn)是一種基于有限狀態(tài)模型并檢驗(yàn)該模型的期望特性的技術(shù)。它對(duì)模型的狀態(tài)空間進(jìn)行遍歷搜索，以確認(rèn)該系統(tǒng)模型是否具有某些性質(zhì)。（2）定理證明則是選定一個(gè)數(shù)學(xué)邏輯體系，用體系中的公式描述系統(tǒng)和系統(tǒng)性質(zhì)。依據(jù)該體系中的公理和定理，推導(dǎo)系統(tǒng)性質(zhì)的描述公式。

定理證明因其在驗(yàn)證過程中需要人工交互而導(dǎo)致自動(dòng)化程度不高，相比于定理證明，以模型檢驗(yàn)的方法則可以對(duì)系統(tǒng)變量進(jìn)行全狀態(tài)空間的檢驗(yàn)和證明，在提升系統(tǒng)狀態(tài)覆蓋完備性同時(shí)，提高了驗(yàn)證的自動(dòng)化程度。

法國(guó)巴黎地鐵14號(hào)線的自動(dòng)駕駛系統(tǒng)就是用形式化方法開發(fā)并驗(yàn)證的，1998年投入運(yùn)行，至今未發(fā)現(xiàn)任何缺陷。法國(guó)戴高樂機(jī)場(chǎng)用于接送乘客無人駕駛線路也應(yīng)用形式化方法對(duì)系統(tǒng)安全性進(jìn)行了驗(yàn)證。

3 聯(lián)鎖系統(tǒng)軟件的形式化驗(yàn)證

隨著鐵路信號(hào)控制系統(tǒng)的復(fù)雜性在不斷地增加，世界各大業(yè)主和信號(hào)廠商也越來越重視形式化方法的應(yīng)用：（1）形式化驗(yàn)證方法從系統(tǒng)的安全需求出發(fā)，通過模型檢驗(yàn)，證明系統(tǒng)的安全需求已經(jīng)實(shí)現(xiàn)且系統(tǒng)功能滿足安全需求的要求，驗(yàn)證系統(tǒng)安全性確實(shí)滿足既定要求；（2）通過驗(yàn)證，檢驗(yàn)系統(tǒng)在安全實(shí)現(xiàn)上的缺陷，做到查漏補(bǔ)缺，能夠早發(fā)現(xiàn)，早解決，為系統(tǒng)的安全提供安全保障；（3）形式化驗(yàn)證在系統(tǒng)的全狀態(tài)空間的搜索過程中，能夠完整檢驗(yàn)系統(tǒng)在任意狀態(tài)可能潛在的風(fēng)險(xiǎn)問題，增強(qiáng)產(chǎn)品信心。

將安全需求的形式化驗(yàn)證方法應(yīng)用于聯(lián)鎖系統(tǒng)，需要考慮在實(shí)際控制應(yīng)用過程中的特殊性。聯(lián)鎖系統(tǒng)軟件內(nèi)部邏輯主要是布爾邏輯，從狀態(tài)空間的角度出發(fā)，對(duì)其進(jìn)行模型檢驗(yàn)更為可行。對(duì)于聯(lián)鎖系統(tǒng)而言，危及行車安全的風(fēng)險(xiǎn)主要有列車或車列迎面沖撞、側(cè)面沖撞、追尾沖撞、錯(cuò)道、擠岔和掉道等。對(duì)于一個(gè)完善的聯(lián)鎖系統(tǒng)，除了要通過測(cè)試說明各項(xiàng)功能需求被正確無誤的實(shí)現(xiàn)，還必須要驗(yàn)證導(dǎo)致上述各種危險(xiǎn)的事件不可能發(fā)生。采用歸納驗(yàn)證和模型檢驗(yàn)相結(jié)合的形式化驗(yàn)證方法用于確保系統(tǒng)的輸出確實(shí)無法導(dǎo)致危險(xiǎn)事件發(fā)生。其中，通過模型檢驗(yàn)可以覆蓋每一個(gè)周期的所有狀態(tài)空間，而通過歸納驗(yàn)證，則可以覆蓋所有的周期。

3.1 驗(yàn)證流程

本文所描述的是通過開發(fā)通用的形式化安全需求，結(jié)合具體站型對(duì)實(shí)例化后的既有聯(lián)鎖應(yīng)用進(jìn)行形式化驗(yàn)證的過程。其中，所涉及到的聯(lián)鎖系統(tǒng)邏輯的通用應(yīng)用和特定應(yīng)用都是以布爾表達(dá)式進(jìn)行描述。對(duì)聯(lián)鎖系統(tǒng)特定應(yīng)用進(jìn)行形式化驗(yàn)證的過程如圖1所示，主要包括：（1）聯(lián)鎖系統(tǒng)安全需求通用建模及針對(duì)特定應(yīng)用的配置，即圖中兩個(gè)虛線框內(nèi)的部分。這兩部分完成后，就可以直接輸入到實(shí)例化工具中，將通用安全性質(zhì)實(shí)例化為針對(duì)特定站場(chǎng)的特定安全性質(zhì)；（2）將特定安全性質(zhì)輸入到帶有歸納證明功能的模型檢驗(yàn)的驗(yàn)證器中進(jìn)行形式化驗(yàn)證，得到最終的結(jié)果，并通過對(duì)最終結(jié)果的分析確定系統(tǒng)是否滿足相關(guān)的安全性質(zhì)。其中，針對(duì)安全需求通用建模，主要是建立聯(lián)鎖信號(hào)設(shè)備的邏輯模型，用以描述聯(lián)鎖功能上的邏輯關(guān)系，同時(shí)，設(shè)計(jì)形式化安全需求與應(yīng)用的接口，以實(shí)現(xiàn)后續(xù)安全需求實(shí)例化。

圖1 聯(lián)鎖軟件形式化驗(yàn)證流程

3.2 安全需求形式化描述

為了能夠?qū)崿F(xiàn)安全需求的形式化驗(yàn)證，要求驗(yàn)證輸入的需求必須以形式化方式進(jìn)行描述。用于安全需求形式化描述的語言很多，本文提出了一種基于面向?qū)ο蠹夹g(shù)和一階謂詞邏輯[3]的形式化語言。

面向?qū)ο蟮募夹g(shù)可以很好地對(duì)驗(yàn)證系統(tǒng)的各功能模塊及控制對(duì)象進(jìn)行建模，而一階謂詞邏輯能夠清楚地描述各個(gè)控制對(duì)象之間的聯(lián)鎖關(guān)系，且能夠通過實(shí)例化和變換轉(zhuǎn)變?yōu)槲鋈》妒?，便于?yàn)證器進(jìn)行驗(yàn)證。該語言由基本的邏輯操作符（如and,or,not,=＞）、量詞（如ALL,EXIT）組成，具有面向?qū)ο蟮睦^承、方法重載等特性?；镜牟僮髟厥菍?duì)象，每個(gè)對(duì)象屬于一個(gè)類，類包括屬性、函數(shù)、等式等字段。例如，對(duì)于安全需求“進(jìn)路開放，則進(jìn)路上的區(qū)段空閑”而言，對(duì)該條安全需求采用形式化方式描述后即為：

"ALL rt(rt.route_clear =＞ ALL seg(rt.segment(seg) =＞seg.vacant))",(PO1)

其中，rt,seg分別為事先定義的控制對(duì)象的應(yīng)用實(shí)例，route_clear,segment，vacant是控制對(duì)象需實(shí)現(xiàn)的功能函數(shù)。

3.3 安全需求實(shí)例化

本文所述的聯(lián)鎖系統(tǒng)形式化驗(yàn)證的應(yīng)用是對(duì)具體的聯(lián)鎖應(yīng)用邏輯進(jìn)行形式化驗(yàn)證，而上述形式化安全需求是從通用角度進(jìn)行描述的，因此，為了能夠進(jìn)行最終的驗(yàn)證工作，還需要對(duì)安全需求進(jìn)行實(shí)例化。從通用的安全需求轉(zhuǎn)換為針對(duì)具體某個(gè)站的安全需求的過程稱為安全需求實(shí)例化。安全需求實(shí)例化實(shí)際就是將每條形式化安全需求中的對(duì)象實(shí)例化為站場(chǎng)上對(duì)應(yīng)的設(shè)備，而功能函數(shù)則通過函數(shù)描述的關(guān)系最終轉(zhuǎn)換為每個(gè)設(shè)備對(duì)應(yīng)的參數(shù)。從數(shù)學(xué)層面來看，整個(gè)實(shí)例化的過程就是在類實(shí)例化和函數(shù)映射的基礎(chǔ)上移除全稱量詞和存在量詞的過程。由于這一過程完全可以通過面向?qū)ο蠹夹g(shù)結(jié)合相應(yīng)的數(shù)學(xué)原理實(shí)現(xiàn)，因此這一過程可以由工具自動(dòng)完成。

3.4 安全需求與通用應(yīng)用接口

由于是對(duì)既有聯(lián)鎖應(yīng)用進(jìn)行形式化驗(yàn)證，而聯(lián)鎖系統(tǒng)邏輯并非用上文提出的形式化語言進(jìn)行設(shè)計(jì)和描述，因此，從形式化語言到聯(lián)鎖通用應(yīng)用邏輯之間必須建立映射關(guān)系，以支持安全需求的實(shí)例化。

安全需求與通用應(yīng)用接口主要包括以下工作：站場(chǎng)信號(hào)設(shè)備面向?qū)ο蠼！⒄緢?chǎng)平面圖信息讀取、信號(hào)設(shè)備模型與站場(chǎng)圖和通用應(yīng)用的映射。

3.4.1 站場(chǎng)信號(hào)設(shè)備面向?qū)ο蠼?/p>

結(jié)合聯(lián)鎖系統(tǒng)功能，在建模時(shí)，通用設(shè)備對(duì)象的分類采用面向?qū)ο蟮姆绞?，因此，需要?duì)信號(hào)設(shè)備分類，主要包括：進(jìn)路、信號(hào)機(jī)、道岔、軌道區(qū)段，上述這些設(shè)備均可作為父類。如進(jìn)路又包括列車進(jìn)路、調(diào)車進(jìn)路、非進(jìn)路等。信號(hào)機(jī)根據(jù)不同的作用可分為：列車信號(hào)機(jī)、調(diào)車信號(hào)機(jī)和列車兼調(diào)車信號(hào)機(jī)。列車信號(hào)機(jī)主要是用來作為列車進(jìn)路的始端或終端，調(diào)車信號(hào)機(jī)可以作為調(diào)車進(jìn)路的始端和終端，而列車兼調(diào)車信號(hào)機(jī)，既可以作為列車進(jìn)路的始終端，又可作為調(diào)車進(jìn)路的始終端，但同一時(shí)間只能作為一種進(jìn)路的始端或終端。上述給出的是基本的信號(hào)設(shè)備分類，考慮復(fù)雜的情況時(shí)還可以進(jìn)一步擴(kuò)展。對(duì)于每一個(gè)類，需要設(shè)計(jì)相應(yīng)的參數(shù)、函數(shù)和等式。參數(shù)是可以直接從站場(chǎng)圖中獲得的信息，如信號(hào)設(shè)備之間的位置關(guān)系等；函數(shù)是信號(hào)設(shè)備的狀態(tài)或功能描述，如信號(hào)機(jī)的開放或關(guān)閉狀態(tài)；等式與函數(shù)很類似，但是與周期相關(guān)，即等式左邊計(jì)算得到的值都是下一周期的值，需要使用本周期的值進(jìn)行計(jì)算。另外，由于進(jìn)路是由信號(hào)機(jī)、道岔和軌道電路組成，因此，還需要設(shè)計(jì)進(jìn)路和其他3種設(shè)備之間的關(guān)系。圖2所示為信號(hào)設(shè)備的面向?qū)ο蟮年P(guān)系圖。

圖2 信號(hào)設(shè)備面向?qū)ο蠼Ｊ疽鈭D

3.4.2 站場(chǎng)平面圖信息讀取

站場(chǎng)平面圖信息的讀取是為了提取出信號(hào)設(shè)備的屬性以及各信號(hào)設(shè)備之間的拓?fù)潢P(guān)系，并將相關(guān)的信息傳給對(duì)象結(jié)構(gòu)中的函數(shù)和參數(shù)。站場(chǎng)平面圖的描述一般采用結(jié)構(gòu)化的文件進(jìn)行，內(nèi)部包括各種數(shù)據(jù)結(jié)構(gòu)。本文描述的是以XML格式的站場(chǎng)圖的信息提取。XML中包含的信號(hào)設(shè)備相關(guān)的字段主要有：SIGNAL,TRACK,SWITCH,ROUTE等，當(dāng)然還包括一些零散的按鈕和表示燈，在此就不進(jìn)行介紹。表1以道岔為例，給出了其在站場(chǎng)描述文件中對(duì)應(yīng)的各種字段。

表1 道岔屬性表

3.4.3 信號(hào)設(shè)備模型與站場(chǎng)圖和通用應(yīng)用的映射

為了對(duì)信號(hào)設(shè)備以及安全需求進(jìn)行實(shí)例化，需要建立信號(hào)設(shè)備模型到站場(chǎng)圖和通用應(yīng)用之間的映射關(guān)系，這里的映射關(guān)系包括兩層：（1）信號(hào)設(shè)備模型到站場(chǎng)圖的映射，進(jìn)行該映射可以將站場(chǎng)圖上的具體的信號(hào)設(shè)備與信號(hào)設(shè)備類聯(lián)系起來，得到信號(hào)設(shè)備實(shí)例以及每個(gè)實(shí)例對(duì)應(yīng)的拓?fù)潢P(guān)系相關(guān)的參數(shù)值。以信號(hào)機(jī)為例，根據(jù)type確定信號(hào)機(jī)父類，根據(jù)subtype確定子類，這樣就可以產(chǎn)生一個(gè)信號(hào)機(jī)實(shí)例，再根據(jù)其他字段，可得到實(shí)例中相關(guān)參數(shù)的取值。（2）信號(hào)設(shè)備類中的函數(shù)、變量到通用應(yīng)用邏輯中實(shí)際變量之間的映射，如對(duì)于軌道區(qū)段， TRACK類會(huì)有一個(gè)vacant的函數(shù)，用來表示區(qū)段的占用或空閑狀態(tài)，那么在通用應(yīng)用邏輯中會(huì)有一個(gè)相同含義的變量，如：用布爾變量DGJ表示區(qū)段占用（DGJ=0）或空閑（DGJ=1）。表2列出了一些主要的函數(shù)映射關(guān)系。

表2 主要信號(hào)設(shè)備類函數(shù)與聯(lián)鎖應(yīng)用邏輯變量映射表

4 形式化驗(yàn)證實(shí)現(xiàn)

在聯(lián)鎖系統(tǒng)中，信號(hào)開放必須檢查其內(nèi)方軌道區(qū)段處于空閑狀態(tài)[4]。由此出發(fā)，建立驗(yàn)證該安全需求的通用應(yīng)用，即：若進(jìn)路始端信號(hào)開放，則進(jìn)路內(nèi)方所有區(qū)段應(yīng)空閑。在描述安全需求的通用驗(yàn)證模型外，必須結(jié)合特定的站型對(duì)通用模型進(jìn)行實(shí)例化，以檢驗(yàn)建立的通用模型滿足安全需求，達(dá)到對(duì)安全需求驗(yàn)證的目的。

對(duì)上述安全需求進(jìn)行形式化描述后得到：

"ALL rt(rt.route_clear=＞ ALL seg(rt.segment(seg) =＞seg.vacant))"，

其中，rt表示進(jìn)路變量，seg表示區(qū)段，rt.segment(seg)表示區(qū)段seg是進(jìn)路rt的內(nèi)方區(qū)段，seg.vacant表示區(qū)段seg處于空閑狀態(tài)，route_clear表示進(jìn)路進(jìn)路始端信號(hào)開放，但由于一個(gè)信號(hào)可能會(huì)是多條進(jìn)路的始端信號(hào)，因此，將需求細(xì)化為“進(jìn)路內(nèi)方道岔位置正確，始端信號(hào)開放，則進(jìn)路內(nèi)方區(qū)段空閑”，將route_clear進(jìn)一步定義為：

"route_clear (ROUTE rt) :=

EXISTsi(rt.start_signal(si) and si.permissive and ALL sw(rt.switches(sw) =＞sw.in_required_pos(rt)))"

其中，si表示信號(hào)機(jī)，rt.start_signal(si)表示信號(hào)機(jī)si是進(jìn)路rt的起始信號(hào)機(jī)，si.permissive表示信號(hào)機(jī)si為允許狀態(tài)，sw表示道岔，rt.switches(sw)表示道岔sw是進(jìn)路rt內(nèi)方的道岔，sw.in_required_ pos(rt)表示道岔sw當(dāng)前所處的位置和進(jìn)路rt要求的位置一致。

如圖3所示：（1）進(jìn)站信號(hào)機(jī)X的防護(hù)進(jìn)路有3條，X-S1，X-SII，X-S3，對(duì)應(yīng)的進(jìn)路就會(huì)被實(shí)例化為上述3條；（2）根據(jù)站場(chǎng)圖中的拓?fù)潢P(guān)系去實(shí)例化這3條進(jìn)路的起始信號(hào)機(jī)、內(nèi)方的道岔和區(qū)段；（3）當(dāng)無論當(dāng)前建立的進(jìn)路是這3條進(jìn)路中的哪一條時(shí)，驗(yàn)證結(jié)果均滿足安全需求，才能夠得到對(duì)于X信號(hào)機(jī)而言，滿足“信號(hào)開放，進(jìn)路內(nèi)區(qū)段空閑”的安全性質(zhì)。

圖3 簡(jiǎn)單站場(chǎng)圖示例

根據(jù)上述的站場(chǎng)圖以及相關(guān)的映射關(guān)系進(jìn)行實(shí)例化后共可以得到24條具體的安全需求并且全部通過驗(yàn)證。

實(shí)例化后進(jìn)行安全驗(yàn)證主要是使用了帶有歸納功能的布爾可滿足問題（SAT）約束求解器進(jìn)行模型檢驗(yàn)。其中，SAT約束求解器的基本原理可以參見[5～8]。而歸納功能是針對(duì)聯(lián)鎖系統(tǒng)不同的周期而言的，SAT約束求解器只能針對(duì)一個(gè)周期進(jìn)行求解，如果要求在任何周期都滿足，那么就需要結(jié)合歸納法：（1）檢查在初始周期是否滿足相關(guān)的性質(zhì)；（2）假設(shè)某一個(gè)周期K，系統(tǒng)滿足相關(guān)的性質(zhì)，進(jìn)而去證明K+1個(gè)周期時(shí)，相關(guān)的性質(zhì)也能夠得到滿足，那么就可以得到系統(tǒng)在任何時(shí)候都滿足對(duì)應(yīng)的性質(zhì)。

5 結(jié)束語

聯(lián)鎖系統(tǒng)是安全相關(guān)的系統(tǒng)，其安全性僅僅通過測(cè)試無法保障，通過形式化驗(yàn)證的方式，可以遍歷環(huán)境模型約束下每條安全需求每個(gè)周期的所有狀態(tài)空間，而由于聯(lián)鎖系統(tǒng)軟件邏輯結(jié)構(gòu)比較簡(jiǎn)單，狀態(tài)空間大小適中，對(duì)驗(yàn)證器的要求并不高，因此可以很好地進(jìn)行形式化驗(yàn)證。本文所應(yīng)用的方法可以在不開發(fā)形式化的通用應(yīng)用模型的前提下，進(jìn)行安全需求的驗(yàn)證，只需要開發(fā)通用應(yīng)用模型與安全需求之間的接口即可，適用于對(duì)既有的聯(lián)鎖應(yīng)用進(jìn)行驗(yàn)證，可以作為聯(lián)鎖應(yīng)用開發(fā)過程中的安全補(bǔ)強(qiáng)，增加對(duì)特定聯(lián)鎖應(yīng)用安全性的信心。而且不需要從需求階段就建立形式化模型，應(yīng)用難度遠(yuǎn)小于一般的形式化方法。從驗(yàn)證的結(jié)果可以看到，通過對(duì)安全需求建模，對(duì)其進(jìn)行實(shí)例化，再使用帶歸納法的SAT約束求解器對(duì)實(shí)例化后的安全需求進(jìn)行驗(yàn)證，可以很好地發(fā)現(xiàn)應(yīng)用邏輯中不滿足安全需求的地方，從而實(shí)現(xiàn)安全驗(yàn)證的目的。本文中所介紹的方法已經(jīng)在相關(guān)實(shí)驗(yàn)項(xiàng)目中應(yīng)用，使用真實(shí)的站型驗(yàn)證了其可行性。

[1]Nicolas Halbwachs,FabienneLagnier,Christophe Ratel.Programming and Verifying Real-TimeSystems by Means of the SynchronousData-Flow Language LUSTR[J].IEEE Transactions of Software Engineering,1992,18(9):785-793.

[2]古天龍.軟件開發(fā)的形式化方法[M].北京：高等教育出版社，2005：15-22.

[3]石純一，王家廞.數(shù)理邏輯與集合論[M].北京：清華大學(xué)出版社，2000：54-111.

[4]何文卿.6502電氣集中電路[M].北京：中國(guó)鐵道出版社，2007：112-132.

[5]童湖東，寧 濱，王海峰.基于Event-B的聯(lián)鎖進(jìn)路控制建模驗(yàn)證方法研究[J].鐵路計(jì)算機(jī)應(yīng)用，2013，22（6）：57-61.

[6]季曉慧，張 健.約束問題求解[J].自動(dòng)化學(xué)報(bào)，2007，33（2）：125-131.

[7]Y Vizel，G Weissenbacher，S Malik.Boolean Satisfiability Solvers and Their Applications in Model Checking[J].Proceedings of the IEEE,2015 (11):1-15.

[8]J Marques-Silva.Model checking with Boolean Satisfability[J].Journal of Algorithms,2008,63(1-3):3-16.

責(zé)任編輯 王 浩

Formal method applied to safety verifcation for computer interlocking software

LUO Juan,WANG Yanqin
( CASCO Signal Ltd., Shanghai 200071,China)

The Interlocking System is a safety critical system.Its safety cannot be guaranteed only by testing.Formal verifcation can be used to verify the consistency between the applied logic and the safety requirements of the System.In this article,the general safety requirements were instantiated with the specifc station layout.Then the specifc safety requirements were verifed through inputting them to the SAT induction constraint solver.The completeness of the method was guaranteed by covering all the instances,all the cycles and all the state space of each cycle.

computer based interlocking;safety requirement;general application;formal verifcation

U284.3∶TP39

A

1005-8451（2016）11-0053-05

2016-06-06

羅 娟，助理工程師；王燕芩，工程師。