An Initial Coloured Petri Net Model of the Hypertext Transfer Protocol Operating over the Transmission Control Protocol.

Transfer of resources in the World Wide Web is achieved by using the Hypertext Transfer Protocol (HTTP). The most widely used version of HTTP in the Internet is HTTP/1.1 published as Request for Comments 2616. HTTP/1.1 is currently undergoing revision and is being restructured into a 7 part document by the Internet Engineering Task Force. Part 1 includes a description of the operation of HTTP over reliable transport connections, and is currently a relatively mature Internet Draft. It is therefore timely to subject these revisions to a rigorous analysis using formal techniques. This paper presents an initial Coloured Petri Net model of HTTP operating over transport connections provided by the Transmission Control Protocol (TCP). This requires modelling HTTP entities, the transport service provided by TCP, and their interactions. The design of the model, including its underlying assumptions and validation, is discussed and reachability analysis results are reported. Insights are gained into: the size of the state space as a function of web requests; and the dimensioning of buffers required in HTTP entities.