華　穎,張亞東,饒　暢,胡智杰,王天成,張　琳,徐　坤

(西南交通大學(xué)信息科學(xué)與技術(shù)學(xué)院,成都　611756)

在核電、航空航天和鐵路等安全關(guān)鍵領(lǐng)域中，為降低因硬件設(shè)備故障或軟件失效帶來的系統(tǒng)安全風(fēng)險(xiǎn)，通常采用冗余技術(shù)來保證關(guān)鍵設(shè)備的可靠性和安全性。冗余，是指重復(fù)配置系統(tǒng)的一些組成部件或設(shè)備，當(dāng)系統(tǒng)部件發(fā)生故障時(shí)，冗余配置的部件介入并承擔(dān)故障部件的工作，由此減少系統(tǒng)的故障時(shí)間。系統(tǒng)設(shè)備冗余結(jié)構(gòu)主要有雙機(jī)熱備冗余、三取二冗余和二乘二取二冗余等。

二乘二取二冗余系統(tǒng)目前在計(jì)算機(jī)聯(lián)鎖、列車運(yùn)行控制系統(tǒng)等鐵路信號(hào)領(lǐng)域中廣泛使用[1]，其系統(tǒng)結(jié)構(gòu)包括4臺(tái)主機(jī)、2個(gè)比較器和1個(gè)切換器。其基本思想是雙系熱備，即該系統(tǒng)有2個(gè)熱備的子系統(tǒng)。系內(nèi)采用二取二制式，每一系分別有兩臺(tái)具有故障檢測(cè)功能的主機(jī)和一個(gè)進(jìn)行數(shù)據(jù)比較的比較器[2]。該技術(shù)結(jié)合了雙機(jī)熱備技術(shù)和二取二技術(shù)的特點(diǎn)，既具有熱備系統(tǒng)的高可靠性，又具備二取二的高安全性。

目前對(duì)二乘二取二技術(shù)的研究主要集中在冗余結(jié)構(gòu)設(shè)計(jì)和冗余功能實(shí)現(xiàn)方面，在該過程中忽略了冗余邏輯的可靠性和安全性驗(yàn)證問題。冗余邏輯一旦發(fā)生錯(cuò)誤，極有可能導(dǎo)致系統(tǒng)輸出錯(cuò)誤，進(jìn)而有可能造成各種不可預(yù)見的事故發(fā)生。本文以列控車載ATP系統(tǒng)[3](Automatic Train Protection，列車自動(dòng)防護(hù)系統(tǒng))二乘二取二冗余邏輯為研究基礎(chǔ)，針對(duì)二乘二和二取二控制軟件的冗余邏輯設(shè)計(jì)，基于UPPAAL工具建立了冗余邏輯模型，并在此基礎(chǔ)上對(duì)模型進(jìn)行了驗(yàn)證，最后根據(jù)驗(yàn)證后的邏輯模型，完成了二乘二取二邏輯的程序仿真。

1　二乘二取二系統(tǒng)分析

1.1　二乘二取二系統(tǒng)結(jié)構(gòu)和工作原理

對(duì)文獻(xiàn)[3]中提及的車載ATP系統(tǒng)，該系統(tǒng)是由2套二取二子系統(tǒng)組成的a，b雙系熱備系統(tǒng)，2套熱備系統(tǒng)之間通過切換器進(jìn)行輸出切換。對(duì)其二乘二取二邏輯功能進(jìn)行簡(jiǎn)化，得到簡(jiǎn)化后的結(jié)構(gòu)如圖1所示。

圖1　二乘二取二系統(tǒng)結(jié)構(gòu)

