An Application of Formal Methods to Cognitive Radios

Design and Implementation of Formal Tools and Systems 2011.

计算机科学;

Konstantine Arkoudas ; Ritu Chadha ; Jason Chiang

Others  :  http://ceur-ws.org/Vol-832/paper_11.pdf
PID  :  33672

学科分类：计算机科学（综合）

来源: CEUR

【 摘 要 】

We discuss the design and implementation of a formal policy system regulating dynamic spectrum access (DSA) for cognitive radios. DSA policies are represented and manipulated in a proof framework based on first-order logic with arithmetic and algebraic data types. Various algebraic operations combining such policies can be easily implemented in such a framework. Reasoning about transmission requests is formulated as a satisfiability-modulo-theories (SMT) problem. Efficient SMT solvers are used to answer the corresponding queries and also to analyze the policies themselves. Further, we show how to reason about transmission requests in an optimal way by modeling the problem as an SMT instance of weighted Max-SAT, and we demonstrate that this problem too can be efficiently solved by cuttingedge SMT solvers. We also show that additional optimal operations on transmission requests can be cast as classic optimization problems, and to that end we give an algorithm for minimizing integer-valued objective functions with a small number of calls to an oracle SMT solver. We present experimental results on the performance of our system, and compare it to previous work in the field