TY - GEN
T1 - Formal modeling and verification of software-defined networking with multiple controllers
AU - Kang, Miyoung
AU - Choi, Jin Young
N1 - 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.
PY - 2020
Y1 - 2020
N2 - 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.
AB - 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.
KW - Formal modeling
KW - Formal verification
KW - SDN
KW - UPPAAL
UR - http://www.scopus.com/inward/record.url?scp=85082298755&partnerID=8YFLogxK
U2 - 10.1007/978-3-030-43215-7_6
DO - 10.1007/978-3-030-43215-7_6
M3 - Conference contribution
AN - SCOPUS:85082298755
SN - 9783030432140
T3 - Lecture Notes of the Institute for Computer Sciences, Social-Informatics and Telecommunications Engineering, LNICST
SP - 81
EP - 94
BT - Testbeds and Research Infrastructures for the Development of Networks and Communications - 14th EAI International Conference, TridentCom 2019, Proceedings
A2 - Gao, Honghao
A2 - Li, Kuang
A2 - Yang, Xiaoxian
A2 - Yin, Yuyu
PB - Springer
T2 - 14th EAI International Conference on Testbeds and Research Infrastructures for the Development of Networks and Communications, TridentCom 2019
Y2 - 7 December 2019 through 8 December 2019
ER -
