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 the performance of a network protocol but lack the capability to check 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 state space created by a network simulation model, up to a configurable maximum depth, in order to find an execution (if any) that violates an assertion, i.e. a property specifying an invariant that must always hold true in all states. In this paper, we elaborate on the SSE framework in J-Sim and present one of our fairly complex case studies, namely verifying the simulation model of the Ad-hoc On-demand Distance Vector (AODV) routing protocol for wireless ad-hoc networks. The SSE framework makes 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. State ranking determines whether a state is “better than” another in order to enable the implementation of best-first search (BeFS). Specifically, we develop protocol-specific search heuristics to guide SSE towards finding assertion violations in less time. We evaluate the efficiency of our SSE framework by comparing its performance with 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 SSE framework in J-Sim can be significantly less than that in JPF unless a substantial amount of programming effort is spent in JPF to make its performance close to that of our SSE framework.

In this paper, we present a component-based network simulation environment that provides a systematic way to simulate, with high fidelity, protocol operations in a variety of target network architectures. We take a four-step approach to developing such a composable network simulation environment with reusable components. First, we lay a component-based software architecture, called the autonomous component architecture (ACA). Second, we propose a new real-time, process-driven simulation technique that fits naturally in ACA and simulates the real system realistically. Third, we devise a packet-based network simulation framework, called extensible internetworking framework (INET), on top of ACA. Fourth, we implement in Java both ACA and INET, and several representative suites of protocol components in a variety of network architectures. The resulting codes, along with a scripting framework, constitute a network simulation environment called J-Sim. By virtue of the many desirable features inherited from ACA, the J-Sim environment meets the flexibility, composability, reusability, extensibility and diagnosability requirements. The price J-Sim pays for the many desirable features is, however, the inter-component communication overhead. In this paper, we show (via experimentation) that this overhead is not significant (in the range of 0.2—0.6 μs), and J-Sim achieves better scalability than two other network simulators in the public domains, ns-2 and Scalable Simulation Framework Network Models (SSFNET), in terms of both the experiment setup time and the simulation completion time.

We present a novel technique that speeds up state-space exploration (SSE) for evolving programs with dynamically allocated data. SSE is the essence of explicit-state model checking and an increasingly popular method for automating test generation. Traditional, non-incremental SSE takes one version of a program and systematically explores the states reachable during the program's executions to find property violations. Incremental SSE considers several versions that arise during program evolution: reusing the results of SSE for one version can speed up SSE for the next version, since state spaces of consecutive program versions can have significant similarities. We have implemented our technique in two model checkers: Java PathFinder and the J-Sim state-space explorer. The experimental results on 24 program evolutions and exploration changes show that for non-initial runs our technique speeds up SSE in 22 cases from 6.43% to 68.62% (with median of 42.29%) and slows down SSE in only two cases for -4.71% and -4.81%.

Verification and Validation (VV 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.1

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.1

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 that have already been visited). Figure 1 presents an explicit-state stateful search that avoids visiting a state s1 if another state s2, having the same hash code as s1, has already been visited before. SSExplore() interacts with three instances of a class called GlobalState, which implements the definition of the state of the network protocol. These three instances are initialState (the initial state), currentState (the current state being explored) and nextState (one of the possible successors of the current state). Initially, AlreadyVisited contains the hash code of the initial state only (Figure 1, line 3) and ToBeExplored contains the initial state only (Figure 1, line 4). As long as ToBeExplored is not empty (Figure 1, line 5), SSExplore() removes a state from ToBeExplored and sets currentState to it (Figure 1, line 6). For each state being explored (currentState), SSExplore() determines the events that are enabled in currentState by invoking GenerateEnabledEvents() (Figure 1, line 7). In GenerateEnabledEvents(), the enabling function (Figure 1, line 26) returns the number of possible successor states for each event (zero if the event is disabled). GenerateEnabledEvents() returns EnabledEvents, which is a list of enabled events (Figure 1, line 29). Each entry in EnabledEvents stores the corresponding event information EventInfo (Figure 1, line 28). Specifically, let each protocol entity have a unique ID n (Figure 1, line 24), each event have a unique ID e (Figure 1, line 25), and each enabled event has a set of integer-valued parameters i This technical report shows detailed results for incremental state space exploration in J-Sim, and it is a part of a larger work [6] on incremental state space exploration, including evaluation in Java PathFinder (JPF).

