Testbeds and Research Infrastructures for the Development of Networks and Communications. 14th EAI International Conference, TridentCom 2019, Changsha, China, December 7-8, 2019, Proceedings

Research Article

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

  • @INPROCEEDINGS{10.1007/978-3-030-43215-7_6,
        author={Miyoung Kang and Jin-Young Choi},
        title={Formal Modeling and Verification of Software-Defined Networking with Multiple Controllers},
        proceedings={Testbeds and Research Infrastructures for the Development of Networks and Communications. 14th EAI International Conference, TridentCom 2019, Changsha, China, December 7-8, 2019, Proceedings},
        proceedings_a={TRIDENTCOM},
        year={2020},
        month={3},
        keywords={SDN Formal modeling Formal verification UPPAAL},
        doi={10.1007/978-3-030-43215-7_6}
    }
    
  • Miyoung Kang
    Jin-Young Choi
    Year: 2020
    Formal Modeling and Verification of Software-Defined Networking with Multiple Controllers
    TRIDENTCOM
    Springer
    DOI: 10.1007/978-3-030-43215-7_6
Miyoung Kang1,*, Jin-Young Choi1,*
  • 1: Korea University
*Contact email: mykang@formal.korea.ac.kr, choi@formal.korea.ac.kr

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.