Abstract: Methods and mathematical tools for formalization analysis and verification of SoftwareDefined? Network protocols are suggested in the paper. E-networks apparatus and linear temporal logics are proposed to be used as mathematical tools for modeling and analysis. These mathematical tools can be transparently used to analyze critical requirements and properties of Software-Defined? Networks implementation - OpenFlow? protocol. The suggested methodology is based on the modeling approach and sequence analysis of changes of OpenFlow? protocol elements states. Apparatus of E-networks models the element states of SDN implementation. Such approach allows taking into account the asynchronous nature of complex processes in OpenFlow? protocol and performing stateful inspection. The use of models of E-network allows analyzing such properties as reachability, boundedness, liveliness, find loops and deadlock. The given mathematical method also allows finding difference between specification and designed networks. The method is based on the verification of temporal logic within the context of relationships of satisfaction. Using temporal logic formalisms allows to analysis and verify inconsistent of specification’s requirements. For this purpose formalism was designed that allows checking out the requirements form different specification versions of OpenFlow? protocol.

Keywords: Opеnflow, FlowVisor?, slice, Е-network, temporal logic

ACM Classification Keywords: C.2.1 Network Architecture and Design - Network communications

Link:

MATHEMATICAL METHODS FOR ANALYSIS OF SOFTWARE-DEFINED NETWORKS

Tkachova Olena, Issam Saad, Mohammed Jamal Salim

http://www.foibg.com/ijitk/ijitk-vol09/ijitk09-02-p02.pdf