Formal modeling and verification of SDN-OpenFlow

Miyoung Kang, Eun Young Kang, Dae Yon Hwang, Beom Jin Kim, Ki Hyuk Nam, Myung Ki Shin, Jin Young Choi

Research output: Contribution to conferencePaper

14 Citations (Scopus)

Abstract

Software-Defined Networking (SDN) is a network architecture where a controller manages flow control to enable intelligent networking. Currently, a popular specification for creating an SDN is an open standard called OpenFlow. The behavior of the SDN OpenFlow (SDN-OF) is critical to the safety of the network system and its correctness must be proven so as to avoid system failures. In this paper, we report our experience in applying formal techniques for modeling and analysis of SDN-OF. The formal model of SDN-OF is described in detail and its correctness is formalized in logical formulas based on the informal specification. The desired properties are verified over the model using VERSA and UPPAAL. Our work-in-progressinvolves the development of a model translation tool that facilitates automatic conversion of the verified model to Python for modular code synthesis on the application platform

Original languageEnglish
Pages481-482
Number of pages2
DOIs
Publication statusPublished - 2013
EventIEEE 6th International Conference on Software Testing, Verification and Validation, ICST 2013 - Luxembourg, Luxembourg
Duration: 2013 May 182013 May 20

Other

OtherIEEE 6th International Conference on Software Testing, Verification and Validation, ICST 2013
CountryLuxembourg
CityLuxembourg
Period13/5/1813/5/20

Keywords

  • ACSR
  • Formal Verification
  • SDN
  • UPPAAL

ASJC Scopus subject areas

  • Software

Fingerprint Dive into the research topics of 'Formal modeling and verification of SDN-OpenFlow'. Together they form a unique fingerprint.

  • Cite this

    Kang, M., Kang, E. Y., Hwang, D. Y., Kim, B. J., Nam, K. H., Shin, M. K., & Choi, J. Y. (2013). Formal modeling and verification of SDN-OpenFlow. 481-482. Paper presented at IEEE 6th International Conference on Software Testing, Verification and Validation, ICST 2013, Luxembourg, Luxembourg. https://doi.org/10.1109/ICST.2013.69