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

Résultats de recherche: Contribution dans un livre/un catalogue/un rapport/dans les actes d'une conférenceArticle dans les actes d'une conférence/un colloque

Résumé

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

langue originaleAnglais
titreProceedings - IEEE 6th International Conference on Software Testing, Verification and Validation, ICST 2013
Pages481-482
Nombre de pages2
Les DOIs
étatPublié - 9 sept. 2013
EvénementIEEE 6th International Conference on Software Testing, Verification and Validation, ICST 2013 - Luxembourg, Luxembourg
Durée: 18 mai 201320 mai 2013

Une conférence

Une conférenceIEEE 6th International Conference on Software Testing, Verification and Validation, ICST 2013
PaysLuxembourg
La villeLuxembourg
période18/05/1320/05/13

Empreinte digitale

Computer simulation
Specifications
Network architecture
Flow control
Software defined networking
Controllers

Citer ceci

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. Dans Proceedings - IEEE 6th International Conference on Software Testing, Verification and Validation, ICST 2013 (p. 481-482). [6569764] https://doi.org/10.1109/ICST.2013.69
Kang, Miyoung ; Kang, Eun-Young ; Hwang, Dae Yon ; Kim, Beom Jin ; Nam, Ki Hyuk ; Shin, Myung Ki ; Choi, Jin Young. / Formal modeling and verification of SDN-OpenFlow. Proceedings - IEEE 6th International Conference on Software Testing, Verification and Validation, ICST 2013. 2013. p. 481-482
@inproceedings{201587a73ce04e36826a560947218dc8,
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 Eun-Young Kang and Hwang, {Dae Yon} and Kim, {Beom Jin} and Nam, {Ki Hyuk} and Shin, {Myung Ki} and Choi, {Jin Young}",
year = "2013",
month = "9",
day = "9",
doi = "10.1109/ICST.2013.69",
language = "English",
pages = "481--482",
booktitle = "Proceedings - IEEE 6th International Conference on Software Testing, Verification and Validation, ICST 2013",

}

Kang, M, Kang, E-Y, Hwang, DY, Kim, BJ, Nam, KH, Shin, MK & Choi, JY 2013, Formal modeling and verification of SDN-OpenFlow. Dans Proceedings - IEEE 6th International Conference on Software Testing, Verification and Validation, ICST 2013., 6569764, p. 481-482, IEEE 6th International Conference on Software Testing, Verification and Validation, ICST 2013, Luxembourg, Luxembourg, 18/05/13. https://doi.org/10.1109/ICST.2013.69

Formal modeling and verification of SDN-OpenFlow. / Kang, Miyoung; Kang, Eun-Young; Hwang, Dae Yon; Kim, Beom Jin; Nam, Ki Hyuk; Shin, Myung Ki; Choi, Jin Young.

Proceedings - IEEE 6th International Conference on Software Testing, Verification and Validation, ICST 2013. 2013. p. 481-482 6569764.

Résultats de recherche: Contribution dans un livre/un catalogue/un rapport/dans les actes d'une conférenceArticle dans les actes d'une conférence/un colloque

TY - GEN

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/9/9

Y1 - 2013/9/9

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 - Conference contribution

AN - SCOPUS:84883321148

SP - 481

EP - 482

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

ER -

Kang M, Kang E-Y, Hwang DY, Kim BJ, Nam KH, Shin MK et al. Formal modeling and verification of SDN-OpenFlow. Dans Proceedings - IEEE 6th International Conference on Software Testing, Verification and Validation, ICST 2013. 2013. p. 481-482. 6569764 https://doi.org/10.1109/ICST.2013.69