三模冗余箭機系統的設計及形式化分析

摘要：針對航天系統的具體需求，本文首先設計了三模冗余箭載計算機系統。接著通過形式化方法對三模冗余箭機系統協議進行分析，采用UPPAAL模型工具建立了CPU時間自動機、表決時間自動機、仲裁時間自動機及脈沖發生單元時間自動機。最后對模型進行仿真及相關性質的驗證。經過驗證，提取了兩個重要的參數取值約束關系。該約束關系對于系統的設計具有一定的啟發性，同時也保障了系統的安全性及可靠性。

關鍵詞：三模表決算法；形式化方法；時間自動機；系統驗證

中圖分類號： TP391.9文獻標識碼：A文章編號：1009-3044(2008)32-1257-03

Design and Formal Analysis of a Triple-Modular Redundant Rocket Computer System

ZHANG Hai-bin

(School of Electronic and Information，Tongji University，ShangHai 201804，China)

Abstract: According to the domain requirements in rocket aerospace field， give a design of a Triple-Modular Redundant System. Then process a formal analysis of the system to check its correctness by using the model checking tool-UPPAAL. Model the system as a network of automata that comprises four timed automata: CPU， voter， arbitrator and impulse generator. Based on the model， give the verification and obtain two important parameter constraints， which ensure the dependability of the system.

Key words: triple-modular redundant algorithm; formal method; time automata; system verification

1 引言

隨著科技進步和人類社會的發展，航天技術水平日益成為一個國家綜合國力的重要標志。運載火箭是迄今為止人類進入空間發展航天事業的最主要手段。現代的運載火箭正朝著多樣化、復雜化的方向發展，其造價高昂，一旦發生事故，將會造成重大的財產損失和人員傷亡，因此迫切需要提高運載工具的可靠性和安全性，而增強核心設備——箭載計算機的可靠性、智能化和先進性將為滿足下一代運載火箭的多樣性和安全性打下堅實的基礎 。

傳統的箭載計算機沒有考慮冗余設計，存在單點故障失效模式，從目前的器件等級和工藝水平考慮，如果不從系統的框架上采取措施，進一步提高可靠性是很困難的。為此，本文設計了三模冗余箭載計算機系統，詳細描述了CPU運算處理單元、表決器單元、表決仲裁單元及同步脈沖發生單元的協議規范。

在系統可靠性的驗證上，傳統檢驗方法如仿真、測試等難以檢測系統的全面狀態，而形式化方法具有全狀態空間搜索的優越性，在解決復雜系統的抽象分析與驗證方面問題時具有不可替代的作用 。因此為了檢測三模冗余箭機系統的可靠性，文中將采用形式化方法進行分析，使用UPPAAL模型檢驗工具 對CPU運算處理單元、表決單元和表決仲裁單元進行建模、仿真及驗證，進而得到有效的驗證結果。

2 三模冗余箭機系統

如圖1所示，所設計三模冗余箭機系統的核心部分包括同步脈沖發生單元、CPU運算處理單元、表決單元和表決仲裁單元。

2.1 同步脈沖發生單元

同步脈沖發生單元負責依次發送CPU同步工作脈沖，表決器同步工作脈沖和仲裁器工作脈沖，以觸發系統各部件按序協同工作。

一個系統周期為1ms，在系統初次上電并完成初始化后，脈沖發生單元首先發送CPU同步工作脈沖，觸發CPU單元進入工作過程。經過0.5ms后，脈沖發生單元發送表決器同步工作脈沖，觸發表決器單元工作。再經過0.4ms后，脈沖發生單元發送仲裁器工作脈沖，觸發仲裁器進入工作狀態。

2.2 CPU處理單元

CPU處理單元包含三套規格相同的CPU，每套CPU上安裝不同版本的操作系統。當CPU同步脈沖上升沿到來時，CPU進入中斷服務程序，進行數據采集和運算處理。CPU在運算處理完畢后，將運算結果寫入FIFO緩存。CPU運算處理的時間上限為0.5ms，如果某路CPU在0.5ms內沒有運算完畢，相應通道上的FIFO緩存單元在該CPU工作周期結束時就為空。造成FIFO緩存為空的原因，可能是CPU運算超時或者CPU出現故障。

每個CPU部件都集成了一個看門狗單元。看門狗單元包含一個計數器，計數器在初次上電后從0開始自動累加。CPU在正常工作過程中，會在很短的時間間隔內定期向看門狗發送喂狗信號。看門狗一旦接收到喂狗信號，就將計數器置為一個特定值。如果在一定的時間間隔內CPU沒有正常發送喂狗信號，看門狗計數器就會不斷累加到上限并溢出。計數器溢出將觸發看門狗對CPU進行復位，同時計數器也被清0。

2.3 表決單元

