Show simple item record

dc.contributor.authorBradley, Adam D.en_US
dc.contributor.authorBestavros, Azeren_US
dc.contributor.authorKfoury, Assaf J.en_US
dc.date.accessioned2011-10-20T04:13:42Z
dc.date.available2011-10-20T04:13:42Z
dc.date.issued2003-05-16
dc.identifier.urihttps://hdl.handle.net/2144/1508
dc.description.abstractFormal correctness of complex multi-party network protocols can be difficult to verify. While models of specific fixed compositions of agents can be checked against design constraints, protocols which lend themselves to arbitrarily many compositions of agents-such as the chaining of proxies or the peering of routers-are more difficult to verify because they represent potentially infinite state spaces and may exhibit emergent behaviors which may not materialize under particular fixed compositions. We address this challenge by developing an algebraic approach that enables us to reduce arbitrary compositions of network agents into a behaviorally-equivalent (with respect to some correctness property) compact, canonical representation, which is amenable to mechanical verification. Our approach consists of an algebra and a set of property-preserving rewrite rules for the Canonical Homomorphic Abstraction of Infinite Network protocol compositions (CHAIN). Using CHAIN, an expression over our algebra (i.e., a set of configurations of network protocol agents) can be reduced to another behaviorally-equivalent expression (i.e., a smaller set of configurations). Repeated applications of such rewrite rules produces a canonical expression which can be checked mechanically. We demonstrate our approach by characterizing deadlock-prone configurations of HTTP agents, as well as establishing useful properties of an overlay protocol for scheduling MPEG frames, and of a protocol for Web intra-cache consistency.en_US
dc.description.sponsorshipNational Science Foundation (ANI-9986397, ANI-0095988, CCR-988529, ITR-0113193, ANI-020205294); U.S. Department of Education (GAANN Fellowship)en_US
dc.language.isoen_US
dc.publisherBoston University Computer Science Departmenten_US
dc.relation.ispartofseriesBUCS Technical Reports;BUCS-TR-2003-012
dc.titleSystematic Verification of Safety Properties of Arbitrary Network Protocol Compositions Using CHAINen_US
dc.typeTechnical Reporten_US


This item appears in the following Collection(s)

Show simple item record