系統(tǒng)工作時(shí)，a、b系4臺(tái)主機(jī)同時(shí)接收數(shù)據(jù)，并監(jiān)督數(shù)據(jù)輸入工作狀態(tài)，如圖1第①步所示。若數(shù)據(jù)輸入正常，主機(jī)對(duì)接收的數(shù)據(jù)進(jìn)行校驗(yàn)，并相互通信，如圖1第②步所示。當(dāng)校驗(yàn)相等時(shí)，主機(jī)將數(shù)據(jù)傳送到比較器中進(jìn)行比較；若數(shù)據(jù)輸入錯(cuò)誤或通信中斷，主機(jī)向比較器報(bào)告故障信號(hào)，如圖1第③步所示。若比較器未收到故障信號(hào)，比較器對(duì)主機(jī)傳送的數(shù)據(jù)進(jìn)行數(shù)據(jù)比較，并將比較結(jié)果送到切換器；若比較器收到故障信號(hào)，此時(shí)比較器不進(jìn)行數(shù)據(jù)比較，并向切換器報(bào)告故障信號(hào)，如圖1第④步所示。切換器根據(jù)比較器送來的比較結(jié)果或故障信號(hào)，判定哪一系輸出[4]，如圖1第⑤步所示。若a、b兩系都正常工作，則系統(tǒng)默認(rèn)a系作為主系輸出。主系每個(gè)周期的結(jié)果數(shù)據(jù)及中間數(shù)據(jù)均傳給備系的2個(gè)主機(jī)，如圖1第⑥步所示。

對(duì)系統(tǒng)二乘二取二工作流程簡(jiǎn)化，流程如圖2所示。

圖2　系統(tǒng)工作流程

1.2　二乘二取二關(guān)鍵邏輯分析

1.2.1系統(tǒng)工作狀態(tài)分析

通過對(duì)上述二乘二取二系統(tǒng)的工作原理進(jìn)行分析，可知該系統(tǒng)存在6種工作狀態(tài)。針對(duì)該系統(tǒng)的a、b兩子系統(tǒng)，故障情況包括數(shù)據(jù)輸入錯(cuò)誤、通信中斷，系內(nèi)數(shù)據(jù)比較不相等。通過分析，得出系統(tǒng)工作狀態(tài)如表1所示。

表1　二乘二取二系統(tǒng)工作狀態(tài)

根據(jù)表1，建立對(duì)應(yīng)的系統(tǒng)狀態(tài)轉(zhuǎn)移圖，如圖3所示。

圖3　系統(tǒng)狀態(tài)轉(zhuǎn)移

1.2.2比較邏輯分析

比較器的二取二比較邏輯和切換器的二乘二切換邏輯是二乘二取二系統(tǒng)邏輯的核心組成部分。當(dāng)a1，a2機(jī)的數(shù)據(jù)輸入錯(cuò)誤或兩主機(jī)通信中斷時(shí)，會(huì)向比較器a報(bào)告故障信號(hào)。比較器a收到這個(gè)故障信號(hào)后，會(huì)向切換器發(fā)送a系故障信號(hào)。若系內(nèi)兩主機(jī)工作正常，此時(shí)比較器a將判斷發(fā)送的數(shù)據(jù)是否相等。當(dāng)兩主機(jī)的數(shù)據(jù)相等時(shí)，比較器a向切換器發(fā)送相等信號(hào)，反之則發(fā)送不等信號(hào)。通過工作流程分析，得到系統(tǒng)比較邏輯如圖4所示。

圖4　二取二比較邏輯

1.2.3切換邏輯分析

切換器的切換依據(jù)是兩系的比較器發(fā)來的比較結(jié)果或故障信號(hào)。首先判斷兩系是否報(bào)告故障信號(hào)，如果兩系均有故障信號(hào)或其中一系故障而另一系數(shù)據(jù)比較不相等，或兩系數(shù)據(jù)比較都不相等，切換器判定為故障輸出。其次切換器未收到故障信號(hào)時(shí)，判斷系內(nèi)數(shù)據(jù)比較是否相等。若切換器收到a系數(shù)據(jù)比較相等結(jié)果，則判定a系輸出；若切換器未收到a系數(shù)據(jù)比較相等結(jié)果而收到b系數(shù)據(jù)比較相等結(jié)果，則判定b系輸出。通過分析，得到系統(tǒng)切換邏輯如圖5所示。

