Date Added: Jan 2010
In autonomic networks, the self-configuration of network entities is one of the most desirable properties. In this paper, the authors show how formal verification techniques can verify the correctness of self-configuration. As a case study, they describe the configuration of Physical Cell Identifiers (PCIs), a radio configuration parameter in cellular base stations. They provide formal models of PCI assignment algorithms and their desired properties. They then demonstrate how the potential for conflicting PCI assignments can be detected using model checking and resolved in the design stage. Through this case study, they argue that both simulation and verification should be adopted and highlight the potential of run-time verification approaches in this space.