Formal Modeling and Verification of SDN-OpenFlow

Author

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

fYear

2013

fDate

18-22 March 2013

Firstpage

481

Lastpage

482

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

Keywords

Analytical models; Control systems; Delays; Network topology; Safety; System recovery; Topology; ACSR; Formal Verification; SDN; UPPAAL;

fLanguage

English

Publisher

ieee

Conference_Titel

Software Testing, Verification and Validation (ICST), 2013 IEEE Sixth International Conference on

Conference_Location

Luxembourg, Luxembourg

Print_ISBN

978-1-4673-5961-0

Type

conf

DOI

10.1109/ICST.2013.69

Filename

6569764