Abstract
The Stream Control Transmission Protoco1 (SCTP) is a reliable transport protocol to tackle the limitations of TCP and UDP. SCTP is specified informally in Request For Comments (RFC) 2960, but it still lacks a formal specification. Coloured Petri Net (CPN) 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 using the CPN. The model is used to examine some properties of SCTP and to check the internal consistency of RFC 2960. Through CPN Tools analysis, we find a problem with some informal descriptions in RFC 2960 and solve it by modifying our original CPN model.