表決單元包含了兩套規格相同的表決器。當表決同步脈沖上升沿到來時，兩套表決器同時進入工作狀態。表決器首先讀FIFO緩存上的運算結果，依照表決算法進行表決操作。同時表決器需要統計某路FIFO緩存上運算結果連續錯誤的次數，當該連續錯誤次數達到某個上限值，表決器就判斷相應通道上的CPU出現故障，并向仲裁器報告。

2.3.1 表決算法

表決器讀FIFO緩存的數據，首先進行超時檢測及通訊校驗，再根據有效數據的個數，進入到如下的表決模式。

1) 三模表決：將三個CPU的運算結果進行比較，去除最大值和最小值，選擇中間值作為表決輸出。當存在兩個或者三個CPU的運算結果一致時，選取序號靠前的CPU的運算結果作為表決輸出。

2) 兩模表決：選取序號靠前的CPU，將其運算結果作為表決輸出。

3) 單模表決：選取處于正常工作狀態的CPU，將其運算結果作為表決輸出。

2.3.2 表決器對CPU運算結果連續錯誤次數的統計

表決器在工作過程中，需要統計CPU運算結果連續錯誤的次數。

當CPU處于工作狀態時，表決器一旦連續檢測到 ( )幀錯誤數據，就判斷該CPU出現故障并向仲裁器報告。當CPU處于重啟過程時，表決器一旦連續檢測到 ( )幀錯誤數據，就判斷該CPU出現故障并報告給仲裁器。

2.4 仲裁單元

仲裁單元包含了一個仲裁器。當仲裁器工作脈沖上升沿到來時，仲裁器根據主、次表決器的狀態，選取主表決器的表決結果輸出。同時，若主表決器報告某路CPU出現故障，仲裁器需要發送復位信號重啟故障CPU。

3 三模冗余箭機系統建模

本章主要采用時間有限狀態機的形式化描述方法。時間有限狀態機是一種用來進行對象行為建模的工具，其作用主要是描述對象在它的生命周期內所經歷的狀態序列，以及如何響應來自外界的各種事件。

系統建模采用UPPAAL模型驗證工具。如圖2至圖5所示，分別建立了CPU時間自動機模型，表決器時間自動機模型，仲裁器時間自動機模型以及同步脈沖發生單元時間自動機模型。

以下對CPU時間自動機做簡要的描述：

每個時間自動機都是由狀態(Location)及遷移(Edge)組成。圖2中CPU時間自動機包含了重啟(Restart)、空閑(Idle)及工作(Processing)三個狀態。從一個狀態到另一個狀態的邊就稱為遷移：

1) 遷移E1表示CPU完成啟動，進入空閑狀態，準備工作。

2) 遷移E2表示CPU接收到仲裁器的復位信號，進入重啟過程。

3) 遷移E3表示看門狗計數器達到上限，并對CPU復位。

4) 遷移E4表示CPU的運算處理過程，若運算結果為0，則表示CPU運算出錯。

5) 遷移E5表示CPU在某次同步工作脈沖到來時，不做操作。該情況可能是因為CPU運算超時或進入了死循環而無法正常退出。

6) 遷移E6表示了CPU的一次喂狗操作，看門狗計數器被置特定值。

7) 遷移E7表示了CPU在重啟狀態，被再次復位。

由于篇幅限制，其他的時間自動機不做描述。

4 三模冗余箭機模型驗證

針對上述模型，采用CTL邏輯描述系統特性，進行了相關性質的驗證，主要包括死鎖驗證、數據流驗證及參數取值約束相關的驗證。驗證過程不一一贅述，驗證結果表明，系統不存在死鎖，系統交互及數據流通正確。以下主要介紹兩個重要的參數取值約束的驗證過程。

4.1 參數描述

建模過程中，引入了如下參數：

“const int T = 10; //系統周期為1ms

const int cpu_period = 5， voter_period = 4， arbitrator_period = 1;

//分別表示CPU運算處理上限、表決操作上限及仲裁器處理上限

const int restart_ub = 200， restart_lb=100; //分別表示CPU重啟上限與重啟下限

const int counter_ub = 300;//看門狗計數器上限

const int reset_counter = 200; //看門狗接收到喂狗信號，計數器被置特定值

const int errorcount1= 11; //CPU工作狀態下，允許運算結果連續錯誤的最大次數

const int errorcount2 = 21; //CPU重啟狀態下，允許運算結果連續錯誤的最大次數”。

由于UPPAAL工具無法表示小數，所以需要將所有的參數擴大若干倍后表示為整數。如CPU運算處理上限為0.5ms，在模型中擴大10倍取值為5。

4.2 errorcount1取值約束

系統設計過程中，看門狗與CPU集成在一個部件上，看門狗對CPU的復位操作更直接更高效。因此當CPU出現故障時，看門狗應盡可能優先對CPU進行復位。仲裁器則主要處理看門狗無法發現的CPU故障。如CPU進入死循環狀態時，仍可以正常發送喂狗信號，卻無法進行正常的運算處理，該情況下，需要由表決器統計CPU運算連續錯誤的次數，并報告仲裁器重啟該CPU。

