曲國遠(yuǎn)，徐曉飛，劉威廷，王沁煜，賀 飛

(1. 中國航空無線電電子研究所， 上海 200233； 2. 清華大學(xué) 軟件學(xué)院， 北京 100084；3. 北京信息科學(xué)與技術(shù)國家研究中心， 北京 100084； 4. 信息系統(tǒng)安全教育部重點(diǎn)實(shí)驗(yàn)室， 北京 100084)

時(shí)間觸發(fā)網(wǎng)絡(luò)[1-3]被廣泛應(yīng)用于航空航天、軌道交通、軍事裝備等實(shí)時(shí)性要求高的系統(tǒng)中。在時(shí)間觸發(fā)網(wǎng)絡(luò)中，所有網(wǎng)絡(luò)消息都由預(yù)先定義的時(shí)刻進(jìn)行觸發(fā)。時(shí)間觸發(fā)網(wǎng)絡(luò)能夠保證網(wǎng)絡(luò)中每一個(gè)終端在某一個(gè)時(shí)刻最多只能發(fā)送一條消息。相比于傳統(tǒng)的基于事件觸發(fā)的網(wǎng)絡(luò)，時(shí)間觸發(fā)網(wǎng)絡(luò)具有更好的通信實(shí)時(shí)性和確定性。

時(shí)間觸發(fā)網(wǎng)絡(luò)必須實(shí)現(xiàn)網(wǎng)絡(luò)中所有設(shè)備的時(shí)鐘同步?？紤]每一個(gè)網(wǎng)絡(luò)設(shè)備都有自己的本地時(shí)鐘，不同設(shè)備的本地時(shí)鐘之間存在偏移，并且這個(gè)偏移在經(jīng)過一定時(shí)間的累積后，可達(dá)到一個(gè)不可忽視的程度。時(shí)間觸發(fā)網(wǎng)絡(luò)利用時(shí)鐘同步協(xié)議建立一個(gè)全局統(tǒng)一的系統(tǒng)時(shí)鐘，并且基于該系統(tǒng)時(shí)鐘調(diào)度網(wǎng)絡(luò)中的所有通信。

時(shí)間觸發(fā)網(wǎng)絡(luò)在我國航空航天、軌道交通等領(lǐng)域有很好的應(yīng)用前景。在將該網(wǎng)絡(luò)引入這些應(yīng)用領(lǐng)域前，需要進(jìn)行適應(yīng)性的補(bǔ)充與修改。如何證明修改后的時(shí)鐘同步協(xié)議仍然具有正確性成為制約時(shí)間觸發(fā)網(wǎng)絡(luò)在這些系統(tǒng)中進(jìn)行應(yīng)用的關(guān)鍵。

本文以擴(kuò)展標(biāo)記變遷模型描述協(xié)議行為，以時(shí)序邏輯刻畫正確性屬性，基于模型檢測工具Beagle[4]，對協(xié)議是否滿足屬性進(jìn)行形式化驗(yàn)證。

1 擴(kuò)展標(biāo)記變遷模型

模型檢測[5-6]是一種用于有限狀態(tài)并發(fā)系統(tǒng)的形式化驗(yàn)證技術(shù)，在電路驗(yàn)證、通信協(xié)議驗(yàn)證、軟件驗(yàn)證中已經(jīng)取得了巨大的成功。給定系統(tǒng)M和正確性屬性P，模型檢測通過搜索M的所有狀態(tài)(或者所有執(zhí)行路徑)來判定M是否滿足P。

在給定網(wǎng)絡(luò)節(jié)點(diǎn)的情況下，時(shí)間觸發(fā)網(wǎng)絡(luò)[1]就是一個(gè)典型的有限狀態(tài)并發(fā)系統(tǒng)。標(biāo)記變遷(Labeled Transition System, LTS)模型是一種經(jīng)典的、針對有限狀態(tài)并發(fā)系統(tǒng)的形式化模型。

定義1(LTS模型)令A(yù)P為原子命題集合，一個(gè)標(biāo)記變遷模型是一個(gè)四元組M=(Σ,S,S0,R),其中Σ是標(biāo)記的有限集，S是狀態(tài)的有限集，S0?S為初始狀態(tài)的集合，R∈S×Σ×S是變遷關(guān)系。

設(shè)s,t∈S為系統(tǒng)的兩個(gè)狀態(tài)，α∈Σ為系統(tǒng)的一個(gè)標(biāo)記，如果〈s,α,t〉∈R，則稱之為系統(tǒng)的一條變遷。設(shè)r∈R為系統(tǒng)M的一條變遷，以l(r)表示r上對應(yīng)的標(biāo)記。

