湯雪乾，李 峭，孔韻雯，何 鋒

（北京航空航天大學電子信息工程學院，北京100191）

1 引言

綜合化計算節(jié)點是航天器電子系統(tǒng)的關鍵部件，其可靠性直接關系到航天器能否安全運行并完成預定任務。對于載人的航天器，高安全關鍵等級的設計要求使用冗余配置來增強航天器內計算節(jié)點容忍多種故障模式的能力，其中最具挑戰(zhàn)性的是對于拜占庭故障的容錯。

拜占庭故障（Byzantine Fault）也被稱為“任意故障”，其特點在于故障節(jié)點對其他不同的節(jié)點表現(xiàn)出任意不同的行為［1］。要求載人航天器的分布式電子系統(tǒng)容忍拜占庭故障，即是要求其多個子系統(tǒng)或者部件滿足處理和傳輸信息的一致性檢查要求，消除局部節(jié)點故障時任意行為對于系統(tǒng)的危害。

經典的容忍拜占庭故障方法為口頭消息算法（Oral Messaging，OM）算法［2］，即使用全交換機制在所有的節(jié)點中達成一致性，所有的節(jié)點使用通道化總線（Channelized Bus）的形式互連。通常使用4個故障封閉區(qū)（Fault Containment Region，F(xiàn)CR），2個輪次的數(shù)據(jù)交換，3條獨立的路徑可以容忍1個節(jié)點的拜占庭故障，并使用符號分析實驗室（Symbolic Analysis Laboratory，SAL）進行形式化驗證［3］。肖愛斌等學者對經典的拜占庭模型進行了改進，增加了網(wǎng)絡單元（NE），并對兩輪交換發(fā)送次序進行了優(yōu)化，提出了一種星載計算機拜占庭容錯設計方法［4］，同時也對這種方法進行了可靠性的分析［5］。 高亞楠等學者［6］提出了一種并行通道配合計算節(jié)點交聯(lián)的體系結構，采用1553B和TTP數(shù)據(jù)總線，使用數(shù)據(jù)交換和數(shù)據(jù)比對達到系統(tǒng)故障檢測和故障容錯的要求。另外，還有使用可進化硬件容錯智能方法來控制計算機容錯［7］。這些研究成果為總線式互連的網(wǎng)絡節(jié)點容錯提供了支持。在時間觸發(fā)以太網(wǎng)（Time-Triggered Ethernet，TTE）的研究中，也曾借鑒類似ARINC659（SAFEbus）總線的層次化拜占庭容錯設計，結合自檢對達到一致性［8］，但并不針對交換式鏈路層，屬于應用層協(xié)議擴展。

航天器電子系統(tǒng)隨著復雜程度提升，為了降低航天器平臺的體積、重量和功耗（SWaP），呈現(xiàn)向綜合模塊化航電（Integrated Modular Avionics，IMA）架構發(fā)展的趨勢［9］。IMA架構采用具有多個網(wǎng)段的交換式綜合化互連技術、商用貨架（Commericial Off-the-Shelf，COTS）產品和開放性接口標準，例如：美國NASA蘭利研究中心提出的SPIDER架構、NASA的演進火星運動項目、獵戶座多用途載人飛船（Multi-Purpose Crew Vehicle， MPCV）［10］；其中，SAE AS6802 標準［11］定義的 TTE 網(wǎng)絡作為MPCV飛船綜合化網(wǎng)絡互連基礎設施，得以實用，實現(xiàn)計算節(jié)點之間數(shù)據(jù)的分發(fā)和同步［12］。

