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

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