In this paper, an almost peer-to-peer (AP2P) clock synchronization protocol is proposed. AP2P is almost peer-to-peer in the sense that it provides the desirable features of a purely hierarchical (client/server) clock synchronization protocol while avoiding the undesirable consequences of a purely peer-to-peer one. In AP2P, a unique node is elected as a leader in a distributed manner. Each non-leader node adjusts its clock rate based on message exchanges with its neighbors, taking into consideration that neighbors that are closer to the leader have more effect on the adjustment than the neighbors that are further away from the leader. We compare the performance of AP2P with that of the server time protocol (STP), which is a purely hierarchical clock synchronization protocol. Simulation results, which have been conducted on several network topologies, have shown that AP2P can provide a clock synchronization accuracy that is indistinguishable from that of STP. Furthermore, AP2P is more fault-tolerant because it can recover from certain types of failures that STP cannot recover from.

Java PathFinder (JPF) is an explicit-state model checker for Java programs. It explores all executions that a given program can have due to different thread interleavings and nondeterministic choices. JPF implements a backtracking Java Virtual Machine (JVM) that executes Java bytecodes using a special representation of JVM states. This special representation enables JPF to quickly store, restore, and compare states; it is crucial for making the overall state exploration efficient. However, this special representation creates overhead for each execution, even execution of deterministic blocks that have no thread interleavings or nondeterministic choices.We propose mixed execution, a technique that reduces execution time of deterministic blocks in JPF. JPF is written in Java as a special JVM that runs on top of a regular, host JVM. Mixed execution works by translating the state between the special JPF representation and the host JVM representation. We also present lazy translation, an optimization that speeds up mixed execution by translating only the parts of the state that a specific execution dynamically depends on. We evaluate mixed execution on six programs that use JPF for generating tests for data structures and on one case study for verifying a network protocol. The results show that mixed execution can improve the overall time for state exploration up to 36.98%, while improving the execution time of deterministic blocks up to 69.15%. Although we present mixed execution in the context of JPF and Java, it generalizes to any model checker that uses a special state representation.

Traditional network simulators perform well in evaluating the performance of network protocols but lack the capability of verifying the correctness of protocols. To address this problem, we have extended the J-Sim network simulator with a model checking capability that explores the state space of a network protocol to find an execution that violates a safety invariant. In this paper, we demonstrate the usefulness of this integrated tool for verification and performance evaluation by analyzing two widely used and important network protocols: AODV and directed diffusion. Our analysis discovered a previously unknown bug in the J-Sim implementation of AODV. More importantly, we also discovered a serious deficiency in directed diffusion. To enable the analysis of these fairly complex protocols, we needed to develop protocol-specific search heuristics that guide state-space exploration. We report our findings on discovering good search heuristics to analyze network protocols similar to AODV and directed diffusion.

In this paper, we present the design methodology, and the software architecture, of J-Sim, an open-source network simulation/emulation environment that has been developed, in part, under the support of the NSF next generation software program. We first give an overview of the component-based software architecture, called the autonomous component architecture (ACA), that is used as the underlying architecture for J-Sim. Then we describe how we lay a generalized packet-based network simulation framework, called extensible internetworking framework (INET), on top of ACA. Both the ACA and the INET have been implemented in Java. The resulting codes, along with an essential suite of network protocols and components (for the Internet best-effort/integrated services/differentiated services architecture) its extension for wireless and sensor networks, and a scripting framework and GUI interfaces, is called J-Sim. To demonstrate the composability and extensibility of J-Sim, we elaborate on how we model in J-Sim several different network architectures, namely the differentiated services (diffserv) architecture, the multiprotocol label switching (MPLS) architecture, and the wireless sensor network architecture.

