Validating DCCP Simultaneous Feature Negotiation Procedure

摘要

This paper investigates the feature negotiation procedure of the Datagram Congestion Control Protocol (DCCP) in RFC 4340 using Coloured Petri Nets (CPNs). After obtaining a formal executable CPN model of DCCP feature negotiation, we analyse it using state spaces. The experimental result reveals that simultaneous negotiation may be incorrect and broken on even a lossless FIFO channel. In the undesired terminal states, the confirmed feature values of the client and the server do not match. To fix this problem we suggest two solutions. Firstly, sending a Change option when an endpoint changes its preference. Secondly, an endpoint in STABLE does not discard non-reordered Confirm options. We have applied our suggested changes to the constructed CPN models. The formal verification of the revised models shows that the undesired terminal states have been eliminated.