基于Uppaal的通信協(xié)議消息傳輸?shù)牧魉€技術(shù)的建模與分析

王長(zhǎng)青

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

0 引言

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

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

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

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

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

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

為了便于模擬，我們提出了一些假設(shè)：1）消息傳遞過程中是沒有丟失的；2）接受者接收到消息時(shí)，對(duì)消息的處理時(shí)間為零。基于以上假設(shè)，當(dāng)消息達(dá)到接受者時(shí)，接受者會(huì)立即發(fā)送一個(gè)成功信號(hào)。

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

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

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

1）int[0,1] buffer[3]={0,0,0} 這是一個(gè)消息隊(duì)列，用來存放要發(fā)送的消息，此隊(duì)列大小為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á)到接受者時(shí)，接受者發(fā)送此信號(hào)；

4）urgent chan medium_ok 當(dāng)一個(gè)消息傳輸完時(shí)，流水線時(shí)間自動(dòng)機(jī)會(huì)發(fā)送此信號(hào)；

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

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

7）urgent chan go消息時(shí)間自動(dòng)機(jī)準(zhǔn)備好要發(fā)送的消息時(shí)發(fā)送的信號(hào)；

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

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

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

2.1 消息模型

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

2.2 發(fā)送者模型

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

2.3 流水線模型

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

2.4 接受者模型

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

2.5 獲取消息傳輸總時(shí)間的模型

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

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

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

4 結(jié)論

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

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

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

[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.