Towards automated verification of autonomous networks: A case study in self-configuration

JaeSeung Song; Tiejun Ma; Peter Pietzuch

doi:10.1109/PERCOMW.2010.5470504

Towards automated verification of autonomous networks: A case study in self-configuration

JaeSeung Song
, Tiejun Ma
, Peter Pietzuch

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Abstract

In autonomic networks, the self-configuration of network entities is one of the most desirable properties. In this paper, we show how formal verification techniques can verify the correctness of self-configuration. As a case study, we describe the configuration of physical cell identifiers (PCIs), a radio configuration parameter in cellular base stations. We provide formal models of PCI assignment algorithms and their desired properties. We 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, we argue that both simulation and verification should be adopted and highlight the potential of runtime verification approaches in this space.

Original language	English
Title of host publication	2010 8th IEEE International Conference on Pervasive Computing and Communications Workshops (PERCOM Workshops)
Publisher	Institute of Electrical and Electronics Engineers
Pages	582-587
Number of pages	6
ISBN (Electronic)	978-1-4244-6606-1
ISBN (Print)	978-1-4244-6605-4
DOIs	https://doi.org/10.1109/PERCOMW.2010.5470504
Publication status	Published - 29 Mar 2010
Event	8th IEEE International Conference on Pervasive Computing and Communications Workshops - Mannheim, Germany Duration: 29 Mar 2010 → 2 Apr 2010

Conference

Conference	8th IEEE International Conference on Pervasive Computing and Communications Workshops
Abbreviated title	PERCOM Workshops 2010
Country/Territory	Germany
City	Mannheim
Period	29/03/10 → 2/04/10

Access to Document

10.1109/PERCOMW.2010.5470504Licence: All Rights Reserved

https://ieeexplore.ieee.org/document/5470504Licence: All Rights Reserved

Cite this

@inproceedings{25152596d53240bfb3eec76fa41deee7,

title = "Towards automated verification of autonomous networks: A case study in self-configuration",

abstract = "In autonomic networks, the self-configuration of network entities is one of the most desirable properties. In this paper, we show how formal verification techniques can verify the correctness of self-configuration. As a case study, we describe the configuration of physical cell identifiers (PCIs), a radio configuration parameter in cellular base stations. We provide formal models of PCI assignment algorithms and their desired properties. We 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, we argue that both simulation and verification should be adopted and highlight the potential of runtime verification approaches in this space.",

author = "JaeSeung Song and Tiejun Ma and Peter Pietzuch",

year = "2010",

month = mar,

day = "29",

doi = "10.1109/PERCOMW.2010.5470504",

language = "English",

isbn = "978-1-4244-6605-4",

pages = "582--587",

booktitle = "2010 8th IEEE International Conference on Pervasive Computing and Communications Workshops (PERCOM Workshops)",

publisher = "Institute of Electrical and Electronics Engineers",

address = "United States",

note = "8th IEEE International Conference on Pervasive Computing and Communications Workshops, PERCOM Workshops 2010 ; Conference date: 29-03-2010 Through 02-04-2010",

}

Song, J, Ma, T & Pietzuch, P 2010, Towards automated verification of autonomous networks: A case study in self-configuration. in 2010 8th IEEE International Conference on Pervasive Computing and Communications Workshops (PERCOM Workshops). Institute of Electrical and Electronics Engineers, pp. 582-587, 8th IEEE International Conference on Pervasive Computing and Communications Workshops, Mannheim, Baden-Württemberg, Germany, 29/03/10. https://doi.org/10.1109/PERCOMW.2010.5470504

Towards automated verification of autonomous networks: A case study in self-configuration. / Song, JaeSeung; Ma, Tiejun; Pietzuch, Peter.
2010 8th IEEE International Conference on Pervasive Computing and Communications Workshops (PERCOM Workshops). Institute of Electrical and Electronics Engineers, 2010. p. 582-587.

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - Towards automated verification of autonomous networks: A case study in self-configuration

AU - Song, JaeSeung

AU - Ma, Tiejun

AU - Pietzuch, Peter

PY - 2010/3/29

Y1 - 2010/3/29

N2 - In autonomic networks, the self-configuration of network entities is one of the most desirable properties. In this paper, we show how formal verification techniques can verify the correctness of self-configuration. As a case study, we describe the configuration of physical cell identifiers (PCIs), a radio configuration parameter in cellular base stations. We provide formal models of PCI assignment algorithms and their desired properties. We 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, we argue that both simulation and verification should be adopted and highlight the potential of runtime verification approaches in this space.

AB - In autonomic networks, the self-configuration of network entities is one of the most desirable properties. In this paper, we show how formal verification techniques can verify the correctness of self-configuration. As a case study, we describe the configuration of physical cell identifiers (PCIs), a radio configuration parameter in cellular base stations. We provide formal models of PCI assignment algorithms and their desired properties. We 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, we argue that both simulation and verification should be adopted and highlight the potential of runtime verification approaches in this space.

U2 - 10.1109/PERCOMW.2010.5470504

DO - 10.1109/PERCOMW.2010.5470504

M3 - Conference contribution

SN - 978-1-4244-6605-4

SP - 582

EP - 587

BT - 2010 8th IEEE International Conference on Pervasive Computing and Communications Workshops (PERCOM Workshops)

PB - Institute of Electrical and Electronics Engineers

T2 - 8th IEEE International Conference on Pervasive Computing and Communications Workshops

Y2 - 29 March 2010 through 2 April 2010

ER -

Towards automated verification of autonomous networks: A case study in self-configuration

Abstract

Conference

Access to Document

Fingerprint

Cite this