Modeling and verification of SCTP Association Management based on Timed Colored Petri Nets
Shengcai Zhang, Dezhi An, Guangli Wu · 2016
The Stream Control Transmission Protocol (SCTP) is a reliable transport protocol to overcome the limitations of TCP and UDP. SCTP is specified informally in Request For Comments (RFC) 4960, but it still lacks a formal specification. Timed Colored Petri Net is suitable to modeling a system from the dynamic perspective, and has the ability to analyze it in a formal way. We present a formal model of SCTP association management by using event-processing modeling approach and Timed CPN. IP network loss and the retransmission mechanism are considered in the model. Through CPN Tools analysis, we find two types of problems with some informal descriptions in RFC 4960.