標(biāo)記變遷模型中S為系統(tǒng)中所有狀態(tài)的集合。當(dāng)系統(tǒng)狀態(tài)空間較大時(shí)，難以直接使用LTS進(jìn)行建模。擴(kuò)展標(biāo)記變遷(Extended Labeled Transition System, ELTS)模型在LTS的基礎(chǔ)上擴(kuò)展了變量，能夠更方便地描述規(guī)模較大的系統(tǒng)。

定義2(ELTS模型)令A(yù)P為原子命題集合，一個(gè)擴(kuò)展標(biāo)記變遷模型是一個(gè)七元組M=(Σ,X,S,S0,R,τ,η),其中(Σ,S,S0,R)是一個(gè)LTS模型；X是變量的有限集；τ為每條變遷r∈R定義了一個(gè)被稱為守護(hù)條件的表達(dá)式g(r)；η為每條變遷r∈R定義了一個(gè)對X中變量進(jìn)行賦值的動作序列a(r)。

ELTS模型的狀態(tài)是對X∪L的一組賦值，稱ELTS中的L為控制狀態(tài)集合。設(shè)r∈R為系統(tǒng)的一條變遷，r常被表示為：

l(r)[g(r)]:a(r)

圖1給出了一個(gè)信號燈控制系統(tǒng)的ELTS模型。該模型中含有2個(gè)控制狀態(tài)，即Red和Green，分別代表紅色和綠色信號燈。模型中含有1個(gè)變量x，代表時(shí)間。為簡單起見，圖中守護(hù)條件為true時(shí)可以省略，動作序列為空時(shí)也可以省略。該信號燈控制系統(tǒng)的初始控制狀態(tài)為Red，從Red到Green的邊

t3[x=15]/x++

表示該變遷在x的值等于15時(shí)可以被觸發(fā)，并且執(zhí)行該變遷會導(dǎo)致x的值加1。其他邊可以類似地進(jìn)行分析。

定義3(簡單安全屬性驗(yàn)證)給定一個(gè)模型M和一條屬性P，如果在M的所有狀態(tài)上P都成立，則稱M滿足P(記作MP)。

以圖1為例，假設(shè)屬性為x<60，顯然該屬性在M的所有狀態(tài)上都成立，所以MP成立。

圖1 ELTS示例圖Fig.1 An ELTS example

2 時(shí)鐘同步協(xié)議

時(shí)間觸發(fā)網(wǎng)絡(luò)[1]按照事先設(shè)定的時(shí)刻來協(xié)調(diào)網(wǎng)絡(luò)中的數(shù)據(jù)交換。在時(shí)間觸發(fā)網(wǎng)絡(luò)中，不同網(wǎng)絡(luò)終端的本地時(shí)鐘之間存在偏移，并且這個(gè)偏移會隨著時(shí)間累積。為實(shí)現(xiàn)時(shí)間觸發(fā)網(wǎng)絡(luò)，必須借助時(shí)鐘同步協(xié)議，將網(wǎng)絡(luò)中所有設(shè)備的時(shí)鐘誤差控制在一定范圍內(nèi)。

時(shí)間觸發(fā)網(wǎng)絡(luò)[1]中的設(shè)備主要包括交換機(jī)和終端。在時(shí)間觸發(fā)網(wǎng)絡(luò)中，一般稱終端設(shè)備為同步主(Synchronize Master, SM)，交換機(jī)為壓縮主(Compression Master, CM)。圖2給出了一個(gè)包括4個(gè)同步主和1個(gè)壓縮主的時(shí)間觸發(fā)網(wǎng)絡(luò)，其中實(shí)線代表設(shè)備之間的物理連接。

圖2 時(shí)間觸發(fā)網(wǎng)絡(luò)示意圖Fig.2 The time-triggered network

時(shí)鐘同步協(xié)議的主要過程是CM收集SM的本地時(shí)鐘，計(jì)算全局時(shí)鐘，然后再分發(fā)給SM的過程。CM和SM之間的數(shù)據(jù)交換主要依賴協(xié)議控制幀(Protocol Control Frame, PCF)進(jìn)行。處于空閑狀態(tài)的CM接收到SM的PCF后，進(jìn)入收集狀態(tài)。處于收集狀態(tài)的CM開啟一個(gè)時(shí)間窗口，并在該時(shí)間窗口內(nèi)等待后續(xù)PCF。如果CM在時(shí)間窗口內(nèi)接收到一個(gè)新的PCF，將向后延長一個(gè)窗口長度的等待時(shí)間。當(dāng)CM收集到的PCF數(shù)量達(dá)到閾值或在一個(gè)窗口時(shí)間內(nèi)沒有收集到任何新的PCF，CM進(jìn)入到計(jì)算狀態(tài)。在計(jì)算狀態(tài)下，CM對收集到的所有時(shí)鐘進(jìn)行計(jì)算，并將計(jì)算結(jié)果分發(fā)給所有SM，供SM進(jìn)行時(shí)鐘同步。