驗證過程主要就如下兩條用CTL寫出的規范進行比較：

1）E<> arbitrator.Check voters(0).cpu_status_by_voter[0]==0

cpus(0).counter==counter_ub arbitrator.reset_flag_by_arbi[0] !=1

性質①驗證CPU處于工作狀態下，看門狗計數器達到上限并對CPU復位，此時仲裁器并未檢測到CPU的故障。

2）E<> arbitrator.Check voters(0).cpu_status_by_voter[0]==0

cpus(0).counter!=counter_ub arbitrator.reset_flag_by_arbi[0] ==1

性質2）驗證CPU處于工作狀態下，仲裁器對CPU復位，此時看門狗計數器未達到上限。

表1列出了幾組counter_ub、reset_counter及errorcount1的不同取值所得的驗證結果。

如表1中所示，當errorcount<=[(counter_ub-reset_counter)/T]時，性質1）總不滿足，也即看門狗的功能就部分喪失：當CPU在工作狀態出現故障時，總是由仲裁器對CPU復位，看門狗不起作用。而當errorcount1>[(counter_ub-reset_counter)/T]時，看門狗可以對故障CPU進行復位。性質2）對于errorcount1的各種取值總是滿足的，也即當CPU出現故障時，仲裁器總有機會發送復位信號對CPU復位。

對上述參數取其他值進行驗證，驗證結果與表1一致。因此，系統參數errorcount1的取值在滿足errorcount>[(counter_ub-reset_counter)/T]時，可以盡可能優先讓看門狗對出現故障的CPU復位，同時也使得看門狗和仲裁器能夠互為補充，保障了系統的可靠性。

4.3 errorcount2取值約束

當CPU出現故障被復位時，我們希望在達到復位上限前，CPU不會被再次重啟。

需要在UPPAAL中驗證如下性質：

3）E<>cpus(0).Restart cpus(0).counter >restart_lb cpus(0).counter

(arbitrator.reset_flag_by_arbi[0] ==1 || cpus(0).counter == counter_ub )

性質3）驗證CPU在進入重啟狀態，時間超過重啟下限但仍未達到重啟上限時，CPU被再次復位。

表2列出了幾組restart_ub及errorcount2的不同取值所得的驗證結果。

表1 errorcount1取值對性質①②的驗證結果表2 errorcount2取值對性質③的驗證結果

如表2中所示，當errorcount2<=[(restart_ub)/T]時，性質3）總是滿足，CPU可能在未達到復位上限時被再次復位。當errorcount2>[(restart_ub)/T]時，性質3）就不滿足。

對上述參數取其他值進行驗證，驗證結果與表2一致。因此，系統參數errorcount2的取值在滿足errorcount2>[(restart_ub)/T]時，可以避免CPU在進入重啟過程，且未達到復位上限時被再次復位。

5 結論

本文采用形式化的方法設計和分析了三模冗余箭載計算機系統協議，采用UPPAAL模型工具對系統進行建模、仿真以及相關性質的驗證。驗證表明，三模冗余箭機系統具有比較高的可靠性和冗余性。在驗證過程中發現了一些隱蔽問題，為實際的硬件設計提供了理論依據。

形式化方法作為一種以數學為基礎的方法，能夠清晰、精確、抽象、簡明地規范和驗證軟件系統及其性質，能夠極大地提高軟件的安全性和可靠性，因而被廣泛采用，并具有不可替代的作用。形式化方法在航天領域不僅可用于箭載系統中，也可應用于星載、彈載系統中。對于系統關鍵部件在早期方案設計階段的形式化研究，其效果最為明顯，既節省許多研制經費，同時增加寶貴的整星、彈載系統考核時間，提高系統可靠性并縮短研制周期。

參考文獻：

[1] 龍樂豪.中國航天運輸系統的現狀與展望[J]. 中國航天2004(8):12-13.

[2] 韓鴻碩，蔣宇平，林蔚然，等.2005年世界航天發展述評[J].中國航天，2006(3):68-69.

[3] 魏懷鑒，鮑皖蘇.形式化方法和測試技術及其在安全中的應用[J]. 微計算機信息，2006，22(11):60-63.

[4] Larsen K，Pettersson P，Wang Y.Model-Checking for Real-Time Systems[J]. In Proc.of Fundamentals of Computation Theory，1995.

[5] Bengtsson J，Larsen K，Larsson F.et al.UPPAAL-a Tool Suite for AutomaticVerification of Real-Time Systems.Hybrid system， 1995:232-243.

[6] Bengtsson J， Larsson F.Uppaal A Tool for Automatic Verification of Real-time Systems[D].Sweden: Uppsala University， 1996:1-69.