Network simulators perform well in evaluating the performance of network protocols, but lack the capability of verifying their correctness. In order to address this lacuna, we have extended the J-Sim network simulator with a model checking capability to explore the state space of a network protocol to find either an execution where a safety invariant is violated or an exceution where the satisfaction of an eventuality property is witnessed. In this paper, we demonstrate the usefulness of this integrated tool for verification and performance evaluation, by analyzing two widely used and important network protocols: Ad-Hoc On-Demand Distance Vector (AODV) routing protocol and directed diffucion protocol. Our analysis discovered a previously unknown bug in the J-Sim implementation of AODV, and a design flaw in directed diffusion, illustrating that our tool can uncover both bugs in the implementation and design of a protocol. To enable the analysis of these fairly complex protocols, we needed to develop search heuristics to explore the state space. We report our preliminary findings on discovering good search heuristics to analyze routing protocols.

Wireless sensor networks (WSNs) have gained considerable attention in the past few years. As such, there has been an increasing need for defining and developing simulation frameworks for carrying out high-fidelity WSN simulation. In this paper, the authors presented a modeling and simulation framework for WSNs in J-Sim - an open-source, component-based compositional network simulation environment that is developed entirely in Java. This framework is built upon the autonomous component architecture (ACA) and the extensible internetworking framework (INET) of J-Sim, and provides an object-oriented definition of (i) target, sensor and sink nodes, (ii) sensor and wireless communication channels, and (iii) physical media such as seismic channels, mobility model and power model (both energy-producing and energy-consuming components). Application-specific models can be defined by sub-classing classes in the simulation framework and customizing their behaviors. The use of the proposed WSN simulation framework was demonstrated by implementing several well-known localization, geographic routing, and directed diffusion protocols. In addition, performance comparisons were performed (in terms of execution time incurred, and the memory used) in simulating several typical WSN scenarios in J-Sim and ns-2. The simulation study indicates that the proposed WSN simulation framework in J-Sim is much more scalable than ns-2 (especially in memory usage).

Existing network simulators perform reasonably well in evaluating the performance of network protocols, but lack the capability of verifying and validating the correctness of network protocols. In this paper we have extended J-Sim - an open-source, component-based compositional network simulation environment - with the model checking capability to explore the state space created by a network protocol until either the entire state space is explored (if the state space is finite) or an error (e.g., a violation of a user-defined safety assertion) is discovered. We also exploit protocol-specific properties in the process of exploring the state space, to reduce the size of the state space and to guide the (best-first) search towards paths that can potentially locate errors in less time. As a proof of concept, we have demonstrated use of the J-Sim model checker in locating errors in an automatic repeat request (ARQ) protocol. As compared to the Maude LTL model checker, the J-Sim model checker can locate errors in a timely manner and with shorter error traces.

ó Existing network simulators perform reasonably well in evaluating the performance of network protocols, but lack the capability of verifying the correctness of network protocols. In this paper, we present our ongoing research on extending J-Sim ó an open-source, component-based compositional network simulation environment ó with the model checking capability to explore the state space created by a network protocol in order to nd a violation of a desirable safety property and/or to nd a witness for a desirable liveness property if any exists. This paper shows how J-Sim can model-check the Ad-Hoc On-Demand Distance Vector (AODV) routing protocol, a fairly complex network protocol with thousands of lines of Java code. We also exploit protocol-specic properties in the process of exploring the state space, to reduce the size of the state space and to guide the (best-rst) search towards paths that can potentially locate violations/witnesses in less time. The experimental results presented in this paper show that a best-rst search strategy can provide several orders of magnitude reduction in both the time and space overheads needed to nd violations/witnesses.

Application-layer multicast (ALM) protocols differ in, among other aspects, the topology of the underlying overlay network (e.g., tree, mesh or ring). Therefore, comparing the performance of ALM overlay networks is an important step towards assessing the inherent advantages and/or limitations of each overlay network topology. In particular, ring-based ALM overlay networks have the advantages of (a) providing a constant node degree; i.e., the number of neighbors each group member has on the overlay network is constant and independent of the size of the multicast group and (b) enabling the implementation of secure, reliable and totally-ordered message delivery through the use of a ring with a token that contains ordering and flow control information. Motivated thus, we present in this paper a simulation-based performance evaluation and comparison between two ALM overlay networks. The first connects the multicast group members in a ring overlay network while the second connects them in a tree. Simulation results, which have been conducted in J-Sim, have shown that although a ring overlay network incurs a higher path stretch and a higher link stress than a tree overlay network, it provides a constant and lower node degree and a higher data delivery ratio despite the failure/leaving of a single multicast group member than those provided by a tree overlay network.

