【摘要】在介紹TCP協(xié)議基礎(chǔ)上，根據(jù)有色Petri 網(wǎng)的建模方法和工具CPN Tools，對(duì)TCP協(xié)議的連接建立模塊建立了有色Petri網(wǎng)模型，得到模型的可達(dá)樹，通過可達(dá)樹的方法，驗(yàn)證了所建模型的邏輯正確性。

【關(guān)鍵詞】TCP 協(xié)議；有色Petri網(wǎng)；形式化描述；可達(dá)樹

隨著數(shù)據(jù)通信和網(wǎng)絡(luò)的發(fā)展，現(xiàn)在TCP/IP（Transfer Control Protocol/Internet Protocol）協(xié)議簇成為占主導(dǎo)地位的網(wǎng)絡(luò)體系結(jié)構(gòu)，被廣泛的使用。有色Petri網(wǎng)（Colored Petri Net，CPN）是由丹麥的Jensen Kurt于1981年在Petri網(wǎng)基礎(chǔ)上定義的一種具有層次性的高級(jí)Petri網(wǎng)。利用在計(jì)算機(jī)上開發(fā)的CPN的建模分析工具──CPN Tools，可以建立描述系統(tǒng)的CPN靜態(tài)模型，并對(duì)系統(tǒng)模型的動(dòng)態(tài)行為進(jìn)行仿真，分析系統(tǒng)的分布、并發(fā)、同步、異步等特性，以及建立系統(tǒng)模型的狀態(tài)空間并分析系統(tǒng)的活性問題、可達(dá)性問題等。由于CPN具有嚴(yán)格的網(wǎng)理論形式化的數(shù)學(xué)描述、上述的特性以及建模工具提供的仿真分析功能，因此在網(wǎng)絡(luò)通信協(xié)議的驗(yàn)證和分析上得到了廣泛的應(yīng)用。

一、TCP協(xié)議連接的建立過程

TCP是一個(gè)可靠的，面向連接的，端到端的傳輸協(xié)議，它提供了具有流量控制的可靠的數(shù)據(jù)傳輸。TCP的連接建立稱為“三次握手”。（1）客戶發(fā)送第一個(gè)報(bào)文段，SYN報(bào)文段，在這個(gè)報(bào)文段中只有SYN標(biāo)志置1，這個(gè)報(bào)文段的作用是使序號(hào)同步。客戶端選擇一個(gè)隨機(jī)數(shù)作為第一序號(hào)，并把這個(gè)序號(hào)發(fā)給服務(wù)器。注意SYN報(bào)文段是一控制報(bào)文段，不攜帶任何數(shù)據(jù)但它消耗一個(gè)序列號(hào)。（2）服務(wù)器發(fā)送第二個(gè)報(bào)文段，即SYN+ACK報(bào)文段，其中有兩個(gè)標(biāo)志置為1這個(gè)報(bào)文段有兩個(gè)目的，一個(gè)是使用SYN同步初始序號(hào)，另一個(gè)是服務(wù)器使用ACK標(biāo)志確認(rèn)已經(jīng)從客戶端收到的SYN報(bào)文段，同時(shí)給出期望從客戶端收到的下一個(gè)序號(hào)。服務(wù)器還必須定義客戶端要使用的接收窗口（rwnd），這就實(shí)現(xiàn)了TCP的流量控制。（3）客戶端發(fā)送第三個(gè)報(bào)文段。這僅僅是一個(gè)ACK報(bào)文段。它使用ACK標(biāo)志和確認(rèn)號(hào)字段來確認(rèn)收到了第二個(gè)報(bào)文。注意這個(gè)報(bào)文段的序號(hào)和SYN的報(bào)文段使用的序號(hào)一樣，這個(gè)ACK報(bào)文段不消耗任何序號(hào)。客戶還必須定義服務(wù)窗口值。在某些情況下第三個(gè)報(bào)文段可以攜帶客戶端的第一個(gè)數(shù)據(jù)塊，在這種情況下第三個(gè)報(bào)文段必須有一個(gè)新的序號(hào)來表示數(shù)據(jù)源的第一個(gè)自己的編號(hào)。一般的來說，第三個(gè)報(bào)文段不攜帶數(shù)據(jù)的，因而不消耗序號(hào)。

二、CPN模型

