Incorporating Bounded Model Checking in Network Simulation: Theory, Implementation and Evaluation

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

Permalink

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

Description

Title

Incorporating Bounded Model Checking in Network Simulation: Theory, Implementation and Evaluation

Author(s)

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

Issue Date

2004-07

Keyword(s)

networking

Abstract

Existing network simulators perform reasonably well in evaluating the performance of network protocols, but lack the capability of verifying the correctness of network protocols. In this paper, we present our ongoing research on extending J-Sim --- an open-source, component-based compositional network simulation environment --- with the model checking capability to explore the state space created by a network protocol in order to find a violation of a desirable safety property and/or to find a witness for a desirable liveness property if any exists. This paper shows how J-Sim can model-check the Ad-Hoc On-Demand Distance Vector (AODV) routing protocol, a fairly complex network protocol with thousands of lines of Java code. We also exploit protocol-specific properties in the process of exploring the state space, to reduce the size of the state space and to guide the (best-first) search towards paths that can potentially locate violations/witnesses in less time. The experimental results presented in this paper show that a best-first search strategy can provide several orders of magnitude reduction in both the time and space overheads needed to find violations/witnesses.

Type of Resource

text

Permalink

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

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