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
N1 - Copyright:
Copyright 2012 Elsevier B.V., All rights reserved.
PY - 2012
Y1 - 2012
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
T3 - Proceedings - 2012 4th International Conference on Computational Intelligence, Communication Systems and Networks, CICSyN 2012
SP - 359
EP - 363
BT - Proceedings - 2012 4th International Conference on Computational Intelligence, Communication Systems and Networks, CICSyN 2012
T2 - 2012 4th International Conference on Computational Intelligence, Communication Systems and Networks, CICSyN 2012
Y2 - 24 July 2012 through 26 July 2012
ER -