Files in this item



application/pdfBounded Model C ... ol-Specific Heuristics.pdf (185kB)
(no description provided)PDF


Title:Bounded Model Checking of Network Protocols in Network Simulators by Exploiting Protocol-Specific Heuristics
Author(s):Sobeih, Ahmed A.; Viswanathan, Mahesh; Hou, Jennifer C.
Abstract: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.
Issue Date:2005-04
Genre:Technical Report
Other Identifier(s):UIUCDCS-R-2005-2547
Rights Information:You are granted permission for the non-commercial reproduction, distribution, display, and performance of this technical report in any format, BUT this permission is only for a period of 45 (forty-five) days from the most recent time that you verified that this technical report is still available from the University of Illinois at Urbana-Champaign Computer Science Department under terms that include this permission. All other rights are reserved by the author(s).
Date Available in IDEALS:2009-04-17

This item appears in the following Collection(s)

Item Statistics