计算机工程 ›› 2011, Vol. 37 ›› Issue (18): 77-80.doi: 10.3969/j.issn.1000-3428.2011.18.026

• 网络与通信 • 上一篇    下一篇

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

何中阳,李 鸥,杨白薇,刘 洋   

  1. (解放军信息工程大学信息工程学院,郑州 450002)
  • 收稿日期:2011-02-14 出版日期:2011-09-20 发布日期:2011-09-20
  • 作者简介:何中阳(1985-),男,硕士研究生,主研方向:网络协议分析;李 鸥,教授、博士生导师;杨白薇,副教授;刘 洋, 博士研究生
  • 基金项目:
    国家“863”计划基金资助项目(2009AA01Z207)

Formal Description of TCP Protocol Based on Timed Colored Petri Net

HE Zhong-yang, LI Ou, YANG Bai-wei, LIU Yang   

  1. (Institute of Information Engineering, PLA Information Engineering University, Zhengzhou 450002, China)
  • Received:2011-02-14 Online:2011-09-20 Published:2011-09-20

摘要: 提出一种基于赋时着色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

中图分类号: