In: Proc of the 14th IEEE International Symposium on Modelling, Analysis, and Simulation of Computer and Telecommunication Systems (MASCOTS-06), pages 345-352. 11-13 September 2006.
Abstract: This paper investigates the connection establishment procedures of the Datagram Congestion Control Protocol (DCCP) when sequence numbers wrap. A formal executable specification of DCCP connection management is obtained using Coloured Petri Nets. The model includes the synchronization procedure, sequence number wrapping and the algorithm for extending short sequence numbers. We discover that during connection establishment if sequence numbers wrap, it is possible that the attempt to set up the connection fails.
Keywords: DCCP, Formal Methods, Coloured Petri Nets, State Space Methods.