Verification of simulation models of network protocols using state space exploration

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 (SSE) 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 property that must always hold true in all states.;In this thesis, we present the design and implementation of the state space exploration framework in J-Sim. Furthermore, we demonstrate its usefulness and effectiveness in verifying complicated simulation models. Specifically, we verify the simulation models of two widely used and fairly complex routing and data dissemination 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. Moreover, we verify the simulation model of a reliable unicast protocol: the Automatic Repeat reQuest ( ARQ) protocol.;To enable the verification of these fairly complex network simulation models, we make use of protocol-specific properties along two orthogonal dimensions: state similarity and state ranking. State similarity determines whether a state is "similar to" another in order to enable the implementation of stateful search. On the other hand, state ranking determines whether a state is "better than" another with respect to the implementation of best-first search (BeFS). Specifically, we 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 evaluate the efficiency of our state space exploration framework by comparing its performance to that of a state-of-the-art model checker for Java programs, namely Java PathFinder (JPF). The results of the comparison show that the time needed to find an assertion violation by our state space exploration framework in J-Sim can be significantly less than that in JPF unless a significant amount of programming effort is done in JPF to make its performance close to that of our SSE framework.;Finally, we present incremental state space exploration (ISSE), a technique that aims to provide a speedup in the state space exploration time of evolving simulation models; i.e., simulation models whose code changes from one version to another. A code change may or may not lead to a behavioral change. We analytically obtain necessary conditions for the ISSE technique to provide a speedup in the state space exploration time when compared to a traditional (non-incremental) SSE technique. We applied the ISSE technique to our case studies. In two case studies (namely AODV and directed diffusion), ISSE provided a speedup whereas in one case study (namely ARQ), it did not provide a speedup because the necessary conditions were violated.