Author: Ahmed A-G Helmy
Abstract:
The recent growth and increased heterogeneity of the Internet has increased the complexity of network protocol design and testing. In addition, the advent of multipoint (multicast-based) applications has introduced new challenges that are qualitatively different in nature than the traditional point-to-point protocols. Multipoint applications typically involve a group of participants simultaneously, and hence are inherently more complex. As more multipoint protocols are coming to life, the need for systematic and automated methods to study and evaluate such protocols is becoming more apparent. Such methods aim to expedite the protocol development cycle and improve protocol robustness and performance.
Related work on automatic protocol verification has usually targeted protocol correctness under idealized conditions. This study targets protocol robustness and performance in the presence of lower level network failures. In addition, previous work does not address multicast protocols or topology synthesis, both of which are addressed in this study.
In this dissertation a new methodology for developing systematic and
automatic test generation algorithms for multipoint protocols is
proposed. These algorithms attempt to synthesize network topologies
and sequences of events that stress the protocol's correctness or
performance. This problem can be viewed as a domain-specific search
problem that suffers from the state space explosion problem. One goal
of this research is to circumvent the state space explosion problem
utilizing knowledge of network and fault modeling, and multipoint
protocols.
Several approaches are investigated in this dissertation,
including approaches based on heuristic, forward and backward search
techniques. Focus is given on two search algorithms based on an
extended finite state machine (FSM) model of the protocol.
The first algorithm uses forward search to perform reduced
reachability analysis. Using domain-specific information for multicast
routing over LANs, the algorithm complexity is reduced from
exponential to polynomial in the number of routers. This approach,
however, does not fully automate topology synthesis. The second
algorithm; the fault-oriented test generation, automates topology
synthesis by utilizing backward search techniques. This algorithm uses
backtracking to generate event sequences instead of searching forward
from initial states.
Using these algorithms, studies are conducted for correctness of multicast routing protocols over LANs. These algorithms are further extended to study end-to-end multipoint protocols, by incorporating delay semantics and performance criteria. The notion of a virtual LAN is introduced to represent delays of the underlying multicast distribution tree. As a case study, the method is used to generate worst and best case scenarios for the timer suppression mechanism employed in several Internet multipoint protocols.