載人航天器具有極嚴苛的可靠性和容錯能力要求，簡單地堆砌COTS產品無法滿足該要求，必須進行適用性改造。NASA的Loveless和TTTech公司的Fidi等學者［13］提出一套時間觸發(fā)網(wǎng)絡體系結構下的拜占庭容錯實施方案，基于分布式處理器和全交換體制可以容忍一個拜占庭故障。然而，現(xiàn)有研究［12-13］只是對時間觸發(fā)網(wǎng)絡拜占庭容錯方法進行了推理論證，沒有用規(guī)范性的方法進行描述與證明。雖然對OM算法的形式化驗證可供借鑒，但目前尚未發(fā)現(xiàn)其他公開發(fā)表的文獻直接使用形式化工具對該容錯方法的正確性進行驗證。本文在闡明基于TTE互連的航天器拜占庭容錯設計的理論與方法的基礎上，采用符號分析實驗室（SAL）形式化工具［14］，對相應的互連配置和網(wǎng)絡節(jié)點建立形式化分析模型，并進行模型檢查（model checking），為相應容錯方法的協(xié)議正確性和容錯能力提供優(yōu)于推理論證的規(guī)范化驗證。

2 拜占庭容錯

2.1 拜占庭容錯的理論基礎

為了使對抗拜占庭故障的冗余配置更加有效，將系統(tǒng)進行硬件劃分，形成一個個獨立的故障封閉區(qū)域（Fault Containment Region，F(xiàn)CR），依靠設計實現(xiàn)和認證評審使故障的影響和傳播不跨越FCR。這樣，在隨后的容錯方法分析論證中，設每個節(jié)點為一個FCR，即默認“節(jié)點”和“FCR”的稱謂可以互相代替，則理論上容忍f個拜占庭故障必須滿足以下要求［15］：

1）必須具有不少于3f＋1個FCR；

2）節(jié)點間接收消息必須通過不少于2f＋1個獨立路徑；

3）節(jié)點間交換消息必須通過不少于f＋1個輪次；

4）分布式節(jié)點的時鐘同步必須具有一個有界的偏差。

在拜占庭一致性的要求下，所有的非故障節(jié)點必須保證如下的特性［12］：

1）一致性：所有非故障節(jié)點一致同意一個相同的值。

2）有效性：所有非故障節(jié)點都有一個相同的初值，然后所有非故障節(jié)點都一致同意。

3）終止性：所有非故障節(jié)點最終決定一個值。

2.2 經典拜占庭容錯方法

經典的拜占庭容錯方法是執(zhí)行OM算法以保證交互一致性，節(jié)點之間使用全通道數(shù)據(jù)鏈路（Cross-Channel Data Link，CCDL） 形式互連［13］。為了減少成本的開銷和設計的復雜度，引入一種特殊的設備，稱為“級間”（interstage）［15］。 一個級間就是一個FCR，根據(jù)OM算法轉發(fā)消息，但是自身并不要求一致性。級間的目的是提供執(zhí)行拜占庭一致性算法的功能，但不要求所有的參與容錯的FCR都是全功能的處理器［13］，如圖1所示。

圖1 經典拜占庭容錯方法［5］Fig．1 Classical Byzantine fault tolerance method［5］

以節(jié)點讀取傳感器數(shù)據(jù)的過程為例，為達到交互一致性，首先節(jié)點從本地總線接口讀取傳感器的數(shù)據(jù)，這個步驟并不要求一致性。第一輪（R1）節(jié)點1－3發(fā)送自己的初值到其他的計算節(jié)點和級間中；第二輪（R2）節(jié)點1－3和級間發(fā)送第一輪數(shù)據(jù)到其他的計算節(jié)點中。然后節(jié)點1－3對第二輪數(shù)據(jù)執(zhí)行多數(shù)制來校正第一輪的數(shù)據(jù)。非故障計算節(jié)點現(xiàn)在能夠共享相同的交互一致性（Interactive Consistency，IC）向量。最終節(jié)點1－3執(zhí)行一個選擇函數(shù)來選擇最終的值（該選擇函數(shù)為取中位數(shù)或者取平均值）。經典的拜占庭容錯利用的是全連通的獨立信道，在綜合化交換式互連的場景下需要進行改進。

2.3 時間觸發(fā)網(wǎng)絡拜占庭容錯方法

