Software-based optimization of channel utilization in cognitive radio networks using priced timed automata

In Cognitive Radio (CR) networks, the vacant primary user channels should be utilized in an opportunistic manner, without causing any interference to the primary users. This opportunistic channel utilization needs to be effectively optimized for a competent CR network design. With this motivation, in this paper, we approach the channel utilization problem of CR networks from a software based model checking perspective rather than an ordinary analytical decomposition. Specifically, we model and simulate the CR communication system by the aid of the Priced Timed Automata(PTA) based Model Checking paradigm using UPPAAL. We apply this specific model checking enhanced with cost assignments to infer about the optimum utilization of primary user channels in CR networks. This way, given some specific properties of primary users and cognitive users, we are able to simulate and obtain the maximum utilization possible. Instead of running simulations simultaneously and exploring a subset of possible system runs, our proposed model checking has provided us the optimal system run amongst all the possible system runs.