Modeling And Analysis Of SCTP Association Management Using Colored Petri Net

The Stream Control Transmission Protocol(SCTP) is a reliable transport protocol originally specified by the Internet Engineering Task Force(IETF) in 2000.However,after years of implementing and testing,defects and errors in Request For Comments(RFC) 2960 were reported and later fixed and discussed in RFC 4460.IETF revised the SCTP specification and in 2007 published RFC 4960,which replaces RFC 2960,but RFC4960 still lacks a formal specification.Colored Petri Net(CPN) is a high-level Petri net.CPN is suitable to modeling a system from the dynamic perspective,and has the ability to analyze it in a formal way.Moreover,CPN allows models to be built with a hierarchical structuring mechanism and a time concept.Therefore it is suitable to modeling a complex real-time system.Therefore,the function and behaviors of SCTP association management are modeled and analyzed by using the Hierarchical Timed Colored Petri Net(HTCPN).The main results are as follows:1.Basis on RFC4960,we present a formal model of SCTP association management using the Hierarchical Timed Colored Petri Net(HTCPN).The model visually simulates the process of association management,and the model includes the cookie mechanism of SCTP and the timeout retransmission of SCTP. Moreover,in the model the IP network may re-order,delay and lose packets,and the retransmission mechanism of SCTP can be included or not be included.2.Basis on the model in this thesis,the detailed analysis schemes of the model are presented.We investigate both the client-server and simultaneous attempting to establish,shut and abort the association,and some mixed case.On this basis,we analyze and validate a set of desired properties that the functional correctness of SCTP association management must satisfy.They include: termination,absence of deadlocks,absence of livelocks,boundedness and home.3.Through the verification and analysis of the model in this thesis,two types of deadlock problem concerning SCTP association management are detected in RFC4960.There are two types of deadlock in the model 3 of this thesis.In the first type,the key of the problem is that one endpoint receives the unexpected SCTP packet with COOKIE-ECHO chunk in COOKIE_ECHOED state,and deals with the packet according to the section 5.2.4 of RFC4960. Therefore the both endpoints are in ESTABLISHED states but the verification tags in both Transmission Control Blocks do not match.The second type deadlock is that one of the SCTP endpoint can terminate in CLOSED but the other in ESTABLISHED and can not handle the received SCTP packet with SHUTDOWN-ACK chunk.There are no descriptions in RFC4960 for this case.