時間觸發(fā)網(wǎng)絡拜占庭容錯方法基于交換式表決架構（如圖2），采用TTE網(wǎng)絡進行數(shù)據(jù)的分發(fā)和同步。每個機載計算節(jié)點執(zhí)行特定的應用層軟件，與網(wǎng)絡控制器相連接；控制器執(zhí)行TTE協(xié)議所要求的服務；主機和控制器作為一個端系統(tǒng)，通過兩個或者三個冗余TTE網(wǎng)絡交換機實現(xiàn)雙向連接［12］；TTE網(wǎng)絡交換機與數(shù)據(jù)輸入設備和輸出設備實現(xiàn)全雙工連接，通過點對點物理鏈路組成全交換（full-exchange）星型拓撲結構［12］。

另外，依據(jù) SAE AS6802 標準［11］：高完整性的配置的節(jié)點（端系統(tǒng)或交換機）含有指令／監(jiān)視對（COM／MON pair），在圖 2 中以標有“C／M”的灰色方框表示；標準完整性的配置的節(jié)點（端系統(tǒng)或交換機）僅含有指令器（COM），在圖2中的白色框表示未配置監(jiān)視器（MON）。以計算節(jié)點讀取傳感器數(shù)據(jù)的過程為例，為達到交互一致性，時間觸發(fā)網(wǎng)絡算法的執(zhí)行步驟如下：

圖2 時間觸發(fā)網(wǎng)絡拜占庭容錯方法［13］Fig．2 Byzantine fault tolerance method of time-triggered network［13］

1）（R1）每個冗余輸入設備傳輸數(shù)據(jù)到交換機1－3。但是這并不保證非故障設備一致，一個故障設備可能任意傳輸數(shù)據(jù)。

2）（R2）交換機1－3發(fā)送每個冗余輸入設備的消息到所有的計算節(jié)點1－3。

3）計算節(jié)點1－3對來自每個冗余網(wǎng)絡通道的消息執(zhí)行多數(shù)制表決。違反協(xié)議的消息將被丟棄。多數(shù)制必須根據(jù)接收消息的數(shù)量確定，不是靜態(tài)的2／3。非故障計算節(jié)點至此共享相同的IC向量。

4）計算節(jié)點1－3執(zhí)行一個選擇函數(shù)來選擇一個最終的值。

3 時間觸發(fā)網(wǎng)絡容錯的SAL建模

3.1 SAL工具

模型檢查是用形式化方法精確地證明一個系統(tǒng)能夠按照預定目標正確工作，是一種廣泛用于軟硬件形式的驗證工具［16］。SRI計算機科學實驗室推出了一種將定理證明和模型檢驗等多種符號分析技術相整合的框架SAL（Symbolic Analysis Laboratory）工具。SAL框架集成了歸納、程序分析、定理證明和模型檢查等工具。SAL框架的關鍵部分就是一種描述轉換系統(tǒng)（transition systems）的語言，以及對這種語言描述的模型的編譯和屬性查找引擎。SAL提供了規(guī)范狀態(tài)機和它們的屬性的表達式，同時提供了模型檢查器及其狀態(tài)機屬性分析工具。

3.2 SAL模型描述

SAL最基本的建模單元是模塊。模塊可以定義狀態(tài)機，并通過輸入變量和輸出變量實現(xiàn)與其他模塊之間的交互；在模塊的內部，則通過狀態(tài)變量來實現(xiàn)轉換關系。模塊可以嵌套，一個模塊可以作為其它模塊的一部分［17］。

使用SAL語言，建立TTE網(wǎng)絡容錯協(xié)議操作的抽象模型，包括：輸入設備模塊（source模塊）、交換機模塊（switch模塊）和計算節(jié)點模塊（compnode模塊）；為了設置故障場景，設置了控制器模塊協(xié)調各個網(wǎng)絡組件抽象的模塊，它使用stage變量控制整個網(wǎng)絡數(shù)據(jù)交互的進程。

控制器通過設置stage變量來控制數(shù)據(jù)交互的進程（第13行）。在初始化階段（第7－10行），設置對輸入設備和交換機為無故障?？刂破髂K的SAL規(guī)則如圖3所示。

圖3 控制器模塊的SAL規(guī)則Fig．3 SAL specification of controller module

