English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

Software Defined Network (SDN) is an emerging architecture of computer networking. The most important feature of SDN is that it separates the control plane from the data plane. OpenFlow is considered as the first and currently most popular standard southbound interface of SDN. It is a communication protocol which enables the SDN controller to directly interact with the forwarding plane. The widespread use makes the reliability of OpenFlow important. The OpenFlow bundle mechanism is a new mechanism proposed by OpenFlow protocol to guarantee the completeness and consistency of the messages transmitted between SDN switches and controllers during the communication process. Due to the requirement of reliability and security of OpenFlow, we think that it is of great significance to formally analyze and verify the safety-relevant properties of the mechanism. In this paper, we apply Communication Sequential Processes (CSP) and the model checker Process Analysis ToolKit (PAT) to model and verify the OpenFlow bundle mechanism. Our formalization and verification show that the mechanism can satisfy four properties: deadlock freeness, parallelism, atomicity and order property, from which we can conclude that the mechanism offers a better way to guarantee the completeness and consistency. Keywords—OpenFlow; Bundle Mechanism; Formalization; Verification

Formalization and Verification of the OpenFlow Bundle Mechanism Using CSP