Parameterised Coloured Petri Net Channel Models

Computer protocols operate over communication channels with varying properties. Channel characteristics include order of delivery (e.g. first-in first-out (FIFO)), whether it is lossy or not, and capacity. Important Internet protocols, such as the Transmission Control Protocol (TCP) and the Datagram Congestion Control Protocol (DCCP), are designed to operate over channels which can duplicate, reorder and lose packets. It is important to be able to analyse protocol behaviour incrementally, to ensure that channel imperfections, such as reordering or loss, do not hide protocol errors such as unspecified receptions. In order to analyse protocols progressively using FIFO channels without (and then with) loss and then reordering channels without (and then with) loss, this paper proposes Coloured Petri Net (CPN) models which combine the FIFO and reordering behaviour (with or without loss) in a way that reduces maintenance effort as the protocol evolves, and facilitates analysis. The model also includes an arbitrary channel capacity limit, including no limit. We firstly present a simple parameterised model. Unfortunately, this model is not able to be simulated by current CPN support tools. We then modify the model to allow it to be executed in tools such as CPN Tools. The paper discusses the way in which the parameterised channel model is embedded into a protocol specification. Having a combined FIFO/reordering and possibly lossy model was useful in the case of DCCP as we tracked its development by the Internet Engineering Task Force. This paper discusses selected results of the incremental analysis of DCCP’s connection management procedures, exploiting the parameterised channel model.