設置故障時需要根據(jù)SAL的語法改寫圖3中第9 －10 行，如“sf＝［［j：sources］ none］；”改寫為“sf［1］ ＝arbitrary”，通過不確定賦值（圖 4 第17－18行）產生一個任意故障，source模塊對不同的節(jié)點，發(fā)送不同的數(shù)值。SAL并沒有表示消息遺漏的專用符號，因而此處用“0”代表遺漏故障（圖4第14行）。

網(wǎng)絡中數(shù)據(jù)傳輸?shù)倪^程是：輸入設備向交換機發(fā)送傳感器數(shù)據(jù)，然后交換機把接收到的數(shù)據(jù)轉發(fā)到計算節(jié)點中。如圖4所示，在無故障的情況下，輸入設備將發(fā)送正確的數(shù)據(jù)到交換機模塊中（第10－11行）。在設置了故障場景的情況下，輸入設備模塊可以接收來自控制器模塊的故障設置信息，標識自身是否故障。圖4中的第13－15行定義輸入設備發(fā)生遺漏故障，圖4中的第17－18行定義輸入設備發(fā)生任意故障。

圖4 輸入設備模塊的SAL規(guī)則Fig．4 SAL specification of input device module

如圖5所示，交換機模塊接收來自輸入設備發(fā)送的數(shù)據(jù)，在無故障的情況下，將數(shù)據(jù)正確地轉發(fā)到計算節(jié)點模塊中（第10－11行）。在設置了故障場景的情況下，交換機模塊根據(jù)控制器模塊設置的故障信息，標識自身是否故障。圖5中的第14－15行定義交換機發(fā)生遺漏故障，圖5中的第17－18行定義交換機發(fā)生任意故障。

圖5 交換機SAL模型Fig．5 SAL specification of switch module

計算節(jié)點模塊接收來自交換機模塊轉發(fā)的數(shù)據(jù)，如圖6所示，然后執(zhí)行多數(shù)制的表決（第15－16行調用多數(shù)制表決函數(shù)），各個計算節(jié)點最終的處理結果將達到一致。注意：在驗證不一致遺漏故障時，使用%注釋15－17行代碼，反注釋18－21行代碼。

多數(shù)表決函數(shù)的關鍵代碼如圖7所示，其中以正整數(shù)v抽象地表示計算節(jié)點接收到的數(shù)值，由于“0”已經被用來代表遺漏，v參與表決的取值不包含0，而是從1開始，這種方式也與文獻［12］對于故障假設的建模表達相同。

圖6 計算節(jié)點SAL模型Fig．6 SAL specification of computer node module

圖7 多數(shù)制投票表決算法Fig．7 SAL specification of majority vote algorithm

4 模型檢查與結果分析

模型檢查形式化方法不僅要對被檢查的模型建模，而且還要用形式化的語言描述待驗證的特性。在SAL工具中，關鍵字“THEOREM”所定義是斷言規(guī)則，用以描述模型的屬性［17］。利用SAL引擎，即可搜索檢查相應的斷言是否成立。

為驗證時間觸發(fā)網(wǎng)絡拜占庭容錯方法的正確性和有效性，在SAL建模工具中設置3個輸入設備、3個交換機和3個計算節(jié)點的模型實例，互連結構如圖2所示。SAE AS6802標準支持單失效假設和雙失效假設，并規(guī)定端系統(tǒng)的故障模式為任意故障或不一致遺漏故障，交換機的故障模式為不一致遺漏故障。本文設置6種典型故障場景來驗證觸發(fā)網(wǎng)絡拜占庭容錯方法的正確性，分別是單失效假設下端系統(tǒng)的任意故障（場景1）和不一致遺漏故障（場景2），以及雙失效假設下兩個端系統(tǒng)的不一致遺漏故障（場景3），兩個交換機的不一致遺漏故障（場景4），以及一個端系統(tǒng)和一個交換機的不一致遺漏故障（場景5）。以上5種故障場景根據(jù)SAE AS6802標準中的失效假設來設置，同時增加場景6和場景7來進一步測試時間觸發(fā)網(wǎng)絡拜占庭容錯方法的容錯能力。

