基于擴(kuò)展標(biāo)記變遷模型的時(shí)鐘同步協(xié)議正確性驗(yàn)證

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

(1. 中國(guó)航空無(wú)線電電子研究所， 上海 200233； 2. 清華大學(xué) 軟件學(xué)院， 北京 100084；3. 北京信息科學(xué)與技術(shù)國(guó)家研究中心， 北京 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)過(guò)一定時(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ò)在我國(guó)航空航天、軌道交通等領(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í)序邏輯刻畫(huà)正確性屬性，基于模型檢測(cè)工具Beagle[4]，對(duì)協(xié)議是否滿足屬性進(jìn)行形式化驗(yàn)證。

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

模型檢測(cè)[5-6]是一種用于有限狀態(tài)并發(fā)系統(tǒng)的形式化驗(yàn)證技術(shù)，在電路驗(yàn)證、通信協(xié)議驗(yàn)證、軟件驗(yàn)證中已經(jīng)取得了巨大的成功。給定系統(tǒng)M和正確性屬性P，模型檢測(cè)通過(guò)搜索M的所有狀態(tài)(或者所有執(zhí)行路徑)來(lái)判定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)典的、針對(duì)有限狀態(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，則稱(chēng)之為系統(tǒng)的一條變遷。設(shè)r∈R為系統(tǒng)M的一條變遷，以l(r)表示r上對(duì)應(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è)被稱(chēng)為守護(hù)條件的表達(dá)式g(r)；η為每條變遷r∈R定義了一個(gè)對(duì)X中變量進(jìn)行賦值的動(dòng)作序列a(r)。

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

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

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

t3[x=15]/x++

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

定義3(簡(jiǎn)單安全屬性驗(yàn)證)給定一個(gè)模型M和一條屬性P，如果在M的所有狀態(tài)上P都成立，則稱(chēng)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í)刻來(lái)協(xié)調(diào)網(wǎng)絡(luò)中的數(shù)據(jù)交換。在時(shí)間觸發(fā)網(wǎng)絡(luò)中，不同網(wǎng)絡(luò)終端的本地時(shí)鐘之間存在偏移，并且這個(gè)偏移會(huì)隨著時(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ò)中，一般稱(chēng)終端設(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é)議的主要過(guò)程是CM收集SM的本地時(shí)鐘，計(jì)算全局時(shí)鐘，然后再分發(fā)給SM的過(guò)程。CM和SM之間的數(shù)據(jù)交換主要依賴(lài)協(xié)議控制幀(Protocol Control Frame, PCF)進(jìn)行。處于空閑狀態(tài)的CM接收到SM的PCF后，進(jìn)入收集狀態(tài)。處于收集狀態(tài)的CM開(kāi)啟一個(gè)時(shí)間窗口，并在該時(shí)間窗口內(nèi)等待后續(xù)PCF。如果CM在時(shí)間窗口內(nèi)接收到一個(gè)新的PCF，將向后延長(zhǎng)一個(gè)窗口長(zhǎng)度的等待時(shí)間。當(dāng)CM收集到的PCF數(shù)量達(dá)到閾值或在一個(gè)窗口時(shí)間內(nèi)沒(méi)有收集到任何新的PCF，CM進(jìn)入到計(jì)算狀態(tài)。在計(jì)算狀態(tài)下，CM對(duì)收集到的所有時(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會(huì)同時(shí)向兩個(gè)CM發(fā)送PCF，兩個(gè)CM獨(dú)立地運(yùn)行同步協(xié)議，將分別計(jì)算全局時(shí)鐘并發(fā)送給所有SM。SM在收到來(lái)自兩個(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)啟動(dòng)是相對(duì)容易出錯(cuò)的時(shí)刻。本文討論了多種啟動(dòng)模式下時(shí)鐘同步協(xié)議的正確性。

1)單CM啟動(dòng)模式：在普通啟動(dòng)模式下，系統(tǒng)中僅含一臺(tái)交換機(jī)(即CM)。這種啟動(dòng)方式比較簡(jiǎn)單。在初始條件下，CM上電后處于非同步狀態(tài)。主管理器正常啟動(dòng)后啟動(dòng)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í)間同步過(guò)程。

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

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

3 協(xié)議建模

基于擴(kuò)展標(biāo)記變遷模型[4]對(duì)時(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)出了每條遷移邊對(duì)應(yīng)的同步標(biāo)記，守護(hù)條件和動(dòng)作序列都被隱去。

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

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

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

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í)間長(zhǎng)度。

假設(shè)r是模型中從控制狀態(tài)s0到s1的一條遷移邊，l(r),g(r)和a(r)分別表示r的標(biāo)記、守護(hù)條件和動(dòng)作序列。本文使用下面的文法表示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í)行該變遷將對(duì)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ā)來(lái)的本地時(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，動(dòng)作序列都為空，其文法表示省略。模型中定義這兩條變遷的目的主要是為了與其他模塊同步。

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)出了每條遷移邊對(duì)應(yīng)的同步標(biāo)記，隱去了守護(hù)條件和動(dòng)作序列。

