Incremental State Space Exploration in J-Sim
Ahmed Sobeih, Steven Lauterburg · Illinois Digital Environment for Access to Learning and Scholarship (University of Illinois at Urbana-Champaign) · 2007
In this report, we present an incremental state space exploration technique that aims to provide a speedup in exploring the state space created by the execution of the simulation model of a network protocol for the purpose of verifying the model. We analytically obtain necessary conditions for the incremental state space exploration technique to provide a speedup in state space exploration time when compared to a traditional (non-incremental) state space exploration technique. We have implemented the incremental state space exploration technique in the J-Sim state space explorer. We provide three case studies for the simulation models of three network protocols: (a) Ad-Hoc On-Demand Distance Vector (AODV) routing protocol for wireless ad hoc networks, (b) directed diffusion protocol for wireless sensor networks, and (c) Automatic Repeat reQuest (ARQ). We study scenarios in which code changes may or may not lead to behavioral changes. 1 1 Non-incremental state space exploration procedure Figure 1 shows the pseudo-code of the non-incremental state space exploration procedure SSExplore(). The two major data structures in SSExplore() are ToBeExplored (which stores the states from which no transition has been explored yet) and AlreadyVisited (which stores the hash codes of the states