在模型檢查之前，需要對定義的SAL規(guī)則進行基本屬性（活性）的檢查，以保證容錯協(xié)議模型不會死鎖。如圖8所示，通過SAL工具對上述建立的形式化模型進行活性（liveness）檢查，檢查結果表明，模型滿足活性的要求。

圖8 活性檢查定理Fig．8 Liveness checking theorem

如圖9所示，通過構造有效性定理和一致性定理對上述建立的形式化模型進行模型檢查。結果表明，形式化模型滿足有效性、一致性和終止性。表1中的故障場景1和7表明時間觸發(fā)網(wǎng)絡拜占庭容錯方法能夠容忍1個拜占庭故障節(jié)點，但無法容忍2個并發(fā)的拜占庭故障節(jié)點。

圖9 模型檢查定理Fig．9 Model-checking theorem

能夠容忍1個拜占庭故障，必然可以容忍1個“不一致遺漏”故障，表1中故障場景6的檢驗結果印證了這一點。更進一步，在高完整性配置下，時間觸發(fā)網(wǎng)絡節(jié)點能夠將拜占庭故障模式轉化為不一致遺漏故障模式，為了針對性地展示TTE網(wǎng)絡在拜占庭容錯的基礎上的擴展容錯能力，將輸入設備和交換機設置為“不一致遺漏”（inconsistent-omit）故障，作為故障場景3－5，然后驗證拜占庭容錯方法的有效性，實驗結果表1所示。由表1可知，時間觸發(fā)網(wǎng)絡拜占庭容錯方法可以容忍1個不一致遺漏故障節(jié)點或者2個不一致遺漏故障交換機節(jié)點，無法同時容忍2個拜占庭故障。由拜占庭容錯理論可知，在目前的架構中，僅僅增加源端或者交換機的數(shù)量而不增加獨立路徑的個數(shù)無法提高架構的容錯能力。

表1 算法特性分析Table 1 Characteristics analysis of the algorithm

值得說明的是拜占庭故障是最嚴苛的，危害程度也最高。TTE網(wǎng)絡通過高完整性配置能夠將拜占庭故障模式降級為不一致遺漏故障模式，減小了拜占庭故障的危害。TTE網(wǎng)絡在目前時間觸發(fā)架構下能夠容忍一個拜占庭故障，同時依靠C／M對配置還可以容忍2個不一致遺漏故障交換機節(jié)點。理論上容忍f個嚴格不一致遺漏故障必須具有不少于f＋1個FCR，節(jié)點間接收消息的路徑必須不少于f＋1個［12］。因此表1結果與形式化檢查結果完全符合，也與理論結果相吻合。

5 結論

通過對時間觸發(fā)網(wǎng)絡拜占庭容錯方法的形式化分析和驗證，可以確信地掌握相應容錯操作的有效性和能力，主要體現(xiàn)于：

1）通過SAL的模型檢查，從理論上證明了時間觸發(fā)網(wǎng)絡拜占庭容錯方法的正確性。

2）時間觸發(fā)網(wǎng)絡拜占庭容錯方法能夠容忍1個拜占庭故障節(jié)點或者2個不一致遺漏故障交換機節(jié)點，不能容忍兩個及以上并發(fā)的拜占庭故障節(jié)點。

TTE網(wǎng)絡通過COM／MON對能夠將危害程度高的拜占庭故障轉化為危害程度較低的不一致遺漏故障，提高了時間觸發(fā)架構的容錯能力，降低了容錯所需獨立路徑的個數(shù)。本文的結果可以為航空航天高安全等級應用的容錯配置提供了更規(guī)范的依據(jù)。

參考文獻（References）

［ 1 ］ Tseng L.Voting in the presence of Byzantine faults［C］ ／／Dependable Computing（PRDC），2017 IEEE 22nd Pacific Rim International Symposium on.IEEE，2017：1-10.

［2］ Zhao W.Byzantine Fault Tolerance［M］.Building Dependable Distributed Systems.John Wiley ＆ Sons， Inc.2014：239-287.

