（甘肅政法學院 計算機科學學院，甘肅 蘭州， 730070）
摘要：本文利用著色Petri網的建模的方法和工具CPN Tool，建立了TCP協議數據傳輸過程的著色Petri網模型，得到模型的了可達樹，通過可達樹的方法對協議模型的性質進行了分析與驗證，從而確定了TCP協議數據傳輸過程的邏輯正確性。最后通過隨機著色Petri網對TCP 協議數據傳輸過程做了定量的性能分析。
關鍵字：TCP協議，隨機著色Petri網，性能分析
Verification and Performance Analysis TCP Protocol Data Transition Based on Stochastic Colored Petri Net
Zhang Shengcai
（Department of Computer Science ,Gansu institute of political science and law, Lanzhou Gansu, 730070,China；）
Abstract：Colored Petri Nets and CPN tools are used to build a formal model of TCP data transition model. We get the reachability tree of the model, and validate the logic correctness of TCP data transition by the method - Reachability Tree of Petri Net. Lastly, we use Stochastic Colored Petri Nets to make a quantitative performance analysis about the model of the TCP data transition.
Keywords：TCP Protocol, Stochastic Colored Petri Nets, Performance Analysis
參考文獻：
[1] Behrouz A.Forouzan, Sophia Chung Fegan. TCP/IP協議簇[M].清華大學出版社.2006.5
[2] 古天龍，蔡國永. 網絡協議的形式化分析與設計.北京:電子工業出版社.2003,6
[3] 李艷，彭熙，肖德寶.計算機網絡通信協議驗證技術的研究[J].計算機工程,2002,28(11):251～252.
[4] 龔正虎. 計算機網絡協議工程.長沙:國防科技大學出版社.1993,12
[5] 王繼曾，張彥龍，羅靖宇.一種隨機著色Petri網及模型的性能分析[J].計算機應用. 2008，28（2）：292～293.
[6] 林 闖. 隨機Petri網和系統性能評價.北京:清華大學出版社.2005.4
作者簡介：
張生財(1982- ) 男，碩士，講師，研究方向：協議分析，網絡安全。