時(shí)間觸發(fā)網(wǎng)絡(luò)支持雙CM備份。一個(gè)包含2個(gè)CM的時(shí)間觸發(fā)網(wǎng)如圖3所示。在雙CM備份網(wǎng)絡(luò)中，為防止主CM故障導(dǎo)致網(wǎng)絡(luò)結(jié)構(gòu)癱瘓，設(shè)置備用CM用于故障恢復(fù)。所有SM會同時(shí)向兩個(gè)CM發(fā)送PCF，兩個(gè)CM獨(dú)立地運(yùn)行同步協(xié)議，將分別計(jì)算全局時(shí)鐘并發(fā)送給所有SM。SM在收到來自兩個(gè)CM的全局時(shí)鐘時(shí)，有多種策略，例如只采用主CM的時(shí)鐘、采用兩個(gè)CM時(shí)鐘的平均值等。本文假定SM采用前一個(gè)策略，即只使用主CM時(shí)鐘。

圖3 雙CM冗余時(shí)間觸發(fā)網(wǎng)絡(luò)Fig.3 A time-triggered network with double CMs

將時(shí)鐘同步協(xié)議應(yīng)用到航空航天等實(shí)際系統(tǒng)中時(shí)，系統(tǒng)啟動是相對容易出錯的時(shí)刻。本文討論了多種啟動模式下時(shí)鐘同步協(xié)議的正確性。

1)單CM啟動模式：在普通啟動模式下，系統(tǒng)中僅含一臺交換機(jī)(即CM)。這種啟動方式比較簡單。在初始條件下，CM上電后處于非同步狀態(tài)。主管理器正常啟動后啟動PCF發(fā)送，CM收到PCF后進(jìn)入同步狀態(tài)，并轉(zhuǎn)發(fā)PCF。各個(gè)SM上網(wǎng)后，同步到CM轉(zhuǎn)發(fā)的PCF時(shí)間，周期性地發(fā)送PCF，參與時(shí)間同步過程。

2)雙CM同步啟動模式：在該模式下，系統(tǒng)中包含兩臺CM，并且兩臺CM同步啟動。首先雙CM上電后處于非同步狀態(tài)，主管理器爭權(quán)成功，通過雙通道啟動PCF發(fā)送，兩個(gè)CM收到PCF后，都進(jìn)入同步狀態(tài)，并轉(zhuǎn)發(fā)PCF。各個(gè)SM上網(wǎng)后，從工作網(wǎng)絡(luò)接收PCF，并同步時(shí)鐘，周期性地通過雙通道發(fā)送PCF，參與時(shí)間同步過程。

3)雙CM異步啟動模式：雙CM異步啟動的工作模式允許先在單CM的情況下工作一段時(shí)間后再將另一個(gè)CM加入時(shí)間同步網(wǎng)絡(luò)。與同步啟動模式相比，異步啟動更靈活且適用性更廣。首先，單CM上電，系統(tǒng)進(jìn)入時(shí)間同步狀態(tài)。另一個(gè)CM上電，進(jìn)入非同步狀態(tài)。各個(gè)SM節(jié)點(diǎn)通過雙通道發(fā)送PCF給雙CM，CM進(jìn)入同步狀態(tài)，并同步到接收的時(shí)鐘，用第一個(gè)接收到的時(shí)鐘設(shè)置本地時(shí)鐘，可以和接收到幾個(gè)時(shí)鐘無關(guān)。各個(gè)SM周期性地發(fā)送PCF參與同步，各個(gè)SM依舊同步到工作網(wǎng)絡(luò)。

3 協(xié)議建模

基于擴(kuò)展標(biāo)記變遷模型[4]對時(shí)鐘同步協(xié)議進(jìn)行建模，所建模型主要包含4個(gè)模塊，分別是壓縮主CM模塊、同步主SM模塊、觸發(fā)器TRIGGER模塊和監(jiān)視器MONITOR模塊。

3.1 CM模塊

CM模塊包含五個(gè)控制狀態(tài)，分別為：初始狀態(tài)START、空閑狀態(tài)IDLE、收集狀態(tài)COLLECTION、延遲狀態(tài)DELAY和計(jì)算狀態(tài)CALC。CM模塊的ELTS模型如圖4所示。為方便閱讀和理解，在圖4中只標(biāo)出了每條遷移邊對應(yīng)的同步標(biāo)記，守護(hù)條件和動作序列都被隱去。

圖4 CM模型示意圖Fig.4 The CM model