A reliable multicast protocol for wireless mobile multihop ad hoc networks (ReMHoc) is proposed. ReMHoc ensures the eventual delivery of the multicast data to all the multicast group members. ReMHoc is receiver-initiated and NACK-based, and it makes use of feedback suppression in order to avoid negative acknowledgement (NACK) and retransmission implosion. The loss recovery burden is distributed over the multicast group members in order to reduce recovery latency and end-to-end delay. Simulations (using GloMoSim 2.0) have demonstrated the scalability of ReMHoc.

In response to the important role that multicasting plays in wireless mobile multihop ad hoc networks, we study in this paper the reliability of the on-demand multicast routing protocol (ODMRP) in terms of the delivery of data packets. Using GloMoSim 2.0, the simulation results have shown that using ODMRP, the average miss ratio does not always increase with increasing the speeds of mobility of the mobile hosts in the ad hoc network. Instead, there is a "sweet spot" of values of the mobility speeds of the mobile hosts. In addition, the average miss ratio decreases with increasing the number of multicast group members, which indicates that ODMRP has more packet delivery capabilities for denser multicast groups.

This paper presents the design, analysis and performance evaluation of VRing, a novel application-layer multicast (ALM) protocol that establishes a virtual ring as an overlay network among the multicast group members in a self- organizing and distributed manner. VRing takes advantage of the inherent desirable property of a ring; namely, the degree of each node on the ring is O(1) (i.e., independent of the number of the multicast group members) and hence, the state maintained at each multicast group member is also O(1). This property significantly eases the key distribution process, as each member has exactly one predecessor and one successor. In order to reduce the routing delay and increase the survivability of the ring overlay network, we propose to form a spare ring overlay structure that improves connectivity among multicast group members. Furthermore, we also propose, and analytically study the performance of, a data delivery and duplicate suppression mechanism that makes use of both the original ring and the spare ring for forwarding multicast data packets to the multicast group members. We conduct simulations of both VRing and a hierarchical ALM protocol, NICE, using the J-Sim network simulator. Simulation results show that although VRing has a higher path stretch and a higher link stress than NICE, it incurs less control overhead, consumes less bandwidth, and provides lower average node degree than NICE. Furthermore, VRing achieves a higher (up to twice as much) average data delivery ratio in the presence of failures than NICE. The performance improvement is especially pronounced for larger multicast groups.

Sensor networks have gained considerable importance and attention in the past few years. Hence, an inevitable need for developing simulation frameworks for sensor networks in existing network simulators arises. In this paper, we describe our work in incorporating wireless sensor networks simulation in J-Sim. We have built a simulation framework for sensor networks that builds upon the autonomous component architecture (ACA) and the extensible internetworking framework (INET) of J-Sim. The paper shows how each layer in the protocol stack of a sensor node can be implemented as a component and how ports and contracts enable different layers (components) to interact with each other in the initiator-reactor mechanism that is a fundamental concept of J-Sim.

Existing network simulators perform reasonably well in evaluating the performance of network protocols, but lack the capability of verifying the correctness of network protocols. In this paper, we present our ongoing research on extending J-Sim — an open-source, component-based compositional network simulation environment — with the model checking capability to explore the state space created by a network protocol in order to find a violation of a desirable safety property and/or to find a witness for a desirable liveness property if any exists. This paper shows how J-Sim can model-check the Ad-Hoc On-Demand Distance Vector (AODV) routing protocol, a fairly complex network protocol with thousands of lines of Java code. We also exploit protocol-specific properties in the process of exploring the state space, to reduce the size of the state space and to guide the (best-first) search towards paths that can potentially locate violations/witnesses in less time. The experimental results presented in this paper show that a best-first search strategy can provide several orders of magnitude reduction in both the time and space overheads needed to find violations/witnesses.