计算机网络技术是当今发展最迅速的计算机技术之一,而保证网络稳定可靠运行的关键是计算机网络协议。协议是计算机网络的灵魂,协议设计、开发复杂性的增加导致了协议工程技术的出现。协议工程用形式化的方法描述在协议严格的设计和维护中的各个活动。形式描述技术是整个协议工程的关键所在,它不但能够提供无二义性的描述,而且能够对描述进行形式分析和细化。目前已有多种成熟的形式描述技术,建立在异步并发概念上的Petri网是应用较广的一种形式描述技术。本文主要对Petri网技术及其在网络协议中的应用进行研究。首先,简要介绍了形式描述技术在协议工程中的应用范围,Petri网技术的基本概念和发展状况。其次,针对随机Petri网在系统性能分析时其状态空间随着网规模的增大而指数性的增长,造成求解稳定状态概率的复杂性这一问题,提出了一种随机着色Petri网(SCPN),并给出了其系统性能分析的方法。在对TCP协议作详细的非形式化分析的基础之上,利用有色Petri网对其连接建立模块和数据传输模块建立了形式化模型,并通过有色Petri工具CPN Tool进行模型的仿真,得到了模型的可达树。在系统地总结了Petri网的性质基础上,通过Petri网的可达树的分析方法,对模型的性质进行了分析与验证,从而确定了TCP协议的逻辑正确性。最后通过所提出的随机着色Petri网对TCP协议的数据传输模块做了定量的性能分析。这些研究工作对于深入理解TCP协议、分析改进协议和具体实现协议都起着不可或缺的重要作用。