Assume-Guarantee Contracts as a Spectrum Management Tool

In this paper, we use the framework of dynamical systems theory to introduce a new theoretical model that captures the behavior of radio signals over hyper-space time. We focus on modeling the operation of concurrent radio services or operators as dynamical systems that transform radio signals over an n-dimensional hyper-spacetime. This model provides a valuable framework to define spectrum operating rights in a manner that's amenable to automated compositional verification. It builds on prior work within the spectrum management community and helps unify the specification frameworks that rely on probabilistic transmission permissions and reception protections. The primary disadvantage of the dynamical systems approach is that it is a relatively new idea within this community. There needs to be literature on identifying the model descriptions that effectively capture the behavior of any legacy or modern radio service/operator. However, our model provides a sufficient capability for capturing the behavior of the physical environment and the interactions between inter-connected concurrently operating radio users across geographical regions. We describe the framework of specifying the radio operating rights through Assume-Guarantee contracts and illustrate its use with a simple two-system example focusing on the recent FCC "5G-vs-Radio-Altimeter" fiasco. Through the medium of this case study, we propose to use a high-level specification language based on spatiotemporal logic to describe spectrum operating rights. This proposal contrasts the de-facto practice of relying on low-level specifications that describe threshold values for individual physical attributes of the radio signals