圖5　二乘二切換邏輯

2　二乘二取二邏輯建模及驗(yàn)證

2.1　建模原理

UPPAAL是Aalborg大學(xué)和Uppsala大學(xué)聯(lián)合開發(fā)的基于時(shí)間自動(dòng)機(jī)理論的模型驗(yàn)證工具[6]。該工具由系統(tǒng)編輯器、模擬器和驗(yàn)證器3部分組成。系統(tǒng)編輯器用于創(chuàng)建和編輯要分析的模型。模擬器用于檢查所建模型的可執(zhí)行性。驗(yàn)證器使用專業(yè)的語法，通過快速搜索系統(tǒng)模型的狀態(tài)空間檢查系統(tǒng)的安全性。UPPAAL為驗(yàn)證提供了一種BNF語法，Prop：：=E < > p |A []P |E []P IA < > p |p—>q。其中：E<>p表示Possible，E<>p為真，當(dāng)且僅當(dāng)在轉(zhuǎn)換系統(tǒng)存在一個(gè)序列s0→s1→……→sn，使得s0是初始狀態(tài)，sn代表p，A[]P表示Invariantly，等價(jià)于not E<>not p；E []P表示Protentially always，E[]p為真，當(dāng)且僅當(dāng)存在一個(gè)序列s0→s1→…→si…→使得p所在狀態(tài)si中都有效，并且這個(gè)序列無窮或在狀態(tài)(sn，vn)終止；A<>p表示Eventually，等價(jià)于not E[]not p;p—>q表示Lead to，等價(jià)于A[](p imply A[]q)[7]。本文使用UPPAAL的BNF語法驗(yàn)證了兩系切換模型的安全性和可執(zhí)行性。

2.2　模型建立

根據(jù)上述分析，對(duì)系統(tǒng)邏輯進(jìn)行建模?？梢越ㄇ袚Q器、比較器模型等在內(nèi)的7個(gè)模型，還有一個(gè)系統(tǒng)運(yùn)行模型來控制整個(gè)系統(tǒng)。

各模型之間的具體聯(lián)系如圖6所示。

圖6　模型關(guān)系結(jié)構(gòu)

其中a1、a2、b1、b2為主機(jī)模型，comp1和comp2為比較器模型，switch為切換器模型，contr為系統(tǒng)運(yùn)行模型。

由于8個(gè)模型之間互相通信，需要設(shè)置通信信號(hào)使各個(gè)模型之間建立聯(lián)系。根據(jù)上述分析，本文建立了11個(gè)全局變量和4個(gè)信道來建立各個(gè)模型之間的聯(lián)系。模型的全局聲明如表2、表3所示。

表2　變量含義

表3　信道含義

根據(jù)上述的關(guān)鍵邏輯分析，比較器收到主機(jī)的各類工作狀態(tài)信號(hào)，會(huì)向切換器發(fā)送不同的結(jié)果信號(hào)。建立的比較器模型先判斷是否存在故障信號(hào)，若存在則進(jìn)入不比較狀態(tài)，不存在則進(jìn)入比較狀態(tài)。最后分別將結(jié)果發(fā)送給切換器模型。同理，切換器模型判斷各種比較器發(fā)來的結(jié)果信號(hào)，經(jīng)過邏輯運(yùn)算后，判定哪一系作為輸出。

