Award:PTC'23 Emerging Scholar
The Spectrum Policy community continues to deal with a long standing problem of facilitating effective co-existence of numerous radio operators for diverse use-cases while transmitting and receiving signals over the electromagnetic spectrum. Historically, the regulator has relied on developing a socio-legal construction of “spectrum operating rights” to enforce coordination between concurrent operations with the goal of avoiding all instances of “harmful
interference”. However, with the recent surge in the demand for radio-use licenses and the consequent risk of disruption in concurrent operation due to harmful interference, the regulator
has been forced to search for alternative ways to facilitate spectrum sharing and efficient resource utilization. In this paper, we develop a “spectrum-as-concurrent-programming” metaphor to describe spectrum policy by adopting tools developed within the domain of
programming language theory. We develop a methodology that focuses on defining a specification of the radio-frequency(RF) environment which provides the context within which
the behavior of concurrent radio-operations may be constrained, to replace the de-facto practice of relying on a description of radio-equipment standards. Additionally, we introduce the
rely-guarantee reasoning framework for automatically verifying the logical consistency of the set of operating rights issued by the regulator to the regulated entities.