HTTP Verification

The popular HTTP/1.1 protocol was first publicly specified in RFC2068, published in early 1997. Over the following years, a number of deficiencies and ambiguities were found in the specification, largely either by way of thought experiments or complications with implementations. This collective experience fed into the formulation of a new revised specification document, RFC2616, published in the summer of 1999.

We propose that a more rigorous analysis of protocol features in the design phase can help to minimize the appearance of design errors such as those found in RFC2068, and can also significantly shorten the revision cycle and improve the strength of interoperability and back/forward-compatibility claims. As a case study to illustrate this proposal, we used the SPIN modeling tool from Bell Labs to model the expect/continue behavior of HTTP protocol agents (clients, proxies, and servers) to formalize HTTP agent behavior and identify both well-known and less-known potential deadlock conditions.

Code

You may use this code for academic and research purposes only. Redistribution is prohibited.

Publications