Bounded Model Checking of Network Protocols in Network Simulators by Exploiting Protocol-Specific Heuristics

Network simulators perform well in evaluating the performance of network protocols, but lack the capability of verifying their correctness. In order to address this lacuna, we have extended the J- Sim network simulator with a model checking capability to explore the state space of a network protocol to find either an execution where a safety invariant is violated or an exceution where the satisfaction of an eventuality property is witnessed. 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: Ad-Hoc On-Demand Distance Vector (AODV) routing protocol and directed diffucion protocol. Our analysis discovered a previously unknown bug in the J-Sim implementation of AODV, and a design flaw in directed diffusion, illustrating that our tool can uncover both bugs in the implementation and design of a protocol. To enable the analysis of these fairly complex protocols, we needed to develop search heuristics to explore the state space. We report our preliminary findings on discovering good search heuristics to analyze routing protocols