Verification of Simulation Models of Network Protocols Using State Space Exploration and Protocol-Specific Properties

Sobeih, Ahmed A.; d'Amorim, Marcelo; Viswanathan, Mahesh; Marinov, Darko; Hou, Jennifer C.

Permalink

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

Description

Title

Verification of Simulation Models of Network Protocols Using State Space Exploration and Protocol-Specific Properties

Author(s)

• Sobeih, Ahmed A.
• d'Amorim, Marcelo
• Viswanathan, Mahesh
• Marinov, Darko
• Hou, Jennifer C.

Issue Date

2007-08

Keyword(s)

networking

Abstract

"Verification and Validation (V&V) is a critically important phase in the development life cycle of a simulation model. In the context of network simulation, traditional network simulators perform well in using a simulation model for evaluating/predicting the performance of a network protocol but lack the capability of verifying the ""correctness"" of the simulation model being used. To address this problem, we have extended J-Sim --- an open-source component-based network simulator written entirely in Java --- with a state space exploration capability that explores the (entire) state space created by a network simulation model in order to find an execution (if any) that violates an assertion; i.e., a safety property. In this paper, we elaborate on the state space exploration framework in J-Sim and demonstrate its usefulness and effectiveness in verifying complicated simulation models. Specifically, we verify the simulation models of two widely used and fairly complex network protocols: the Ad-Hoc On-Demand Distance Vector (AODV) routing protocol for wireless ad hoc networks and the directed diffusion data dissemination protocol for wireless sensor networks. To enable the verification of these fairly complex network simulation models, we make use of structural properties in the underlying state space along two orthogonal dimensions; the first uses a non-trivial simulation relation to prune the states to be searched, and the second is state ranking that determines whether a state is ""better than"" another in order to enable the implementation of a best-first search (BeFS). We also develop protocol-specific search heuristics to guide state space exploration towards finding assertion violations in less time. In particular, we report findings on how to devise good search heuristics for routing/data dissemination protocols similar to AODV and directed diffusion. We also show that the time needed to find an assertion violation by our state space exploration framework in J-Sim is comparable to that of Java PathFinder (JPF), a state-of-the-art model checker for Java programs."

Type of Resource

text

Permalink

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

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