This Article Full Text (OnlineFirst PDF) Alert me when this article is cited Alert me if a correction is posted Services Email this article to a friend Similar articles in this journal Alert me to new issues of the journal Add to Saved Citations Download to citation manager Request Permissions Request Reprints Add to My Marked Citations Citing Articles Citing Articles via Scopus Google Scholar Articles by Sobeih, A. Articles by Hou, J. Social Bookmarking                         What's this?

Assertion Checking in J-Sim Simulation Models of Network Protocols

Department of Computer Science, University of Illinois at Urbana-Champaign, IL 61801, USA

^* To whom correspondence should be addressed. E-mail: s_ahmed_adel{at}yahoo.com.

	Abstract

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.

First published on October 22, 2009
SIMULATION 2009, doi:10.1177/0037549709349326


CiteULike    Complore    Connotea    Del.icio.us    Digg    Reddit    Technorati    Twitter    What's this?