Issam S. The models and methods for analysis and verification control protocols in Software-Defined Networks based on apparatus of algebra communication shared resources and reachability graphs

The object - the design, analysis and verification of OpenFlow protocol. Methods - algebra communication distributed resources, the E-networks, graph theory, formal methods of verification, set theory. Results - first proposed the application of mathematical apparatus of the algebra of communication shared resources, distributed resources with a view to formalizing the requirements of the contradiction specifications; development apparatus E-networks through the use of runing transition in modeling the functional properties of the OpenFlow protocol and implementation of quantitative values of the attributes of transitions; development of a method of verification, which eliminates the effect of "combinatorial explosion" of space study states. Implemented - in the educational process of the Kharkiv National University of Radio Electronics, during the execution of the state research work № 299-1. Sphere of application - telecommunication networks