@inproceedings{97d1a6c33e2f4214a67c637dc49eed54,
title = "Finding bugs in network protocols using simulation code and protocol-specific heuristics",
abstract = "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.",
author = "Ahmed Sobeih and Mahesh Viswanathan and Darko Marinov and Hou, {Jennifer C.}",
year = "2005",
doi = "10.1007/11576280_17",
language = "English (US)",
isbn = "3540297979",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
pages = "235--250",
booktitle = "Formal Methods and Software Engineering - 7th International Conference on Formal Engineering Methods, ICFEM 2005, Proceedings",
note = "7th International Conference on Formal Engineering Methods, ICFEM 2005 ; Conference date: 01-11-2005 Through 04-11-2005",
}