基于TCPN的TCP协议形式化描述  

Formal Description of TCP Protocol Based on Timed Colored Petri Net

作　　者：何中阳[1] 李鸥[1] 杨白薇[1] 刘洋[1] 

机构地区：[1]解放军信息工程大学信息工程学院,郑州450002

出　　处：《计算机工程》2011年第18期77-80,共4页Computer Engineering

基　　金：国家"863"计划基金资助项目(2009AA01Z207)

摘　　要：提出一种基于赋时着色Petri网模型的TCP协议形式化描述方法。采用序号、确认号和数据3个参数对TCP报文进行更准确的描述,引入时间参数以便进行协议的性能评估,加入超时重传、流量控制和确认信息捎带传输等机制,使模型更符合协议的实际运行规程。通过CPN Tools对模型进行动态模拟,仿真结果证明了该模型的正确性。This paper proposes a formal description method of TCP protocol based on Timed Colored Petri Net（TCPN）.Three parameters of sequence number,confirmation number and data unit are adopted to describe the packet more accurately.A time parameter is introduced to evaluate the performance of the protocol.The model is closer to the actual running order agreement because of timeout retransmission,flow control and validation data piggyback transmission.CPN Tools is used for modeling dynamic simulation,and its result proves the correctness of the model.

关 键 词：TCP协议 赋时着色PETRI网 形式化描述 有界性 活性 

分 类 号：TP393[自动化与计算机技术—计算机应用技术]