處于START狀態(tài)的CM接收到start同步標(biāo)簽后進(jìn)入IDLE狀態(tài)，此時(shí)CM會等待SM發(fā)送PCF。當(dāng)收到第一個(gè)PCF后，CM進(jìn)入COLLECTION狀態(tài)。處于COLLECTION的CM循環(huán)等待不同的SM發(fā)來的PCF，直到收到的PCF數(shù)量等于所有SM的數(shù)量。之后CM進(jìn)入DELAY狀態(tài)，延遲一段時(shí)間并通過時(shí)間同步算法計(jì)算出統(tǒng)一時(shí)鐘，然后進(jìn)入CALC狀態(tài)，通過calc同步標(biāo)簽對各個(gè)SM進(jìn)行時(shí)間同步。最后在轉(zhuǎn)移回START狀態(tài)之前，CM通過agree_sync同步標(biāo)簽通知MONITOR模塊已經(jīng)完成時(shí)間同步，從而模擬分發(fā)統(tǒng)一時(shí)間的PCF，等待下一個(gè)循環(huán)周期的開始。

下面定義圖4中每一條遷移邊的守護(hù)條件和動作序列。首先引入下列變量：

int clock;

int current_reading_index;

int SM_amount;

int delay_timeout;

其中，clock是CM的本地時(shí)鐘，current_reading_index是CM當(dāng)前收到的PCF數(shù)量，SM_amount是系統(tǒng)中SM數(shù)量，delay_timeout代表了CM計(jì)算統(tǒng)一時(shí)間時(shí)需要延遲的時(shí)間長度。

假設(shè)r是模型中從控制狀態(tài)s0到s1的一條遷移邊，l(r),g(r)和a(r)分別表示r的標(biāo)記、守護(hù)條件和動作序列。本文使用下面的文法表示r:

froms0tos1onl(r) providedg(r) doa(r);

根據(jù)上面的文法，CM模塊從START狀態(tài)到IDLE狀態(tài)的變遷可以表示為：

from START to IDLE on start do {

clock = 0;

SM_amount = 5;

current_reading_index = 0;

delay_timeout = 5;

};

這條變遷的守護(hù)條件為true，執(zhí)行該變遷將對CM中的各個(gè)變量進(jìn)行初始化操作。

CM模塊從IDLE狀態(tài)到COLLECTION狀態(tài)的變遷表示為：

from IDLE to COLLECTION on dispatchi

provided (current_reading_index == 0)

do {

current_reading_index = 1;

};

該變遷必須在current_reading_index==0的條件下由第i個(gè)SM發(fā)出的dispatchi觸發(fā)，執(zhí)行該變遷將賦值current_reading_index=1。

CM模塊從COLLECTION狀態(tài)到COLLECTION狀態(tài)的變遷表示為：

from COLLECTION to COLLECTION

on dispatchi

provided

current_reading_index < SM_amount

do {

current_reading_index =

current_reading_index + 1;

};

這是CM收集不同SM發(fā)出的dispatchi時(shí)執(zhí)行的變遷，該變遷反復(fù)執(zhí)行，直到CM收到的PCF數(shù)量等于系統(tǒng)中SM的總數(shù)，每次執(zhí)行導(dǎo)致current_reading_index的計(jì)數(shù)加1。

DELAY狀態(tài)模擬了CM收集完所有SM發(fā)來的本地時(shí)鐘后進(jìn)行全局時(shí)鐘計(jì)算所產(chǎn)生的延遲。這里的 delay_timeout為預(yù)先設(shè)定的一個(gè)延遲時(shí)間。CM模塊從COLLECTION狀態(tài)到DELAY狀態(tài)，從DELAY狀態(tài)到CALC狀態(tài)的變遷的守護(hù)條件均為true，動作序列都為空，其文法表示省略。模型中定義這兩條變遷的目的主要是為了與其他模塊同步。

CM模塊從CALC狀態(tài)到START狀態(tài)的變遷表示為：

from CALC to START on agree_sync

provided delay_timeout == 0 do {

current_reading_index = 0;

delay_timeout = 0;

clock = clock + 1;

};

該變遷主要用于各個(gè)變量值的重置，以及利用agree_sync標(biāo)簽與MONOITOR模塊同步，表示CM的一個(gè)計(jì)算周期結(jié)束。

3.2 SM模塊

SM模塊的行為與網(wǎng)絡(luò)中包含的CM個(gè)數(shù)相關(guān)。下面分情況討論單CM網(wǎng)絡(luò)和雙CM網(wǎng)絡(luò)中SM模塊的形式化模型。

3.2.1 單CM網(wǎng)絡(luò)的SM模塊

單CM的SM模型包含四個(gè)控制狀態(tài)，分別是：初始狀態(tài)START、空閑狀態(tài)IDLE、分發(fā)狀態(tài)DISPATCH和同步狀態(tài)SYNC。其ELTS模型如圖5所示。同樣，在圖5中只標(biāo)出了每條遷移邊對應(yīng)的同步標(biāo)記，隱去了守護(hù)條件和動作序列。

