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