基于有色Petri網的TCP協議建模與分析

【摘要】在介紹TCP協議基礎上，根據有色Petri 網的建模方法和工具CPN Tools，對TCP協議的連接建立模塊建立了有色Petri網模型，得到模型的可達樹，通過可達樹的方法，驗證了所建模型的邏輯正確性。

【關鍵詞】TCP 協議；有色Petri網；形式化描述；可達樹

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

一、TCP協議連接的建立過程

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

二、CPN模型

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

三、模型驗證與分析

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

本文利用有色Petri網的建模的方法和工具CPN Tool，建立了TCP協議的連接建立過程的有色Petri網模型，得到模型的了可達樹，通過可達樹的方法，驗證了所建模型的有界性、安全性、活性、可逆性等性質。從而證明了所構造的形式化模型的正確性，同時也驗證了協議的邏輯正確性。

參 考 文 獻

[1]周必水，酈泓．有色Petri網在通信協議中的應用[J]．系統仿真學報．2003，15（8）：112～114

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

[3]胡瑜．基于有色Petri網理論的并行自動測試系統建模研究[J]．電子科技大學學報．2003：47～53