基于UPPAAL的二乘二取二邏輯建模與仿真

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

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

在核電、航空航天和鐵路等安全關鍵領域中，為降低因硬件設備故障或軟件失效帶來的系統安全風險，通常采用冗余技術來保證關鍵設備的可靠性和安全性。冗余，是指重復配置系統的一些組成部件或設備，當系統部件發生故障時，冗余配置的部件介入并承擔故障部件的工作，由此減少系統的故障時間。系統設備冗余結構主要有雙機熱備冗余、三取二冗余和二乘二取二冗余等。

二乘二取二冗余系統目前在計算機聯鎖、列車運行控制系統等鐵路信號領域中廣泛使用[1]，其系統結構包括4臺主機、2個比較器和1個切換器。其基本思想是雙系熱備，即該系統有2個熱備的子系統。系內采用二取二制式，每一系分別有兩臺具有故障檢測功能的主機和一個進行數據比較的比較器[2]。該技術結合了雙機熱備技術和二取二技術的特點，既具有熱備系統的高可靠性，又具備二取二的高安全性。

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

1　二乘二取二系統分析

1.1　二乘二取二系統結構和工作原理

對文獻[3]中提及的車載ATP系統，該系統是由2套二取二子系統組成的a，b雙系熱備系統，2套熱備系統之間通過切換器進行輸出切換。對其二乘二取二邏輯功能進行簡化，得到簡化后的結構如圖1所示。

圖1　二乘二取二系統結構

系統工作時，a、b系4臺主機同時接收數據，并監督數據輸入工作狀態，如圖1第①步所示。若數據輸入正常，主機對接收的數據進行校驗，并相互通信，如圖1第②步所示。當校驗相等時，主機將數據傳送到比較器中進行比較；若數據輸入錯誤或通信中斷，主機向比較器報告故障信號，如圖1第③步所示。若比較器未收到故障信號，比較器對主機傳送的數據進行數據比較，并將比較結果送到切換器；若比較器收到故障信號，此時比較器不進行數據比較，并向切換器報告故障信號，如圖1第④步所示。切換器根據比較器送來的比較結果或故障信號，判定哪一系輸出[4]，如圖1第⑤步所示。若a、b兩系都正常工作，則系統默認a系作為主系輸出。主系每個周期的結果數據及中間數據均傳給備系的2個主機，如圖1第⑥步所示。

對系統二乘二取二工作流程簡化，流程如圖2所示。

圖2　系統工作流程

1.2　二乘二取二關鍵邏輯分析

1.2.1系統工作狀態分析

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

表1　二乘二取二系統工作狀態

根據表1，建立對應的系統狀態轉移圖，如圖3所示。

圖3　系統狀態轉移

1.2.2比較邏輯分析

比較器的二取二比較邏輯和切換器的二乘二切換邏輯是二乘二取二系統邏輯的核心組成部分。當a1，a2機的數據輸入錯誤或兩主機通信中斷時，會向比較器a報告故障信號。比較器a收到這個故障信號后，會向切換器發送a系故障信號。若系內兩主機工作正常，此時比較器a將判斷發送的數據是否相等。當兩主機的數據相等時，比較器a向切換器發送相等信號，反之則發送不等信號。通過工作流程分析，得到系統比較邏輯如圖4所示。

圖4　二取二比較邏輯

1.2.3切換邏輯分析

切換器的切換依據是兩系的比較器發來的比較結果或故障信號。首先判斷兩系是否報告故障信號，如果兩系均有故障信號或其中一系故障而另一系數據比較不相等，或兩系數據比較都不相等，切換器判定為故障輸出。其次切換器未收到故障信號時，判斷系內數據比較是否相等。若切換器收到a系數據比較相等結果，則判定a系輸出；若切換器未收到a系數據比較相等結果而收到b系數據比較相等結果，則判定b系輸出。通過分析，得到系統切換邏輯如圖5所示。

圖5　二乘二切換邏輯

2　二乘二取二邏輯建模及驗證

2.1　建模原理

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

2.2　模型建立

根據上述分析，對系統邏輯進行建模。可以建立包括切換器、比較器模型等在內的7個模型，還有一個系統運行模型來控制整個系統。

各模型之間的具體聯系如圖6所示。

圖6　模型關系結構

其中a1、a2、b1、b2為主機模型，comp1和comp2為比較器模型，switch為切換器模型，contr為系統運行模型。

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

表2　變量含義

表3　信道含義

根據上述的關鍵邏輯分析，比較器收到主機的各類工作狀態信號，會向切換器發送不同的結果信號。建立的比較器模型先判斷是否存在故障信號，若存在則進入不比較狀態，不存在則進入比較狀態。最后分別將結果發送給切換器模型。同理，切換器模型判斷各種比較器發來的結果信號，經過邏輯運算后，判定哪一系作為輸出。

主機模型如圖7所示。主機啟動后，若主機未正常工作，向比較器發送a1fault信號。若主機正常工作，進行數據計算，計算完成后向另一主機發送A1result信號，收到對方發來的信號后向比較器發送一個完成信號senda1。若未收到，主機等待直到運行周期結束，向比較器發送通信中斷信號。切換器切換輸出后，主機判斷輸出結果。若a系輸出，即a系為主系，則向b系發送數據，以便下一周期主備系切換后繼續進行計算。若b系輸出，則清零并等待b系發送結果數據。

圖7　主機模型

