Mathematical tools for SDN formalisation and verification

This paper is devoted to analysis of existing components and architecture of Software-Defined Networks. The main features of SDN and components interaction are considered. Based on the results we propose formalisms that define rules coordination and interaction of the main components and controls SDN architecture. The methodology and mathematical tools for formalization and verifying OpenFlow protocol are suggested. This methods can be transparently used to analyze critical requirements and properties prior to system implementation. For analysis and verification of OpenFlow protocol was designed formalism that allows checking out the requirements form different specification versions of OpenFlow protocol.