基于赋时层次着色Petri网的流控制传输协议连接建模与分析

Modeling and Analysis of Stream Control Transmission Protocol Association Based on Hierarchical Timed Colored Petri Nets

流控制传输协议(stream control transmission protocol,SCTP)是一种可靠的传输协议,2007年Internet工程任务组修订了52处缺陷并发布了SCTP新规范RFC4960,但仍缺乏形式化的描述和验证。赋时层次着色Petri网适用于从动态角度对复杂系统进行建模,并能够用形式化的方法进行验证分析。因此,采用基于事件和基于状态的建模方法,提出了SCTP连接的赋时层次着色Petri网模型,该模型考虑了网络时延和丢失以及重传机制。通过CPN Tools分析,验证了SCTP连接过程的预期性质,并在RFC4960中描述的SCTP连接过程中发现了两类死锁问题。

Stream control transmission protocol(SCTP)is a reliable transmission protocol.The Internet Engineering Task Force revised 52 defects and issued a new SCTP specification RFC4960 in 2007,but SCTP still lacked formal description and verification.Hierarchical timed colored petri nets(HTCPN)are suitable for modeling complex systems from a dynamic perspective,and can be used for formal method of verification analysis.Therefore,a HTCPN-based model for SCTP association was proposed by using event-based and state-based modeling methods.The network delay,loss and retransmission mechanisms were considered in the model.Through CPN Tools analysis,the expected nature of SCTP association was verified,and two types of deadlock problems were discovered during the SCTP association process described in RFC4960.