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

  • Miyoung Kang
  • Jin-Young ChoiEmail author
Conference paper
Part of the Lecture Notes of the Institute for Computer Sciences, Social Informatics and Telecommunications Engineering book series (LNICST, volume 309)


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.


SDN Formal modeling Formal verification UPPAAL 



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).


  1. 1.
    KcKeown, N., et al.: OpenFlow: enabling innovation in campus networks. ACM SIGCOMM Comput. Commun. Rev. 28, 69–74 (2008)Google Scholar
  2. 2.
    Hawilo, H., Shami, A., Mirahmadi, M., Asal, R.: NFV: state of the art, challenges and implementation in next generation mobile networks (vEPC). IEEE Netw. Mag. 28, 18–26 (2014)CrossRefGoogle Scholar
  3. 3.
    Dotan, D., Pinter, R.Y.: HyperFlow: an integrated visual query and dataflow language for end-user information analysis. In: IEEE Symposium Visual Languages and Human-Centric Computing (VL/HCC), pp. 27–34 (2005)Google Scholar
  4. 4.
    Shtykh, R.Y., Suzuki, T.: Distributed data stream processing with Onix. In: IEEE 4th International Conference on Big Data Cloud Computing, pp. 267–268 (2014)Google Scholar
  5. 5.
    Yegabeh, S.H., Ganjali, Y.: Kandoo: a framework for efficient and scalable offloading of control applications. In: HotSDN 2012, Helsinki, Finland (2012)Google Scholar
  6. 6.
    Behrmann, G., David, A., Larsen, K.G.: A tutorial on UPPAAL. In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol. 3185, pp. 200–236. Springer, Heidelberg (2004). Scholar
  7. 7.
    OpenFlow Switch Specification. Accessed 26 Aug 2019
  8. 8.
  9. 9.
    ONF. Accessed 25 July 2018
  10. 10.
    Braun, W., Menth, M.: Software-defined networking using OpenFlow: protocols, applications and architectural design choices. Future Internet 6, 302–3363 (2014)CrossRefGoogle Scholar
  11. 11.
    Canini, M., Venzano, D., Peresini, P., Kostic, D., Rexford, J.: A NICE way to test OpenFlow applications. In: NSDI (2012)Google Scholar
  12. 12.
    Foster, N., Harrison, R., Meola, M.L., Freedman, M.J., Rexford, M.J.J., Walker, D.: Frenetic: a high-level language for OpenFlow networks. In: Proceedings on PRESTO 2010 (2011)Google Scholar
  13. 13.
    Monsanto, C., Foster, N., Harrison, R., Walker, D.: A compiler and run-time system for network programming languages. In: POPL (2012)Google Scholar
  14. 14.
    Kazemian, P., Varghese, G., McKeown, N.: Header space analysis: static checking for networks. In: NSDI (2012)Google Scholar
  15. 15.
    Reitblatt, M., Foster, N., Rexford, J., Schlesinger, C., Walker, D.: Abstraction for network update. In: SIGCOMM (2012)Google Scholar
  16. 16.
    Canini, M., Kuznetsov, P., Levin, D., Schmid, S.: Distributed and robust SDN control plane for transactional network updates. In: INFOCOM 2015 (2015)Google Scholar
  17. 17.
    Kang, M., Choi, J., Kang, I., Kwak, H., Ahn, S., Shin, M.: A verification method of SDN firewall applications. IEICE Trans. Commun. E99-B(7), 1408–1415 (2016)CrossRefGoogle Scholar
  18. 18.
    Xiao, L., Xiang, S., Zhu, H.: Modeling and verifying SDN with multiple controllers. In: Proceedings of SAC 2018: Symposium on Applied Computing (2018)Google Scholar

Copyright information

© ICST Institute for Computer Sciences, Social Informatics and Telecommunications Engineering 2020

Authors and Affiliations

  1. 1.Center for Information Security TechnologiesKorea UniversitySeoulKorea

Personalised recommendations