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
- Source Code for most of the agents discussed in the WCW2002 paper
You may use this code for academic and research purposes only. Redistribution is prohibited.
Publications
[thesis] Adam D. Bradley, A Type-Disciplined Approach to Developing Resources and Applications for the World-Wide Web, Ph.D. Dissertation, Boston University, Boston, MA, 2004.
[chain:icnp2003] Adam D. Bradley and Azer Bestavros and Assaf J. Kfoury, Systematic Verification of Safety Properties of Arbitrary Network Protocol Compositions Using CHAIN, IEEE International Conference on Network Protocols (ICNP), Atlanta, GA, 2003. [PDF] [PS.gz]
- Also appeared as: [chain:tr]
[chain:tr] Adam D. Bradley and Azer Bestavros and Assaf J. Kfoury, Systematic Verification of Safety Properties of Arbitrary Network Protocol Compositions Using CHAIN, BU Computer Science Technical Report, BUCS-TR-2003-012, Boston, MA, 2003. [PDF] [PS.gz]
- Also appeared as: [chain:icnp]
[infinitemodel:tr] Adam D. Bradley and Azer Bestavros and Assaf J. Kfoury, Validating Arbitrarily Large Network Protocol Compositions with Finite Computation, BU Computer Science Technical Report, BUCS-TR-2002-030, Boston, MA, 2002. [PDF] [PS]
[httpverify:wcw2002] Adam D. Bradley and Azer Bestavros and Assaf J. Kfoury, Safe Composition of Web Communication Protocols for Extensible Edge Services, 7th International Workshop on Web Content Caching and Distribution (WCW), Boulder, CO, 2002. [PDF] [PS.gz] [PPT]
- Extended version: [httpverify:tr]
[httpverify:tr] Adam D. Bradley and Azer Bestavros and Assaf J. Kfoury, Safe Composition of Web Communication Protocols for Extensible Edge Services, BU Computer Science Technical Report, BUCS-TR-2002-017, Boston, MA, 2002. [PS] [PDF]
- Extended version of: [httpverify:wcw2002]

