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

doi:10.1109/ICST.2013.69

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 conference › Paper › peer-review

19 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 language	English
Pages	481-482
Number of pages	2
DOIs	https://doi.org/10.1109/ICST.2013.69
Publication status	Published - 2013
Event	IEEE 6th International Conference on Software Testing, Verification and Validation, ICST 2013 - Luxembourg, Luxembourg Duration: 2013 May 18 → 2013 May 20

Other

Other	IEEE 6th International Conference on Software Testing, Verification and Validation, ICST 2013
Country/Territory	Luxembourg
City	Luxembourg
Period	13/5/18 → 13/5/20

Keywords

ACSR
Formal Verification
SDN
UPPAAL

ASJC Scopus subject areas

Software

Access to Document

10.1109/ICST.2013.69

Cite this

@conference{8c0af85b49c74b7db5f422ed1f68b6b7,

title = "Formal modeling and verification of SDN-OpenFlow",

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 = "ACSR, Formal Verification, SDN, UPPAAL",

author = "Miyoung Kang and Kang, {Eun Young} and Hwang, {Dae Yon} and Kim, {Beom Jin} and Nam, {Ki Hyuk} and Shin, {Myung Ki} and Choi, {Jin Young}",

year = "2013",

doi = "10.1109/ICST.2013.69",

language = "English",

pages = "481--482",

note = "IEEE 6th International Conference on Software Testing, Verification and Validation, ICST 2013 ; Conference date: 18-05-2013 Through 20-05-2013",

}

TY - CONF

T1 - Formal modeling and verification of SDN-OpenFlow

AU - Kang, Miyoung

AU - Kang, Eun Young

AU - Hwang, Dae Yon

AU - Kim, Beom Jin

AU - Nam, Ki Hyuk

AU - Shin, Myung Ki

AU - Choi, Jin Young

PY - 2013

Y1 - 2013

N2 - 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

AB - 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

KW - ACSR

KW - Formal Verification

KW - SDN

KW - UPPAAL

UR - http://www.scopus.com/inward/record.url?scp=84883321148&partnerID=8YFLogxK

U2 - 10.1109/ICST.2013.69

DO - 10.1109/ICST.2013.69

M3 - Paper

AN - SCOPUS:84883321148

SP - 481

EP - 482

T2 - IEEE 6th International Conference on Software Testing, Verification and Validation, ICST 2013

Y2 - 18 May 2013 through 20 May 2013

ER -

Formal modeling and verification of SDN-OpenFlow

Abstract

Other

Keywords

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this