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, 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