圖5 單CM的SM模型Fig.5 SM model in a single-CM network

處于START狀態(tài)的SM模塊收到start標(biāo)簽后進(jìn)入IDLE狀態(tài)。當(dāng)SM的本地時(shí)鐘到達(dá)預(yù)定的發(fā)送時(shí)刻，SM會發(fā)送一個(gè)PCF給CM，然后進(jìn)入DISPATCH狀態(tài)。SM在進(jìn)入DIAPATCH狀態(tài)后會等待，直到CM計(jì)算出全局時(shí)鐘。最后，SM收到CM計(jì)算的全局時(shí)鐘，進(jìn)入SYNC狀態(tài)完成時(shí)鐘同步。

為詳細(xì)定義SM模塊的每條遷移，需要引入下列變量：

int clock;

int dispatch_timeout;

int deviation;

其中，clock是SM的本地時(shí)鐘，dispatch_timeout是預(yù)先設(shè)定的發(fā)送時(shí)間點(diǎn)，deviation則是為了模擬現(xiàn)實(shí)的晶振誤差和傳輸延遲所設(shè)定的一個(gè)時(shí)間偏移。模型中會設(shè)定deviation為一個(gè)0到5范圍內(nèi)的隨機(jī)數(shù)。

SM模塊從START狀態(tài)到IDLE狀態(tài)的變遷表示為：

from START to IDLE on start do {

clock = dispatch_timeout + deviation;

dispatch_timeout = 0;

deviation = 0;

};

這個(gè)遷移由start標(biāo)簽觸發(fā)，會將SM的本地時(shí)鐘置成dispatch_timeout與deviation的和，表示CM收到的SM的本地時(shí)鐘存在時(shí)間偏移。

SM模塊從IDLE狀態(tài)轉(zhuǎn)移到DISPATCH狀態(tài)的變遷表示為：

from IDLE to DISPATCH on dispatchiprovided

deviation ==0 && dispatch_timeout == 0;

該遷移需要滿足deviation和dispatch_timeout的值都為零的守護(hù)條件才能觸發(fā)，執(zhí)行此遷移將發(fā)送第i個(gè)SM的dispatchi標(biāo)簽給CM模塊。

SM模塊從DISPATCH狀態(tài)到SYNC狀態(tài)的變遷表示為：

from DISPATCH to SYNC on calc do {

clock = CM.clock;

};

當(dāng)處于DISPATCH狀態(tài)的SM收到CM模塊發(fā)出的calc標(biāo)簽時(shí)，表示CM已經(jīng)完成了時(shí)間同步，此時(shí)需要將SM的本地時(shí)鐘更新成CM的全局時(shí)鐘，并轉(zhuǎn)移至SYNC狀態(tài)。

SM模塊從SYNC狀態(tài)到START狀態(tài)的變遷表示為：

from SYNC to START on sync;

當(dāng)SM處于SYNC狀態(tài)時(shí)代表了SM的本地時(shí)鐘已經(jīng)處于了同步狀態(tài)，需要等待所有其他SM都到達(dá)同步狀態(tài)后一起返回START狀態(tài)完成一個(gè)同步周期。

3.2.2 雙CM網(wǎng)絡(luò)的SM模塊

雙CM網(wǎng)絡(luò)中SM模塊的ELTS模型如圖6所示。相比于單CM網(wǎng)絡(luò)的模型，該SM模型主要多了一個(gè)DISPATCH狀態(tài)，用來記錄當(dāng)前SM已經(jīng)給某個(gè)CM發(fā)送了本地時(shí)鐘的情況。注意一個(gè)SM對于不同的CM的傳輸延遲可能不同，所以在SM模型中，對于不同CM其對應(yīng)的deviation的值也不同，觸發(fā)dispatch標(biāo)簽的時(shí)間也不一致。雙CM的模型會根據(jù)觸發(fā)的dispatch標(biāo)簽編號進(jìn)入對應(yīng)的DISPATCH狀態(tài)，然后等待本地時(shí)鐘值到達(dá)觸發(fā)另一個(gè)dispatch標(biāo)簽時(shí)進(jìn)入END狀態(tài)，代表SM模塊已經(jīng)發(fā)送。

圖6 雙CM的SM模型Fig.6 SM model in a double-CMs network

3.3 觸發(fā)器模塊

為了實(shí)現(xiàn)不同的啟動模式，本文設(shè)計(jì)了一個(gè)觸發(fā)器模塊TRIGGER。基本思想是通過TRIGGER給當(dāng)前應(yīng)啟動的SM和CM發(fā)送啟動標(biāo)簽來模擬不同的啟動場景。

