王長青

同濟(jì)大學(xué)軟件學(xué)院，上海 201804

0 引言

在嵌入式系統(tǒng)中，有很多是基于通信協(xié)議的消息傳遞，那么一個消息從發(fā)送到接受需要多少時間呢？多個消息傳輸又需要多少時間呢？有沒有減少通信時間的可能性？因此，為了研究這幾個問題，我們做了一個實驗，即我們模擬一個通信協(xié)議，我們把這個通信協(xié)議通過UPPAAL[1]、[2]、[3]建成一個時間自動機(jī)的模型，然后模擬利用流水線技術(shù)進(jìn)行消息傳輸，最后我們得到一組數(shù)據(jù)，然后我們對這組數(shù)據(jù)進(jìn)行分析，以此研究采用流水線技術(shù)減少時間通信的可能性。

在第1節(jié)中，我們簡要的描述了這個通信協(xié)議，在第2節(jié)中，我們分析了這個通信協(xié)議，并對流水線傳輸機(jī)制進(jìn)行了建模，在第3節(jié)中，我們對這個系統(tǒng)的屬性進(jìn)行了驗證，在第4節(jié)中，我們進(jìn)行了總結(jié)并提出了以后可以改進(jìn)的可能性。

1 通信協(xié)議的模擬

1.1 通信協(xié)議的簡單描述

這個通信協(xié)議是非常容易理解的，即有一個通信媒介，一個發(fā)送者，一個接受者，消息的長度是固定的并且我們假定這個通信媒介傳送消息是有延遲的。比如傳送消息延遲為delay，那么當(dāng)我們在時刻t的時候發(fā)送一個消息，接受者接受消息應(yīng)該是在t +delay。

1.2 一些通信協(xié)議的假設(shè)

為了便于模擬，我們提出了一些假設(shè)：1）消息傳遞過程中是沒有丟失的；2）接受者接收到消息時，對消息的處理時間為零?；谝陨霞僭O(shè)，當(dāng)消息達(dá)到接受者時，接受者會立即發(fā)送一個成功信號。

2 基于UPPAAL工具的流水線建模

我們采用流水線技術(shù)來模擬發(fā)送，即我們把介質(zhì)發(fā)送的延遲時間分段，其中每段為固定的消息長度，這樣我們就可以得到一些段，這些段就可以組成一個流水線，我們就可以模擬這個流水線進(jìn)行消息傳輸。

在這個模型設(shè)計中，為了便于研究，我們假設(shè)消息長度為5，消息傳遞延遲為消息長度的整數(shù)倍，假設(shè)為15，下面是模型中用到的一些公共變量：

1）int[0,1] buffer[3]={0,0,0} 這是一個消息隊列，用來存放要發(fā)送的消息，此隊列大小為3，其中0代表沒有消息，1代表有消息；

2）int[0,1] medium[3] = {0,0,0} 這是流水線的狀態(tài)標(biāo)志，0代表此段空閑，1代表此段正在處理消息；

3）urgent chan msg_ok 當(dāng)消息達(dá)到接受者時，接受者發(fā)送此信號；

4）urgent chan medium_ok 當(dāng)一個消息傳輸完時，流水線時間自動機(jī)會發(fā)送此信號；

5）urgent chan b_medium1 流水線第一段處理完消息時發(fā)送的信號；

6）urgent chan b_medium2 流水線第二段處理完消息時發(fā)送的信號；

7）urgent chan go消息時間自動機(jī)準(zhǔn)備好要發(fā)送的消息時發(fā)送的信號；

8）int totleTime = 0 發(fā)送所有消息總的時間消耗。

9）int lock = 0防止系統(tǒng)出現(xiàn)死循環(huán)的鎖。

下面是兩個函數(shù)：

2.1 消息模型

消息模型主要實現(xiàn)了以下幾個步驟：1）準(zhǔn)備消息，消息的長度為5；2）消息準(zhǔn)備好時，檢查消息隊列是否滿；3）如果消息隊列滿了，則等待；否則，發(fā)送信號給發(fā)送者。如圖1.4描述了消息模型。

2.2 發(fā)送者模型

發(fā)送者模型主要實現(xiàn)了以下功能：接受消息模型準(zhǔn)備好消息的信號，把消息放到消息隊列中。圖1.5描述了發(fā)送者模型。

2.3 流水線模型

主要實現(xiàn)了以下幾個步驟：1）檢查消息隊列，看有沒有要發(fā)送的消息；2）從消息隊列中拿第一條消息，模擬延遲；3）發(fā)送信號給流水線第二段；4）處理下一條消息；5）流水線第二段接受流水線第一段的消息；6）模擬延遲；7）發(fā)送信號給流水線第三段；8）處理下一個消息；9）流水線第三段接受來自流水線第二段的消息；10）模擬延遲；11）發(fā)送消息給接受者，令其接受消息；12）消息隊列消息數(shù)量減一。如圖1.1，圖1.2，圖1.3所示。

2.4 接受者模型

接受消息，并檢查所有消息是否傳輸完成。圖1.6描述了接受者模型。

2.5 獲取消息傳輸總時間的模型

當(dāng)消息隊列中的消息傳輸完后，我們會得到所有消息傳輸?shù)目倳r間，這個功能有兩個模型組成，分別為observer和loop，其中l(wèi)oop負(fù)責(zé)監(jiān)控消息是否全部完成，observer負(fù)責(zé)計算時間。如圖1.7，1.8所示。

3 系統(tǒng)屬性的分析和驗證

A[] not deadlock 這個系統(tǒng)不會死循環(huán)。

4 結(jié)論

在整個試驗中，我們依次模擬了5條，20條，50條，100條消息傳輸所需的時間，實驗結(jié)果如下圖所示：

消息數(shù) 采用流水線技術(shù)花費時間不采用流水線技術(shù)花費時間 時間減少百分比5 47 75 24.00%20 135 300 55.00%50 314 750 58.13%100 615 1500 59.00%

從以上結(jié)果可以看出，隨著消息數(shù)的增多，減少的時間逐漸增多，最終可以達(dá)到一半以上，這說明在基于通信協(xié)議的消息傳輸過程中，流水線技術(shù)可以大大減少傳輸所需要的時間。后面的實驗我們會考慮兩點：1）傳輸延遲不是固定的；2）傳輸延遲長度可能小于消息長度。

[1]Systems and Software Verification: Model-Checking Techniques and Tools, B.Berard (Author),M.Bidoit (Author),A.Finkel (Author),F.Laroussinie (Author),A.Petit (Author),L.Petrucci (Author),P.Schnoebelen (Author),P.McKenzie.

[2]Temporal Verification of Recactive Systems:Safety,Zohar Manna (Author),Amir Pnueli (Author).

[3]UPPAAL Manual, www.uppaal.com.