Process algebraic specification of software defined networks

Miyoung Kang, Junkil Park, Jin Young Choi, Ki Hyuk Nam, Myung Ki Shin

Research output: Chapter in Book/Report/Conference proceedingConference contribution

3 Citations (Scopus)

Abstract

In this paper, we first present a formal specification for a part of Software Defined Networks(SDN) using a process algebra called Algebra of Communicating Shard Resources(ACSR). To provide a correct and efficient solution for forwarding packets on the Software Defined Networks, ACSR can express processes running concurrently and communicating switches and a controller. Forwarding packets can be modeled as prioritized synchronization of events in ACSR. During specifying formally, we could find the Subtle Ambiguity in the SDN specification. The central contribution of this paper is to describe how to apply a formal specification method to a part of informal SDN specification. It is important to specify SDN and verify the properties of the SDN using formal specification before implementing the systems. Furthermore, we prove the correctness of ACSR specification to show deadlockfreeness using VERSA.

Original languageEnglish
Title of host publicationProceedings - 2012 4th International Conference on Computational Intelligence, Communication Systems and Networks, CICSyN 2012
Pages359-363
Number of pages5
DOIs
Publication statusPublished - 2012 Oct 17
Event2012 4th International Conference on Computational Intelligence, Communication Systems and Networks, CICSyN 2012 - Phuket, Thailand
Duration: 2012 Jul 242012 Jul 26

Other

Other2012 4th International Conference on Computational Intelligence, Communication Systems and Networks, CICSyN 2012
CountryThailand
CityPhuket
Period12/7/2412/7/26

Fingerprint

Algebra
Specifications
Synchronization
Switches
Controllers
Formal specification

Keywords

  • Formal Specification
  • Future Internet
  • OpenFlow
  • SDN

ASJC Scopus subject areas

  • Artificial Intelligence
  • Computer Networks and Communications

Cite this

Kang, M., Park, J., Choi, J. Y., Nam, K. H., & Shin, M. K. (2012). Process algebraic specification of software defined networks. In Proceedings - 2012 4th International Conference on Computational Intelligence, Communication Systems and Networks, CICSyN 2012 (pp. 359-363). [6274368] https://doi.org/10.1109/CICSyN.2012.72

Process algebraic specification of software defined networks. / Kang, Miyoung; Park, Junkil; Choi, Jin Young; Nam, Ki Hyuk; Shin, Myung Ki.

Proceedings - 2012 4th International Conference on Computational Intelligence, Communication Systems and Networks, CICSyN 2012. 2012. p. 359-363 6274368.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Kang, M, Park, J, Choi, JY, Nam, KH & Shin, MK 2012, Process algebraic specification of software defined networks. in Proceedings - 2012 4th International Conference on Computational Intelligence, Communication Systems and Networks, CICSyN 2012., 6274368, pp. 359-363, 2012 4th International Conference on Computational Intelligence, Communication Systems and Networks, CICSyN 2012, Phuket, Thailand, 12/7/24. https://doi.org/10.1109/CICSyN.2012.72
Kang M, Park J, Choi JY, Nam KH, Shin MK. Process algebraic specification of software defined networks. In Proceedings - 2012 4th International Conference on Computational Intelligence, Communication Systems and Networks, CICSyN 2012. 2012. p. 359-363. 6274368 https://doi.org/10.1109/CICSyN.2012.72
Kang, Miyoung ; Park, Junkil ; Choi, Jin Young ; Nam, Ki Hyuk ; Shin, Myung Ki. / Process algebraic specification of software defined networks. Proceedings - 2012 4th International Conference on Computational Intelligence, Communication Systems and Networks, CICSyN 2012. 2012. pp. 359-363
@inproceedings{093bbdb19fe848d7954f510cabb340d2,
title = "Process algebraic specification of software defined networks",
abstract = "In this paper, we first present a formal specification for a part of Software Defined Networks(SDN) using a process algebra called Algebra of Communicating Shard Resources(ACSR). To provide a correct and efficient solution for forwarding packets on the Software Defined Networks, ACSR can express processes running concurrently and communicating switches and a controller. Forwarding packets can be modeled as prioritized synchronization of events in ACSR. During specifying formally, we could find the Subtle Ambiguity in the SDN specification. The central contribution of this paper is to describe how to apply a formal specification method to a part of informal SDN specification. It is important to specify SDN and verify the properties of the SDN using formal specification before implementing the systems. Furthermore, we prove the correctness of ACSR specification to show deadlockfreeness using VERSA.",
keywords = "Formal Specification, Future Internet, OpenFlow, SDN",
author = "Miyoung Kang and Junkil Park and Choi, {Jin Young} and Nam, {Ki Hyuk} and Shin, {Myung Ki}",
year = "2012",
month = "10",
day = "17",
doi = "10.1109/CICSyN.2012.72",
language = "English",
isbn = "9780769548210",
pages = "359--363",
booktitle = "Proceedings - 2012 4th International Conference on Computational Intelligence, Communication Systems and Networks, CICSyN 2012",

}

TY - GEN

T1 - Process algebraic specification of software defined networks

AU - Kang, Miyoung

AU - Park, Junkil

AU - Choi, Jin Young

AU - Nam, Ki Hyuk

AU - Shin, Myung Ki

PY - 2012/10/17

Y1 - 2012/10/17

N2 - In this paper, we first present a formal specification for a part of Software Defined Networks(SDN) using a process algebra called Algebra of Communicating Shard Resources(ACSR). To provide a correct and efficient solution for forwarding packets on the Software Defined Networks, ACSR can express processes running concurrently and communicating switches and a controller. Forwarding packets can be modeled as prioritized synchronization of events in ACSR. During specifying formally, we could find the Subtle Ambiguity in the SDN specification. The central contribution of this paper is to describe how to apply a formal specification method to a part of informal SDN specification. It is important to specify SDN and verify the properties of the SDN using formal specification before implementing the systems. Furthermore, we prove the correctness of ACSR specification to show deadlockfreeness using VERSA.

AB - In this paper, we first present a formal specification for a part of Software Defined Networks(SDN) using a process algebra called Algebra of Communicating Shard Resources(ACSR). To provide a correct and efficient solution for forwarding packets on the Software Defined Networks, ACSR can express processes running concurrently and communicating switches and a controller. Forwarding packets can be modeled as prioritized synchronization of events in ACSR. During specifying formally, we could find the Subtle Ambiguity in the SDN specification. The central contribution of this paper is to describe how to apply a formal specification method to a part of informal SDN specification. It is important to specify SDN and verify the properties of the SDN using formal specification before implementing the systems. Furthermore, we prove the correctness of ACSR specification to show deadlockfreeness using VERSA.

KW - Formal Specification

KW - Future Internet

KW - OpenFlow

KW - SDN

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

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

U2 - 10.1109/CICSyN.2012.72

DO - 10.1109/CICSyN.2012.72

M3 - Conference contribution

AN - SCOPUS:84867378780

SN - 9780769548210

SP - 359

EP - 363

BT - Proceedings - 2012 4th International Conference on Computational Intelligence, Communication Systems and Networks, CICSyN 2012

ER -