圖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會(huì)發(fā)送一個(gè)PCF給CM，然后進(jìn)入DISPATCH狀態(tài)。SM在進(jìn)入DIAPATCH狀態(tài)后會(huì)等待，直到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í)間偏移。模型中會(huì)設(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ā)，會(huì)將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)，用來(lái)記錄當(dāng)前SM已經(jīng)給某個(gè)CM發(fā)送了本地時(shí)鐘的情況。注意一個(gè)SM對(duì)于不同的CM的傳輸延遲可能不同，所以在SM模型中，對(duì)于不同CM其對(duì)應(yīng)的deviation的值也不同，觸發(fā)dispatch標(biāo)簽的時(shí)間也不一致。雙CM的模型會(huì)根據(jù)觸發(fā)的dispatch標(biāo)簽編號(hào)進(jìn)入對(duì)應(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)不同的啟動(dòng)模式，本文設(shè)計(jì)了一個(gè)觸發(fā)器模塊TRIGGER?；舅枷胧峭ㄟ^(guò)TRIGGER給當(dāng)前應(yīng)啟動(dòng)的SM和CM發(fā)送啟動(dòng)標(biāo)簽來(lái)模擬不同的啟動(dòng)場(chǎng)景。

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

(a) 同步啟動(dòng)模式(a) Synchronous model

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

3.4 監(jiān)視器模塊

為了更方便地對(duì)協(xié)議模型進(jìn)行驗(yàn)證，設(shè)計(jì)一個(gè)監(jiān)視器模塊MONITOR。MONITOR監(jiān)測(cè)系統(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)簽來(lái)觸發(fā)，代表時(shí)間同步算法已經(jīng)啟動(dòng)。TMP狀態(tài)是為處理雙CM模型所設(shè)計(jì)的臨時(shí)狀態(tài)，單CM模型中沒(méi)有這個(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ā)來(lái)的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è)定的用來(lái)判斷各個(gè)SM的本地時(shí)鐘時(shí)間差是否過(guò)大的閾值。

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

from START to SMALL on start do {

dispatch_num = 0;

max_drift = 10;

};

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

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

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)的變遷說(shuō)明為：

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都會(huì)觸發(fā)這個(gè)變遷并使dispatch_num加1。

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

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

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

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

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

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

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

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

from BIG to TMP on agree_sync_ido {

dispatch_num = 0;

};

from TMP to SMALL on agree_sync_i;

在雙CM的情況下，MONITOR需要收到兩個(gè)CM完成同步分別發(fā)來(lái)的標(biāo)簽agree_sync_0和agree_sync_1，才代表整個(gè)時(shí)鐘同步過(guò)程結(jié)束，因此需要一個(gè)中間狀態(tài)TMP來(lái)緩存收到一個(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í)鐘的誤差不會(huì)超出一個(gè)閾值。根據(jù)前面對(duì)監(jiān)視器模塊的建模，這一屬性可以歸結(jié)為MONITOR模塊永遠(yuǎn)不會(huì)到達(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)不會(huì)到達(dá)CALC終止?fàn)顟B(tài)，SM永遠(yuǎn)不會(huì)到達(dá)最終的SYNC狀態(tài)。如果針對(duì)上面兩條屬性的驗(yàn)證都返回false，說(shuō)明CM和SM可以到達(dá)終止?fàn)顟B(tài)，同步完成屬性成立。反之，對(duì)于任何一條屬性的驗(yàn)證返回true，說(shuō)明對(duì)應(yīng)模塊永遠(yuǎn)不能到達(dá)終止?fàn)顟B(tài)，同步算法不終止。

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

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

4.3 結(jié)果分析

對(duì)時(shí)鐘同步協(xié)議是否滿足時(shí)鐘誤差屬性(以下簡(jiǎn)稱(chēng)P1)和同步完成屬性(以下簡(jiǎn)稱(chēng)P2)進(jìn)行驗(yàn)證。實(shí)驗(yàn)中，根據(jù)單CM和雙CM的不同啟動(dòng)方式，以及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列為啟動(dòng)模式(第2節(jié)中介紹的3種啟動(dòng)模式分別以1，2，3表示)。采用限界模型檢測(cè)執(zhí)行驗(yàn)證，第5列表示限界模型檢測(cè)展開(kāi)的步數(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í)間與模型展開(kāi)步數(shù)正相關(guān)。這是因?yàn)楫?dāng)展開(kāi)步數(shù)增加時(shí)，整個(gè)模型的規(guī)模變大，驗(yàn)證所需的時(shí)間因此也將增大。

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

5 相關(guān)工作

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

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

6 結(jié)論

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