Title: Validating Arbitrarily Large Network Protocol Compositions with Finite Computation
Authors: Adam D. Bradley, Azer Bestavros, and Assaf J. Kfoury
Date: November 1, 2002
Abstract:
Formal tools like finite-state model checkers have proven useful in
verifying the correctness of systems of bounded size and for hardening
single system components against arbitrary inputs. However,
conventional applications of these techniques are not well suited to
characterizing emergent behaviors of large compositions of processes.
In this paper, we present a methodology by which arbitrarily large
compositions of components can, if sufficient conditions are proven
concerning properties of small compositions, be modeled and completely
verified by performing formal verifications upon only a finite set of
compositions. The sufficient conditions take the form of reductions,
which are claims that particular sequences of components will be
causally indistinguishable from other shorter sequences of components.
We show how this methodology can be applied to a variety of network
protocol applications, including two features of the HTTP protocol, a
simple active networking applet, and a proposed web cache consistency
algorithm. We also doing discuss its applicability to framing protocol
design goals and to representing systems which employ non-model-checking
verification methodologies. Finally, we briefly discuss how we hope to
broaden this methodology to more general topological compositions of
network applications.
Keywords: Protocol Verification, Formal Methods, Model Checking,
Language Reduction, Protocol Design