［3］ Rushby J.SAL tutorial： analyzing the fault-tolerant algorithm OM （1）［R］.Computer Science Laboratory， SRI International， Menlo Park， CA， CSL Technical Note， 2004.

［4］ 肖愛斌，楊孟飛，劉波.星載計算節(jié)點拜占庭容錯設計與驗證［J］. 空間控制技術與應用，2008，34（04）：17-22 ＋64.XIAO Aibin， YANG Mengfei， LIU Bo.Design and validation of byzantine fault tolerance for on-board computer［J］.Aerospace Control and Application，2008，34（04）：17-22 ＋ 64.（in Chinese）

［5］ 肖愛斌，胡明明，任憲朝，等.四模冗余拜占庭容錯計算節(jié)點可靠性分析［J］. 空間控制技術與應用，2014，40（03）：41-46.XIAO Aibin， HU Mingming， Ren Xianchao，etal.Reliability analysis of the computer with quad-modularredundancy Byzantine fault tolerant［ J］.Aerospace Control and Application，2014，40（03）：41-46. （in Chinese）

［6］ 高亞楠，賈英民，藺玥.基于數(shù)據(jù)總線的故障容錯體系結構的仿真研究［J］. 計算機仿真， 2014（5）：17-21.GAO Yanan， JIA Yingmin， LIN Yue.Simulation study on data bus based fault-tolerant architecture［J］.Computer Simulation， 2014（5）：17-21. （in Chinese）

［7］ 龔健，楊孟飛.一種衛(wèi)星控制計算節(jié)點智能容錯方法的探討［C］／／全國第十三屆空間及運動體控制技術學術會議論文集，2008：360-365.Gong Jian，Yang Mengfei.Discussion on intelligent fault tolerance method of satellite control computer［C］ ／／Proceedings of the 13th National Symposium on Space and Vehicle Control Technology，.2008：360-365. （in Chinese）

［8］ Driscoll R.K.， Hall B.Schweiker K.Application Agreement and Integration Services ［R］. NASA／CR-2013-217963，NF1676L-15890.2013

［9］ 孔韻雯，李峭，湯雪乾，等.TTE網(wǎng)絡壓縮功能計算開銷的測量方法［J］. 載人航天，2017，23（05）：645-649.KONG Yunwen， LI Qiao， TANG Xueqian， et al.Measuring method for calculation overhead of compression function in TTE network［J］.Manned Spaceflight， 2017， 23（05）：645-649. （in Chinese）.

［10］ Loveless A T.On TTEthernet for integrated fault-tolerant spacecraft networks［C］ ／／AIAA SPACE 2015 Conference and Exposition.2015.

［11］ SAE AS6802 Time-Triggered Ethernet［S］.SAE，2011.11.

［12］ Loveless A， Fidi C， Wernitznigg S.A proposed byzantine fault-tolerant voting architecture using time-triggered ethernet［R］.JSC-CN-40651，Paper＃2017-01-2111，2017.

［13］ Loveless A.Notional 1FT voting architecturewith time-triggered ethernet［R］.JSC-CN-38812， 2016

［14］ Dutertre B，Easwaran A，Hall B，et al.Model-based analysis of Timed-Triggered Ethernet［C］ ／／IEEE／AIAA， Digital Avionics Systems Conference.IEEE， 2012：9D2-1-9D2-11.

［15］ Rushby J.Bus architectures for safety-critical embedded systems［J］.Lecture Notes in Computer Science， 2001， 2211：306-323.

［16］ 何洋，洪玫，祁琳瑩，等.基于模型檢測工具NuSMV的功能測試用例生成方法［J］.計算機應用，2015，35（S2）：155-159.HE Yang， HONG Mei， QI Linying， et al.Appoach of functional test case generation based on model checker NuSMV［J］.Computer Applications，2015，35（S2）：155-159.（in Chinese）

［17］ Moura L D， Owre S， Shankar N.The SAL language manual［EB／OL］. （2003）［2017］.http：／／sal.csl.sri.com／doc／language-report.pdf.