主機(jī)模型如圖7所示。主機(jī)啟動(dòng)后，若主機(jī)未正常工作，向比較器發(fā)送a1fault信號(hào)。若主機(jī)正常工作，進(jìn)行數(shù)據(jù)計(jì)算，計(jì)算完成后向另一主機(jī)發(fā)送A1result信號(hào)，收到對(duì)方發(fā)來的信號(hào)后向比較器發(fā)送一個(gè)完成信號(hào)senda1。若未收到，主機(jī)等待直到運(yùn)行周期結(jié)束，向比較器發(fā)送通信中斷信號(hào)。切換器切換輸出后，主機(jī)判斷輸出結(jié)果。若a系輸出，即a系為主系，則向b系發(fā)送數(shù)據(jù)，以便下一周期主備系切換后繼續(xù)進(jìn)行計(jì)算。若b系輸出，則清零并等待b系發(fā)送結(jié)果數(shù)據(jù)。

圖7　主機(jī)模型

比較器模型如圖8所示。比較器收到主機(jī)的啟動(dòng)信號(hào)后啟動(dòng)，進(jìn)入start狀態(tài)，判斷主機(jī)的工作狀況。若a1，a2主機(jī)未正常工作或未收到完成信號(hào)senda1、senda2，轉(zhuǎn)入cannot_comp狀態(tài)，比較器不進(jìn)行比較，向切換器模型發(fā)送故障信號(hào)fault1。若比較器收到主機(jī)完成信號(hào)senda1，senda2，此時(shí)轉(zhuǎn)入judgeA狀態(tài)，比較器進(jìn)行對(duì)a系數(shù)據(jù)的比較，當(dāng)比較相等時(shí)，轉(zhuǎn)入same狀態(tài)，向切換器發(fā)送相等信號(hào)；當(dāng)比較不相等時(shí)，轉(zhuǎn)入diff狀態(tài)，向切換器發(fā)送不相等信號(hào)。比較器向切換器發(fā)送完信號(hào)后，轉(zhuǎn)入reset狀態(tài)，等候系統(tǒng)運(yùn)行模型發(fā)送重置信號(hào)，重置相關(guān)變量。

圖8　比較器模型

切換器模型如圖9所示。切換器收到比較器的啟動(dòng)信號(hào)后啟動(dòng)，進(jìn)入start狀態(tài)，判斷故障信號(hào)和數(shù)據(jù)比較信號(hào)。

圖9　切換器模型

若未收到2個(gè)比較器的故障信號(hào)，切換器轉(zhuǎn)入judgesame1狀態(tài)，判斷比較器1的數(shù)據(jù)比較結(jié)果。若相同，轉(zhuǎn)入judgesame2_1狀態(tài)。判斷比較器2的數(shù)據(jù)比較結(jié)果，若相同則轉(zhuǎn)入state1狀態(tài)，否則轉(zhuǎn)入state2狀態(tài)，向系統(tǒng)運(yùn)行模型發(fā)送OUT1信號(hào)，表示a系輸出。若比較器1的數(shù)據(jù)比較結(jié)果不同，轉(zhuǎn)入judgesame2_2狀態(tài)，判斷比較器2的數(shù)據(jù)比較結(jié)果，若相同則轉(zhuǎn)入state5狀態(tài)，向系統(tǒng)運(yùn)行模型發(fā)送OUT2信號(hào)表示b系輸出，否則轉(zhuǎn)入state6狀態(tài)，向系統(tǒng)運(yùn)行模型發(fā)送fault信號(hào)，表示故障輸出。

若收到了2個(gè)比較器中的一個(gè)故障信號(hào)，轉(zhuǎn)入comp1sendfault或comp2sendfault狀態(tài)，再判斷另一個(gè)比較器是否故障，若故障，轉(zhuǎn)入state6狀態(tài)，故障輸出。若另一個(gè)比較器未故障，轉(zhuǎn)入state2或state4狀態(tài)，分別向系統(tǒng)運(yùn)行模型發(fā)送OUT1和OUT2信號(hào)，表明a系輸出或b系輸出。

向系統(tǒng)運(yùn)行模型發(fā)送信號(hào)后，切換器轉(zhuǎn)入到reset狀態(tài)，等待系統(tǒng)運(yùn)行模型發(fā)送重置信號(hào)，重置相關(guān)變量。