同步和異步啟動模式下TRIGGER模塊的ELTS模型分別如圖7(a)和圖7(b)所示。觸發(fā)器一開始處在IDLE狀態(tài)并等待啟動。對于同步啟動模式(無論單CM或雙CM)，觸發(fā)器只需向所有的SM和CM以及MONITOR發(fā)送一次start標(biāo)簽即可。對于異步啟動模式，觸發(fā)器先轉(zhuǎn)移至WORKING1狀態(tài)，并向需要先啟動的模塊發(fā)送start標(biāo)簽，然后再向后啟動的模塊發(fā)送later_start標(biāo)簽去觸發(fā)它們啟動。在完成一個(gè)完整的同步周期后，通過一個(gè)start標(biāo)簽回到WORKING1狀態(tài)，重新進(jìn)入啟動狀態(tài)等待新一個(gè)同步周期的開始。

(a) 同步啟動模式(a) Synchronous model

(b) 異步啟動模式(b) Asynchronous mode圖7 TRIGGER模型Fig.7 The TRIGGER model

3.4 監(jiān)視器模塊

為了更方便地對協(xié)議模型進(jìn)行驗(yàn)證，設(shè)計(jì)一個(gè)監(jiān)視器模塊MONITOR。MONITOR監(jiān)測系統(tǒng)中所有SM的本地時(shí)鐘，并判斷其同步精度是否在預(yù)先設(shè)定的范圍之內(nèi)。

圖8 MONITOR模型Fig.8 The MONITOR model

監(jiān)視器模塊的ELTS模型如圖8所示。監(jiān)視器模塊包含四個(gè)控制狀態(tài)，分別為：START，SMALL，BIG和BAD。START為初始狀態(tài)。SMALL表示當(dāng)前網(wǎng)絡(luò)處于同步狀態(tài)，各個(gè)SM本地時(shí)鐘之間的差值應(yīng)該較小(或者近似相等)，否則監(jiān)視器進(jìn)入BAD狀態(tài)。BIG表示當(dāng)前網(wǎng)絡(luò)正在運(yùn)行時(shí)鐘同步協(xié)議，各個(gè)SM本地時(shí)鐘之間的差值可能較大，但也應(yīng)該在一個(gè)預(yù)先設(shè)定的范圍之內(nèi)。如果超出該預(yù)先設(shè)定的范圍，監(jiān)視器也進(jìn)入BAD狀態(tài)。

處于START狀態(tài)的監(jiān)視器收到start標(biāo)簽后遷移到SMALL狀態(tài)。從SMALL狀態(tài)轉(zhuǎn)移到BIG狀態(tài)需要等待任意一個(gè)SM發(fā)出dispatchi標(biāo)簽來觸發(fā)，代表時(shí)間同步算法已經(jīng)啟動。TMP狀態(tài)是為處理雙CM模型所設(shè)計(jì)的臨時(shí)狀態(tài)，單CM模型中沒有這個(gè)狀態(tài)。處于BIG狀態(tài)的MONITOR收到CM0發(fā)出的agree_sync_0或CM1發(fā)出的agree_sync_1標(biāo)簽后轉(zhuǎn)移到TMP狀態(tài)，繼續(xù)等待另一個(gè)CM發(fā)來的agree_sync標(biāo)簽，然后轉(zhuǎn)移至SMALL狀態(tài)。

MONITOR模塊中變量聲明為：

int dispatch_num;

int max_drift;

其中，dispatch_num是當(dāng)前已經(jīng)發(fā)出PCF的SM數(shù)量，max_drift是預(yù)先設(shè)定的用來判斷各個(gè)SM的本地時(shí)鐘時(shí)間差是否過大的閾值。

MONITOR模塊從START狀態(tài)到SMALL狀態(tài)的變遷說明為：

from START to SMALL on start do {

dispatch_num = 0;

max_drift = 10;

};

主要執(zhí)行對MONITOR變量的初始化。

MONITOR模塊從SMALL狀態(tài)到BIG狀態(tài)的變遷說明為：

from SMALL to BIG on dispatchiprovided

dispatch_num == 0 do {

dispatch_num = dispatch_num + 1;

};

處于SMALL狀態(tài)的MONITOR收到任一個(gè)SM發(fā)出的dispatchi標(biāo)簽后觸發(fā)該變遷，并將dispatch_num的值加1。

MONITOR模塊從BIG狀態(tài)到BIG狀態(tài)的變遷說明為：

from BIG to BIG on dispatchiprovided dispatch_num > 0 and dispatch_num < CM_amount * SM_amount do {

dispatch_num = dispatch_num + 1;

};

當(dāng)dispatch_num大于0且小于CM數(shù)量乘以SM數(shù)量時(shí)，每個(gè)SM發(fā)出的dispatchi都會觸發(fā)這個(gè)變遷并使dispatch_num加1。

