In: Proc. of the 4th International Network Conference, pages 63-70. July 2004. University of Plymouth, UK.
Abstract: A new protocol in the TCP/UDP family, the Datagram Congestion Control Protocol (DCCP), is designed to control congestion when considering delay sensitive applications. We believe it is useful to formally verify DCCP's connection management procedures before they are implemented. We use Coloured Petri Nets (CPNs) to model these procedures. The CPN model is analyzed using reachability analysis which reveals an undesirable terminal state in the connection establishment procedure.
Keywords: DCCP; Formal Methods; Coloured Petri Nets; Reachability analysis.