在利用CPN Tool建立具體模型之前，先對(duì)模型中各庫所和變遷，以及顏色類型，變量做一說明。當(dāng)P1，P2，P4，P7中有標(biāo)識(shí)的時(shí)候，即發(fā)送端主動(dòng)打開準(zhǔn)備發(fā)送連接請(qǐng)求和接受端被動(dòng)打開監(jiān)聽，發(fā)送第一個(gè)請(qǐng)求報(bào)文，其序號(hào)用變量n1綁定，在接收端收到這個(gè)請(qǐng)求信息的時(shí)候把n1加1作為服務(wù)器想從客戶端得到下一報(bào)文段的序號(hào)，同時(shí)和自己的初始序號(hào)一起組成確認(rèn)報(bào)文段序列，用（n3，n2）來綁定。當(dāng)客戶端接到這個(gè)報(bào)文的時(shí)候進(jìn)行檢查，如果n3=n1+1，說明得到服務(wù)器確認(rèn)報(bào)文安全，發(fā)送客戶確認(rèn)報(bào)文，用（n3，n4）綁定，同時(shí)把n1作為數(shù)據(jù)傳輸?shù)某跏夹蛱?hào)。如果n3不等于n1+1，客戶端重新發(fā)送連接請(qǐng)求。在服務(wù)器端收到客戶端確認(rèn)報(bào)文的時(shí)進(jìn)行檢查，如果n4=n2+1，把n2作為接收數(shù)據(jù)的初始編號(hào)，等待接收數(shù)據(jù)，否則繼續(xù)監(jiān)聽。在初始標(biāo)識(shí)下最后到的P8和P11中有標(biāo)記，說明連接建立成功。

三、模型驗(yàn)證與分析

Petri網(wǎng)的模型驗(yàn)證方法有兩種：可達(dá)樹（Reachability Tree）方法和線性代數(shù)（Matrix Equations）方法。在初始標(biāo)識(shí)下通過工具CPN Tool我們可以得到連接的CPN模型的可達(dá)樹。（1）可達(dá)樹各結(jié)點(diǎn)中庫所包含的標(biāo)記不超過兩個(gè)，且當(dāng)庫所包含兩個(gè)標(biāo)識(shí)時(shí)標(biāo)記顏色各不相同，因此TCP協(xié)議連接建立的有色Petri網(wǎng)模型是安全的，有界的。（2）可達(dá)樹中各變遷至少引發(fā)一次，沒有從不引發(fā)的變遷。樹中每個(gè)標(biāo)號(hào)有后繼標(biāo)號(hào)，即每個(gè)標(biāo)號(hào)都是可以引發(fā)的。對(duì)于可達(dá)集R（M0），每一標(biāo)號(hào)都有一條從根到的變遷路徑，即。根據(jù)活性的定義，可知該模型是活的，不會(huì)有死鎖發(fā)生。（3）可達(dá)樹中不存在無用的循環(huán)，其中兩個(gè)循環(huán)是處理發(fā)送端和接收端所接受的報(bào)文序號(hào)是否匹配。（4）可達(dá)樹中可達(dá)狀態(tài)M3經(jīng)變遷T3可回到初始狀態(tài)，所以該CPN模型是可逆的。保證了協(xié)議周期性行為的實(shí)現(xiàn)，即能夠重復(fù)執(zhí)行請(qǐng)求連接的功能。

本文利用有色Petri網(wǎng)的建模的方法和工具CPN Tool，建立了TCP協(xié)議的連接建立過程的有色Petri網(wǎng)模型，得到模型的了可達(dá)樹，通過可達(dá)樹的方法，驗(yàn)證了所建模型的有界性、安全性、活性、可逆性等性質(zhì)。從而證明了所構(gòu)造的形式化模型的正確性，同時(shí)也驗(yàn)證了協(xié)議的邏輯正確性。

參 考 文 獻(xiàn)

[1]周必水，酈泓．有色Petri網(wǎng)在通信協(xié)議中的應(yīng)用[J]．系統(tǒng)仿真學(xué)報(bào)．2003，15（8）：112～114

[2]Behrouz A.Forouzan，Sophia Chung Fegan.TCP/IP協(xié)議簇[M]．清華大學(xué)出版社，2006（5）

[3]胡瑜．基于有色Petri網(wǎng)理論的并行自動(dòng)測(cè)試系統(tǒng)建模研究[J]．電子科技大學(xué)學(xué)報(bào)．2003：47～53