MONITOR模塊從SMALL狀態(tài)到BAD狀態(tài)的變遷說明為：

from SMALL to BAD provided!(SMi.clock==SMj.clock);

其中，“！”表示否定。處于SMALL狀態(tài)的MONITOR會檢測每兩個(gè)SM之間的本地時(shí)鐘是否相同。如果存在不同的時(shí)鐘則會進(jìn)入BAD狀態(tài)。

MONITOR模塊從BIG狀態(tài)到BAD狀態(tài)的變遷說明為：

from BIG to BAD provided (SMi.clock>SMj.clock + max_drift) && (dispatch_num == SM_amount);

處于BIG狀態(tài)的MONITOR會檢測每兩個(gè)SM之間的本地時(shí)鐘之差是否超過設(shè)定的閾值max_drift。如果存在兩個(gè)SM之間的時(shí)鐘差超過max_drift且收到PCF的SM數(shù)量dispatch_num等于SM總數(shù)SM_amount，則會進(jìn)入BAD狀態(tài)。

當(dāng)驗(yàn)證包含兩個(gè)CM的系統(tǒng)時(shí)需要在BIG狀態(tài)到SMALL狀態(tài)的中間加入TMP狀態(tài)用來接收兩個(gè)不同CM的時(shí)鐘同步信號。

MONITOR模塊從BIG狀態(tài)到TMP狀態(tài)，以及從TMP狀態(tài)到SMALL狀態(tài)的變遷說明為：

from BIG to TMP on agree_sync_ido {

dispatch_num = 0;

};

from TMP to SMALL on agree_sync_i;

在雙CM的情況下，MONITOR需要收到兩個(gè)CM完成同步分別發(fā)來的標(biāo)簽agree_sync_0和agree_sync_1，才代表整個(gè)時(shí)鐘同步過程結(jié)束，因此需要一個(gè)中間狀態(tài)TMP來緩存收到一個(gè)agree_sync_i標(biāo)簽的情況。

4 協(xié)議驗(yàn)證

4.1 驗(yàn)證屬性

為保證時(shí)鐘同步協(xié)議模型的正確性，驗(yàn)證下列兩條屬性。

4.1.1 時(shí)鐘誤差屬性

時(shí)鐘同步協(xié)議的基本目標(biāo)是保證任何時(shí)刻所有SM本地時(shí)鐘的誤差不會超出一個(gè)閾值。根據(jù)前面對監(jiān)視器模塊的建模，這一屬性可以歸結(jié)為MONITOR模塊永遠(yuǎn)不會到達(dá)BAD狀態(tài)，即

INVARSPEC !(MONITOR.location == BAD)

4.1.2 同步完成屬性

除了時(shí)鐘誤差屬性外，還需要保證SM和CM運(yùn)行的時(shí)鐘同步算法最后都能正常終止，到達(dá)終止?fàn)顟B(tài)。采用反證法，分別驗(yàn)證

INVARSPEC !(CM.location == CALC)

INVARSPEC !(SM.location == SYNC)

即CM永遠(yuǎn)不會到達(dá)CALC終止?fàn)顟B(tài)，SM永遠(yuǎn)不會到達(dá)最終的SYNC狀態(tài)。如果針對上面兩條屬性的驗(yàn)證都返回false，說明CM和SM可以到達(dá)終止?fàn)顟B(tài)，同步完成屬性成立。反之，對于任何一條屬性的驗(yàn)證返回true，說明對應(yīng)模塊永遠(yuǎn)不能到達(dá)終止?fàn)顟B(tài)，同步算法不終止。

4.2 驗(yàn)證環(huán)境

本節(jié)對4.1小節(jié)提到的不同屬性，在不同的SM和CM數(shù)量配置下進(jìn)行了驗(yàn)證，試驗(yàn)環(huán)境為：Intel(R) Xeon(R) CPU E5-2620 v3 @ 2.40 GHz，32 056 M內(nèi)存，操作系統(tǒng)為Ubuntu 16.04.2 LTS。

實(shí)驗(yàn)采用Beagle[4]執(zhí)行模型檢測。Beagle是清華大學(xué)軟件學(xué)院開發(fā)的一個(gè)基于ELTS的模型檢測工具。Beagle工具中分別基于二叉決策圖(Binary Decision Diagram, BDD)和可滿足性(SATisfiability, SAT)實(shí)現(xiàn)了基本的模型檢測方法，并在此基礎(chǔ)上，提出了一系列針對構(gòu)件化系統(tǒng)的高效模型檢測算法[7-10]。

4.3 結(jié)果分析

