摘要： 提出一种基于赋时着色Petri网模型的TCP协议形式化描述方法。采用序号、确认号和数据3个参数对TCP报文进行更准确的描述，引入时间参数以便进行协议的性能评估，加入超时重传、流量控制和确认信息捎带传输等机制，使模型更符合协议的实际运行规程。通过CPN Tools对模型进行动态模拟，仿真结果证明了该模型的正确性。
关键词:
TCP协议,
赋时着色Petri网,
形式化描述,
有界性,
活性
Abstract: 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.
Key words:
TCP protocol,
Timed Colored Petri Net(TCPN),
formal description,
boundedness,
liveness
中图分类号:
何中阳, 李鸥, 杨白薇, 刘洋. 基于TCPN的TCP协议形式化描述[J]. 计算机工程, 2011, 37(18): 77-80.
HE Zhong-Yang, LI Ou, YANG Bai-Wei, LIU Xiang. Formal Description of TCP Protocol Based on Timed Colored Petri Net[J]. Computer Engineering, 2011, 37(18): 77-80.