Институт системного программирования им. В.П. Иванникова РАН


Формальная модель и задачи верификации программно-конфигурируемых сетей.

Авторы

Захаров В.А., Смелянский Р.Л., Чемерицкий Е.В.

Аннотация

Программно-коммутируемые сети (ПКС) - это класс компьютерных телекоммуникационных сетей, появившийся несколько лет назад в стремлении упростить проектирование и повысить гибкость управления сетями за счет разделения потоков данных (пакетов) и потоков управления (сообщений и команд), циркулирующие в сетях. ПКС представляет собой распределенную систему, в которой один или несколько контроллеров управляют множеством сетевых коммутаторов, обеспечивающих продвижение пакетов по каналам сети. Функциональные возможности и порядок взаимодействия коммутаторов и контроллеров ПКС определяются протоколом OpenFlow. На основе аппарата булевых функций и дискретных преобразователей нами предложена формальная модель ПКС, введен прототип формального языка спецификаций, поставлены задачи верификации моделей ПКС и получены оценки их сложности. Для одной из задач верификации моделей ПКС описан метод ее решения, на основе которого разработано программно-инструментальное средство верификации ПКС.

Полный текст статьи в формате pdf

Ключевые слова

программно-конфигурируемая сеть, коммутатор, контроллер, правило коммутации, пакет, формальная модель, спецификация, верификация моделей

Издание

Моделирование и анализ информационных систем, 2013, том 20, № 6, с. 33-48.

Научная группа

Теоретическая информатика

Все публикации за 2013 год Все публикации