對時(shí)鐘同步協(xié)議是否滿足時(shí)鐘誤差屬性(以下簡稱P1)和同步完成屬性(以下簡稱P2)進(jìn)行驗(yàn)證。實(shí)驗(yàn)中，根據(jù)單CM和雙CM的不同啟動方式，以及SM的數(shù)量分別構(gòu)建了時(shí)鐘同步協(xié)議的模型，并執(zhí)行驗(yàn)證。

驗(yàn)證結(jié)果如表1所示，其中第1列表示驗(yàn)證的屬性，第2列和第3列表示網(wǎng)絡(luò)中包含的CM和SM數(shù)量，第4列為啟動模式(第2節(jié)中介紹的3種啟動模式分別以1，2，3表示)。采用限界模型檢測執(zhí)行驗(yàn)證，第5列表示限界模型檢測展開的步數(shù)，第6列表示驗(yàn)證所需的時(shí)間，第7列表示屬性驗(yàn)證的結(jié)果。注意屬性P1為true、屬性P2為false為期望的模型驗(yàn)證結(jié)果。

從表1中可以發(fā)現(xiàn)，在給定的網(wǎng)絡(luò)結(jié)構(gòu)下，時(shí)鐘同步屬性和同步完成屬性的驗(yàn)證結(jié)果都與期望一致。因此時(shí)鐘同步協(xié)議在這些網(wǎng)絡(luò)結(jié)構(gòu)下的正確性得到驗(yàn)證。另外，可以觀察到，驗(yàn)證所需時(shí)間與模型展開步數(shù)正相關(guān)。這是因?yàn)楫?dāng)展開步數(shù)增加時(shí)，整個(gè)模型的規(guī)模變大，驗(yàn)證所需的時(shí)間因此也將增大。

表1 實(shí)驗(yàn)結(jié)果

5 相關(guān)工作

模型檢測在協(xié)議驗(yàn)證方面得到了廣泛的應(yīng)用,例如路由協(xié)議驗(yàn)證、密碼協(xié)議驗(yàn)證、網(wǎng)絡(luò)協(xié)議驗(yàn)證等。在文獻(xiàn)[11]中，Roy等采用概率時(shí)間自動機(jī)來驗(yàn)證在無線局域網(wǎng)IEEE0802.11協(xié)議中的介質(zhì)訪問控制層協(xié)議，采用確定路徑壓縮算法優(yōu)化模型，減少協(xié)議中的冗余，以應(yīng)對驗(yàn)證中的狀態(tài)爆炸空間問題。在文獻(xiàn)[12]中，Esparza等驗(yàn)證了Population protocol的正確性，該協(xié)議是主要應(yīng)用在傳感器網(wǎng)絡(luò)中的形式化模型,用于在不同設(shè)備之間獲得一致的值，設(shè)備與設(shè)備之間通過交互以改變自身狀態(tài)。在文獻(xiàn)[13]中，He等驗(yàn)證了發(fā)布訂閱分布式協(xié)議的正確性。

Steiner和Dutertre等對TTEthernet中的時(shí)鐘同步協(xié)議標(biāo)準(zhǔn)進(jìn)行了驗(yàn)證[14-16]。他們基于SAL model checker實(shí)現(xiàn)了對同步算法的正確性分析，并驗(yàn)證了在協(xié)議規(guī)定下，系統(tǒng)滿足的同步精度范圍。與他們的工作相比，本文采用了一種新的建模語言(即擴(kuò)展標(biāo)記變遷模型)，建模過程說明了該語言對于時(shí)鐘同步協(xié)議驗(yàn)證的有效性。特別地，本文所建立的模型中考慮了時(shí)間觸發(fā)網(wǎng)絡(luò)的不同啟動模式。該特性是時(shí)間觸發(fā)網(wǎng)絡(luò)國際標(biāo)準(zhǔn)中沒有規(guī)定的內(nèi)容，但卻是將時(shí)間觸發(fā)網(wǎng)絡(luò)引入到我國航空領(lǐng)域某系統(tǒng)的設(shè)計(jì)中所必須考慮的一個(gè)適配性問題。本文結(jié)果為該系統(tǒng)的設(shè)計(jì)提供了可信依據(jù)。

6 結(jié)論

本文給出了一種基于擴(kuò)展標(biāo)記變遷模型對時(shí)鐘同步協(xié)議進(jìn)行建模的方法，并基于模型檢測工具對其正確性進(jìn)行了驗(yàn)證。除了標(biāo)準(zhǔn)中規(guī)定的時(shí)鐘同步協(xié)議外，還對多個(gè)啟動場景下協(xié)議的正確性進(jìn)行了分析與驗(yàn)證。驗(yàn)證結(jié)果證明了在復(fù)雜啟動場景下時(shí)鐘同步網(wǎng)絡(luò)協(xié)議的正確性，也表明了擴(kuò)展標(biāo)記變遷模型對于協(xié)議驗(yàn)證的有效性。