Formal Modeling and Verification of Software-Defined Networking with Multiple Controllers

Miyoung Kang, Jin Young Choi

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

Traditional SDN has one controller, but more recent SDN approaches use multiple controllers on one network. However, the multiple controllers need to be synchronized with each other in order to guarantee a consistent network view, and complicated control management and additional control overhead are required. To overcome these limitations, Kandoo [5] has been proposed in which a root controller manages multiple unsynchronized local controllers. However, in this approach, loops can form between the local controllers because they manage different topologies. We propose a method for modeling a hierarchical design to detect loops in the topology and prevent them from occurring using UPPAAL model checker. In addition, the properties of multiple controllers are defined and verified based UPPAAL framework. In particular, we verify the following properties in a multiple controller: (1) elephant flows go through the root controller, (2) all flows go through the switch that is required to maintain security, and (3) they avoid unnecessary switches for energy efficiency.

Original languageEnglish
Title of host publicationTestbeds and Research Infrastructures for the Development of Networks and Communications - 14th EAI International Conference, TridentCom 2019 - Proceedings
EditorsHonghao Gao, Kuang Li, Xiaoxian Yang, Yuyu Yin
PublisherICST
Pages81-94
Number of pages14
ISBN (Electronic)9783030432157
DOIs
Publication statusPublished - 2020
Event14th EAI International Conference on Testbeds and Research Infrastructures for the Development of Networks and Communications, TridentCom 2019 - Changsha, China
Duration: 2019 Dec 72019 Dec 8

Publication series

NameEAI International Conference on Testbeds and Research Infrastructures for the Development of Networks and Communities (TRIDENTCOM)
ISSN (Electronic)2413-1059

Conference

Conference14th EAI International Conference on Testbeds and Research Infrastructures for the Development of Networks and Communications, TridentCom 2019
Country/TerritoryChina
CityChangsha
Period19/12/719/12/8

Bibliographical note

Funding Information:
Acknowledgments. This research was supported by Basic Science Research Program through the National Research Foundation of Korea (NRF) funded by the Ministry of Education (2018R1A6A3A01012955) and supported by Basic Science Research Program through the National Research Foundation of Korea (NRF) funded by the Ministry of Education (2018R1A2B6009122).

Publisher Copyright:
© ICST Institute for Computer Sciences, Social Informatics and Telecommunications Engineering 2020 Published by Springer Nature Switzerland AG 2020. All Rights Reserved.

Keywords

  • Formal modeling
  • Formal verification
  • SDN
  • UPPAAL

ASJC Scopus subject areas

  • Hardware and Architecture
  • Information Systems
  • Computer Science (miscellaneous)
  • Artificial Intelligence
  • Computer Networks and Communications

Fingerprint

Dive into the research topics of 'Formal Modeling and Verification of Software-Defined Networking with Multiple Controllers'. Together they form a unique fingerprint.

Cite this