系統(tǒng)運(yùn)行模型如圖10所示。其主要功能是對(duì)其余模型的初始化和重置。系統(tǒng)運(yùn)行模型收到切換器的輸出信號(hào)后，向各個(gè)模型發(fā)送重置信號(hào)，各個(gè)模型重置后會(huì)自動(dòng)進(jìn)行新一輪的工作。

圖10　系統(tǒng)運(yùn)行模型

2.3　模型驗(yàn)證

使用UPPAAL的BNF語法[8]將二乘二取二冗余結(jié)構(gòu)的性質(zhì)公式化，用驗(yàn)證器對(duì)其性質(zhì)進(jìn)行自動(dòng)驗(yàn)證。二乘二取二冗余邏輯需求如下。

(1)系統(tǒng)未死鎖：A[]not deadlock

(2)二取二比較過程邏輯驗(yàn)證：由于主機(jī)數(shù)據(jù)傳送異常，比較器從初始狀態(tài)轉(zhuǎn)移到不能比較狀態(tài)：E<>((comp1.idle imply comp1.cannot_comp) and (a1.idle imply a1.a1port_unual))

(3)二乘二比較過程邏輯驗(yàn)證：比較器可從初始狀態(tài)轉(zhuǎn)移到比較結(jié)果狀態(tài)：E<> ((comp1.idle imply comp1.same) or (comp1.idle imply comp1.diff))

(4)二乘二切換過程邏輯驗(yàn)證：切換器可從初始狀態(tài)轉(zhuǎn)移到上述的各個(gè)結(jié)果狀態(tài)，并進(jìn)行輸出切換：E<> ((switch.idle imply switch.state5)or(switch.idle imply switch.state6) or (switch.idle imply switch.state1) or (switch.idle imply switch.state2)or(switch.idle imply switch.state3) or (switch.idle imply switch.state4))

(5)a1等待超過運(yùn)行周期則與a2通信不成功：A[]a1.a1com_failed imply a1.t1 >=100

上述的模型驗(yàn)證結(jié)果如圖11所示，由此得出所建立的模型滿足二乘二取二冗余結(jié)構(gòu)的性質(zhì)。

圖11　模型驗(yàn)證結(jié)果

3　二乘二取二邏輯仿真

基于建模思路，在Windows平臺(tái)應(yīng)用程序的集成開發(fā)環(huán)境Visual Studio 2012下，采用C++開發(fā)實(shí)現(xiàn)。

仿真程序按照系統(tǒng)運(yùn)行模型所指定的各種運(yùn)行狀態(tài)進(jìn)行仿真，包括a、b系均正常工作或b系故障，a系輸出；a系故障，b系輸出；a、b系均故障，故障輸出等運(yùn)行狀況。

下面以a系比較器數(shù)據(jù)輸入不相等，b系比較器數(shù)據(jù)輸入相等且工作正常為例進(jìn)行說明。

對(duì)上述情況進(jìn)行仿真，a系主機(jī)計(jì)算結(jié)果輸出不相等，此時(shí)比較器comp1工作狀態(tài)如圖12所示；b系主機(jī)計(jì)算結(jié)果輸出相等，此時(shí)比較器comp2工作狀態(tài)如圖13所示。

圖12　a系主機(jī)及比較器comp1結(jié)果

圖13　b系主機(jī)及比較器comp2結(jié)果

圖14　切換器switch1結(jié)果

根據(jù)上述工作原理可知，此時(shí)b系輸出，切換器switch1工作狀態(tài)如圖14所示。

由上述結(jié)果，程序仿真驗(yàn)證了二乘二取二冗余結(jié)構(gòu)的工作原理和過程。

4　結(jié)論

