Files in this item

FilesDescriptionFormat

application/pdf

application/pdfIncorporating B ... ntation and Evaluation.pdf (274kB)
(no description provided)PDF

Description

Title:Incorporating Bounded Model Checking in Network Simulation: Theory, Implementation and Evaluation
Author(s):Sobeih, Ahmed A.; Viswanathan, Mahesh; Hou, Jennifer C.
Subject(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.
Issue Date:2004-07
Genre:Technical Report
Type:Text
URI:http://hdl.handle.net/2142/10891
Other Identifier(s):UIUCDCS-R-2004-2466
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-16


This item appears in the following Collection(s)

Item Statistics