For the most recent entries see the Petri Nets Newsletter.

Modelling and analysing the functional behaviour of TCPs connection management procedures.

Billington, Jonathan; Han, Bing

In: International Journal on Software Tools for Technology Transfer (STTT). 2007. URL:

Abstract: The transmission control protocol (TCP) is the most widely used transport protocol in the Internet. It provides a reliable data transfer service to many applications. In this paper, Coloured Petri Nets are used to model TCPs connection management procedures. The model is created to verify TCP's functional correctness (e.g. the absence of deadlocks and livelocks). We discuss different modelling approaches to motivate the approach taken. The paper defines the termination property of TCP's connection management procedures, including the notions of desired and acceptable terminal states. Finally, we analyse TCPs connection management procedures operating over re-ordering non-lossy and lossy channels. This is done incrementally and considers 11 different configurations. The analysis provides some insights into TCP's behaviour where in certain circumstances the protocol fails to establish or terminate successfully.

Do you need a refined search? Try our search engine which allows complex field-based queries.

Back to the Petri Nets Bibliography