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

Sobeih, Ahmed A.; Viswanathan, Mahesh; Hou, Jennifer C.

Permalink

https://hdl.handle.net/2142/11002 Copy

Description

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.

Issue Date

2005-04

Keyword(s)

• networking
• heuristics

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.

Type of Resource

text

Permalink

http://hdl.handle.net/2142/11002

Copyright and License 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).

Owning Collections