In this paper, we report our work on extending the J-Sim network simulator to be an integrated environment for both simulation and model checking of network protocols. We also present a case study in which we model-checked AODV in J-Sim.

Many next generation applications (such as video flows) are likely to have associated minimum data rate requirements in order to ensure satisfactory quality as perceived by end-users. In this paper, we develop a framework to address the problem of maximizing the aggregate utility of traffic flows in a multi-hop wireless network, with constraints imposed both due to self-interference and minimum rate requirements. The parameters that are tuned in order to maximize the utility are (i) transmission powers of individual nodes and (ii) the channels assigned to the different communication links. Our framework is based on using a cross-decomposition technique that takes both inter-flow interference and self-interference into account. The output of our framework is a schedule that dictates what links are to be activated in each slot and the parameters associated with each of those links. If the minimum rate constraint cannot be satisfied for all of the flows, the framework intelligently rejects a sub-set of the flows and recomputes a schedule for the remaining flows. We also design an admission control module that determines if new flows can be admitted without violating the rate requirements of the existing flows in the network. We provide numerical results to demonstrate the efficacy of our framework.