比較器模型如圖8所示。比較器收到主機的啟動信號后啟動，進入start狀態，判斷主機的工作狀況。若a1，a2主機未正常工作或未收到完成信號senda1、senda2，轉入cannot_comp狀態，比較器不進行比較，向切換器模型發送故障信號fault1。若比較器收到主機完成信號senda1，senda2，此時轉入judgeA狀態，比較器進行對a系數據的比較，當比較相等時，轉入same狀態，向切換器發送相等信號；當比較不相等時，轉入diff狀態，向切換器發送不相等信號。比較器向切換器發送完信號后，轉入reset狀態，等候系統運行模型發送重置信號，重置相關變量。

圖8　比較器模型

切換器模型如圖9所示。切換器收到比較器的啟動信號后啟動，進入start狀態，判斷故障信號和數據比較信號。

圖9　切換器模型

若未收到2個比較器的故障信號，切換器轉入judgesame1狀態，判斷比較器1的數據比較結果。若相同，轉入judgesame2_1狀態。判斷比較器2的數據比較結果，若相同則轉入state1狀態，否則轉入state2狀態，向系統運行模型發送OUT1信號，表示a系輸出。若比較器1的數據比較結果不同，轉入judgesame2_2狀態，判斷比較器2的數據比較結果，若相同則轉入state5狀態，向系統運行模型發送OUT2信號表示b系輸出，否則轉入state6狀態，向系統運行模型發送fault信號，表示故障輸出。

若收到了2個比較器中的一個故障信號，轉入comp1sendfault或comp2sendfault狀態，再判斷另一個比較器是否故障，若故障，轉入state6狀態，故障輸出。若另一個比較器未故障，轉入state2或state4狀態，分別向系統運行模型發送OUT1和OUT2信號，表明a系輸出或b系輸出。

向系統運行模型發送信號后，切換器轉入到reset狀態，等待系統運行模型發送重置信號，重置相關變量。

系統運行模型如圖10所示。其主要功能是對其余模型的初始化和重置。系統運行模型收到切換器的輸出信號后，向各個模型發送重置信號，各個模型重置后會自動進行新一輪的工作。

圖10　系統運行模型

2.3　模型驗證

使用UPPAAL的BNF語法[8]將二乘二取二冗余結構的性質公式化，用驗證器對其性質進行自動驗證。二乘二取二冗余邏輯需求如下。

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

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

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

(4)二乘二切換過程邏輯驗證：切換器可從初始狀態轉移到上述的各個結果狀態，并進行輸出切換：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等待超過運行周期則與a2通信不成功：A[]a1.a1com_failed imply a1.t1 >=100

上述的模型驗證結果如圖11所示，由此得出所建立的模型滿足二乘二取二冗余結構的性質。

圖11　模型驗證結果

3　二乘二取二邏輯仿真

基于建模思路，在Windows平臺應用程序的集成開發環境Visual Studio 2012下，采用C++開發實現。

仿真程序按照系統運行模型所指定的各種運行狀態進行仿真，包括a、b系均正常工作或b系故障，a系輸出；a系故障，b系輸出；a、b系均故障，故障輸出等運行狀況。

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

對上述情況進行仿真，a系主機計算結果輸出不相等，此時比較器comp1工作狀態如圖12所示；b系主機計算結果輸出相等，此時比較器comp2工作狀態如圖13所示。

圖12　a系主機及比較器comp1結果

圖13　b系主機及比較器comp2結果

圖14　切換器switch1結果

根據上述工作原理可知，此時b系輸出，切換器switch1工作狀態如圖14所示。

由上述結果，程序仿真驗證了二乘二取二冗余結構的工作原理和過程。

4　結論

二乘二取二冗余結構已經成功應用于我國鐵路信號及其他安全關鍵領域。本文提出了一種基于UPPAAL的二乘二取二安全冗余邏輯的建模和驗證方法。并基于驗證后的二乘二取二安全模型，仿真實現了二乘二取二的安全冗余邏輯，驗證了二乘二取二冗余邏輯的安全性和可靠性。

參考文獻：

[1]許崇.二乘二取二系統的可靠性和安全性[D].合肥：合肥工業大學，2013

[2]高宏.基于通用計算機的二取二安全計算平臺的研究[D].北京：北京交通大學，2009.

[3]楊揚.車站信號控制系統[M].成都：西南交通大學出版社，2012.

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

[5]蔡煊，王長林.車載列車自動防護的二乘二取二安全計算機平臺同步機制[J].計算機工程，2015(8):301-305.

[6]熊振華，魏臻.基于UPPAAL的鐵路車站信號聯鎖系統模型驗證[J].科學技術與工程，2008(7):1843-1844

[7]郭華，莊雷，張習勇.UPPAAL—一種適合自動驗證實時系統的工具[J].微計算機信息，2006，22(15)：52-54.

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

[9]郭進，張亞東.中國高速鐵路信號系統分析與思考[J].北京交通大學學報，2012(5):90-94.

[10] 張亞東.高速鐵路列車運行控制系統安全風險辨識及分析研究[D].成都：西南交通大學，2013.

[11] 劉霄，張亞東，郭進.CTCS3級列控車載協同仿真子系統的研究與實現[J].鐵道標準設計，2013(11):113-116，130.

[12] 胡雪蓮，陶彩霞.基于MSC與UPPAAL的列控系統等級轉換場景形式化驗證[J].鐵道標準設計，2015(2)：122-127.

[13] 賀歡歡，陳永剛，羅雅允，等.移動授權的形式化建模與驗證[J].鐵道標準設計，2015(3)：118-121.

[14] 周翔，武曉春.基于MSC與UPPAAL的高鐵跨界臨時限速建模與驗證[J].鐵道標準設計，2016(10)：126-131.

[15] 謝林，楊揚.基于模型的進路建立過程測試用例自動生成[J].鐵道標準設計，2017(2)：109-116.

[16] 安越，李國寧.基于Timed-UML順序圖的RBC交接形式化建模與分析[J].鐵道標準設計，2016(6)：132-138.