Abstract: We present a new algorithm for automatic test generation for multicast routing. Our algorithm processes a nite state machine (FSM) model of the protocol and uses a mix of forward and backward search techniques to generate the tests. The output tests include a set of topologies, protocol events and network failures, that lead to violation of protocol correctness and behavioral requirements. We target protocol robustness in speci c, and do not attempt to verify other properties in this paper. We apply our method to a multicast routing protocol; PIM-DM, and investigate its behavior in the presence of selective packet loss on LANs and router crashes. Our study unveils several robustness violations in PIM-DM, for which we suggest xes with the aid of the presented algorithm.
Ahmed Helmy, Deborah Estrin, Sandeep K. S. Gupta