Traditional network simulators perform well in evaluating the performance of network protocols but lack the capability of verifying the correctness of protocols. To address this problem, we have extended the J-Sim network simulator with a model checking capability that explores the state space of a network protocol to find an execution that violates a safety invariant. In this paper, we demonstrate the usefulness of this integrated tool for verification and performance evaluation by analyzing two widely used and important network protocols: AODV and directed diffusion. Our analysis discovered a previously unknown bug in the J-Sim implementation of AODV. More importantly, we also discovered a serious deficiency in directed diffusion. To enable the analysis of these fairly complex protocols, we needed to develop protocol-specific search heuristics that guide state-space exploration. We report our findings on discovering good search heuristics to analyze network protocols similar to AODV and directed diffusion. © Springer-Verlag Berlin Heidelberg 2005.
CITATION STYLE
Sobeih, A., Viswanathan, M., Marinov, D., & Hou, J. C. (2005). Finding bugs in network protocols using simulation code and protocol-specific heuristics. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 3785 LNCS, pp. 235–250). https://doi.org/10.1007/11576280_17
Mendeley helps you to discover research relevant for your work.