時間觸發(fā)以太網(wǎng)拜占庭容錯方法的形式化驗證

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

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

1 引言

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

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

經(jī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］。肖愛斌等學者對經(jīng)典的拜占庭模型進行了改進，增加了網(wǎng)絡(luò)單元（NE），并對兩輪交換發(fā)送次序進行了優(yōu)化，提出了一種星載計算機拜占庭容錯設(shè)計方法［4］，同時也對這種方法進行了可靠性的分析［5］。 高亞楠等學者［6］提出了一種并行通道配合計算節(jié)點交聯(lián)的體系結(jié)構(gòu)，采用1553B和TTP數(shù)據(jù)總線，使用數(shù)據(jù)交換和數(shù)據(jù)比對達到系統(tǒng)故障檢測和故障容錯的要求。另外，還有使用可進化硬件容錯智能方法來控制計算機容錯［7］。這些研究成果為總線式互連的網(wǎng)絡(luò)節(jié)點容錯提供了支持。在時間觸發(fā)以太網(wǎng)（Time-Triggered Ethernet，TTE）的研究中，也曾借鑒類似ARINC659（SAFEbus）總線的層次化拜占庭容錯設(shè)計，結(jié)合自檢對達到一致性［8］，但并不針對交換式鏈路層，屬于應(yīng)用層協(xié)議擴展。

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

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

2 拜占庭容錯

2.1 拜占庭容錯的理論基礎(chǔ)

為了使對抗拜占庭故障的冗余配置更加有效，將系統(tǒng)進行硬件劃分，形成一個個獨立的故障封閉區(qū)域（Fault Containment Region，F(xiàn)CR），依靠設(shè)計實現(xiàn)和認證評審使故障的影響和傳播不跨越FCR。這樣，在隨后的容錯方法分析論證中，設(shè)每個節(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 經(jīng)典拜占庭容錯方法

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

圖1 經(jīng)典拜占庭容錯方法［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ù)或者取平均值）。經(jīng)典的拜占庭容錯利用的是全連通的獨立信道，在綜合化交換式互連的場景下需要進行改進。

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

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

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

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

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

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

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

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

3.1 SAL工具

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

3.2 SAL模型描述

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

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

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

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

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

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

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

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

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

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

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

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

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

4 模型檢查與結(jié)果分析

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

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

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

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

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

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

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

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

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

5 結(jié)論

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

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

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

TTE網(wǎng)絡(luò)通過COM／MON對能夠?qū)⑽：Τ潭雀叩陌菡纪ス收限D(zhuǎn)化為危害程度較低的不一致遺漏故障，提高了時間觸發(fā)架構(gòu)的容錯能力，降低了容錯所需獨立路徑的個數(shù)。本文的結(jié)果可以為航空航天高安全等級應(yīng)用的容錯配置提供了更規(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é)點拜占庭容錯設(shè)計與驗證［J］. 空間控制技術(shù)與應(yīng)用，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］. 空間控制技術(shù)與應(yīng)用，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ù)總線的故障容錯體系結(jié)構(gòu)的仿真研究［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］／／全國第十三屆空間及運動體控制技術(shù)學術(shù)會議論文集，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)絡(luò)壓縮功能計算開銷的測量方法［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］.計算機應(yīng)用，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.