UDC 004.72
K. I. Nikishin, PhD (Tech.), senior lecturer, department of computer science, PSU, Penza, Russia;
orcid.org/0000-0001-7966-7833, e-mail: This email address is being protected from spambots. You need JavaScript enabled to view it.
The complexity of managing Ethernet switches, routing tables and other network parameters allowed us to offer the technology of Software Defined Networks (SDN). The switches and the SDN controller communicate via the OpenFlow protocol, which is responsible for receiving and transmitting traffic and updating flow tables. The article discusses modeling and verification of the SDN controller, OpenFlow, Flow tables. The aim of the research is to study and build a frame transmission model in SDN networks, study and build models of a controller and entire SDN network system with multiple switches and end nodes hosts and work with the Flow Table using Petri nets. The objectives of the research are to study behavioral and temporal functioning of various models of SDN networks, as well as their verification using invariants. The developed models made it possible to verify SDN network algorithms during traffic transmission, controller and switch operation in the SDN network and the OpenFlow protocol.
Key words: Software Defined Networks, controller, switch, Ethernet, OpenFlow, invariants, Flow Table, Petri Nets, CPN Tools.