论文部分内容阅读
流控制传输协议(Stream Control Transmission Protocol,SCTP)是由Internet工程任务组在2000年提出的一个可靠的传输层协议-Request ForComments(RFC)2960。然而经过多年的实现和测试,在RFC2960中已经发现了52处缺陷,且在RFC4460中讨论了这些缺陷和其解决方法。2007年Internet工程任务组修订并发布了新版本的SCTP规范RFC4960,同时废除了RFC2960,但RFC4960仍然缺乏形式化的描述。有色Petri网(CPN)是一种高级的Petri网,非常适合对系统的动态特性建模,并且能够用形式化的方法进行分析。而且有色Petri网支持层次化扩展和时间扩展,这也使其更适于建模复杂的实时系统。因此,本文采用赋时层次CPN对SCTP关联管理的功能和行为进行建模和分析,并取得了如下研究成果:1.基于RFC4960建立了SCTP关联管理的赋时层次CPN模型。该模型非常形象地模拟了SCTP关联管理的过程,并且包括了SCTP的COOKIE机制和超时重发机制。此外,该模型考虑了网络层数据包的失序、延时和丢失,以及SCTP实体育或无重发机制的情况。2.基于本文提出的模型,给出了详尽的分析方案。该方案考虑了两个终端单方或同时建立、释放、异常终止SCTP关联的情况,同时还包括一些混合情况。在此基础上,分析和验证了SCTP关联管理功能正确执行必须满足的预期性质,它们包括:终止性质、无死锁、死活锁、有界性和回归性。3.通过对本文模型的验证和分析,发现了RFC4960中的两类死锁问题。在本文的模型3中发现了两类死锁问题,第一类问题的关键在于在COOKIE ECHOED状态收到了非期望的带有COOKIE-ECHO块的分组,根据RFC4960的5.2.4节规定处理后,导致了SCTP两端都在ESTABLISHED状态,但其传输控制块的验证标志不一致;第二类问题是SCTP的一端在CLOSED状态,而另一端住ESTABLISHED状态,且无法处理收到的带有SHUTDOWN-ACK块的SCTP分组,而对于这种情况在RFC4960中没有任何描述。