УДК 004.72
МОДЕЛИРОВАНИЕ КОНТРОЛЛЕРА И ВЕРИФИКАЦИЯ ПРОЦЕССА ПЕРЕДАЧИ ДАННЫХ В ПРОГРАММНО-КОНФИГУРИРУЕМЫХ СЕТЯХ
К. И. Никишин, к.т.н., старший преподаватель кафедры ВТ ПГУ, Пенза, Россия;
orcid.org/0000-0001-7966-7833, e-mail: Этот адрес электронной почты защищён от спам-ботов. У вас должен быть включен JavaScript для просмотра.
Сложность управления коммутаторов Ethernet, таблиц маршрутизации и других сетевых
параметров позволило предложить технологию программно-конфигурируемых сетей (ПКС). Коммутаторы и контроллер ПКС общаются через OpenFlow протокол, который отвечает за приём и передачу трафика и обновление потоковых таблиц. В статье рассматривается моделирование и верификация контроллера ПКС, потоковые таблицы OpenFlow протокола. Цель исследования – исследование и построение модели передачи кадра в ПКС, исследование и построение моделей контроллера и всей системы ПКС с несколькими коммутаторами и конечными узлами хостами и работой с таблицей Flow Table с использованием сетей Петри. Задачами исследования являются исследование поведенческого и временного функционирования различных моделей ПКС, а также их верификация с помощью инвариантов. Разработанные модели позволили верифицировать алгоритмы ПКС при передачи трафика, работе контроллера и коммутаторов в ПКС по протоколу OpenFlow.
Ключевые слова: программно-конфигурируемые сети, контроллер, коммутатор, Ethernet, OpenFlow, инварианты, Flow Table, сети Петри, CPN Tools.