二乘二取二冗余結(jié)構(gòu)已經(jīng)成功應(yīng)用于我國(guó)鐵路信號(hào)及其他安全關(guān)鍵領(lǐng)域。本文提出了一種基于UPPAAL的二乘二取二安全冗余邏輯的建模和驗(yàn)證方法。并基于驗(yàn)證后的二乘二取二安全模型，仿真實(shí)現(xiàn)了二乘二取二的安全冗余邏輯，驗(yàn)證了二乘二取二冗余邏輯的安全性和可靠性。

參考文獻(xiàn)：

[1]許崇.二乘二取二系統(tǒng)的可靠性和安全性[D].合肥：合肥工業(yè)大學(xué)，2013

[2]高宏.基于通用計(jì)算機(jī)的二取二安全計(jì)算平臺(tái)的研究[D].北京：北京交通大學(xué)，2009.

[3]楊揚(yáng).車站信號(hào)控制系統(tǒng)[M].成都：西南交通大學(xué)出版社，2012.

[4]李翔.二乘二取二冗余機(jī)制研究[D].成都：西南交通大學(xué)，2012.

[5]蔡煊，王長(zhǎng)林.車載列車自動(dòng)防護(hù)的二乘二取二安全計(jì)算機(jī)平臺(tái)同步機(jī)制[J].計(jì)算機(jī)工程，2015(8):301-305.

[6]熊振華，魏臻.基于UPPAAL的鐵路車站信號(hào)聯(lián)鎖系統(tǒng)模型驗(yàn)證[J].科學(xué)技術(shù)與工程，2008(7):1843-1844

[7]郭華，莊雷，張習(xí)勇.UPPAAL—一種適合自動(dòng)驗(yàn)證實(shí)時(shí)系統(tǒng)的工具[J].微計(jì)算機(jī)信息，2006，22(15)：52-54.

[8]呂繼東，唐濤，燕飛，等.基于UPPAAL的城市軌道交通CBTC區(qū)域控制子系統(tǒng)建模與驗(yàn)證[J].鐵道學(xué)報(bào)，2009，31(3)：59-64.

[9]郭進(jìn)，張亞東.中國(guó)高速鐵路信號(hào)系統(tǒng)分析與思考[J].北京交通大學(xué)學(xué)報(bào)，2012(5):90-94.

[10] 張亞東.高速鐵路列車運(yùn)行控制系統(tǒng)安全風(fēng)險(xiǎn)辨識(shí)及分析研究[D].成都：西南交通大學(xué)，2013.

[11] 劉霄，張亞東，郭進(jìn).CTCS3級(jí)列控車載協(xié)同仿真子系統(tǒng)的研究與實(shí)現(xiàn)[J].鐵道標(biāo)準(zhǔn)設(shè)計(jì)，2013(11):113-116，130.

[12] 胡雪蓮，陶彩霞.基于MSC與UPPAAL的列控系統(tǒng)等級(jí)轉(zhuǎn)換場(chǎng)景形式化驗(yàn)證[J].鐵道標(biāo)準(zhǔn)設(shè)計(jì)，2015(2)：122-127.

[13] 賀歡歡，陳永剛，羅雅允，等.移動(dòng)授權(quán)的形式化建模與驗(yàn)證[J].鐵道標(biāo)準(zhǔn)設(shè)計(jì)，2015(3)：118-121.

[14] 周翔，武曉春.基于MSC與UPPAAL的高鐵跨界臨時(shí)限速建模與驗(yàn)證[J].鐵道標(biāo)準(zhǔn)設(shè)計(jì)，2016(10)：126-131.

[15] 謝林，楊揚(yáng).基于模型的進(jìn)路建立過程測(cè)試用例自動(dòng)生成[J].鐵道標(biāo)準(zhǔn)設(shè)計(jì)，2017(2)：109-116.

[16] 安越，李國(guó)寧.基于Timed-UML順序圖的RBC交接形式化建模與分析[J].鐵道標(biāo)準(zhǔn)設(shè)計(jì)，2016(6)：132-138.