Конференция «Инструменты и методы анализа программ – 2013»

Верификация программно-конфигурируемых сетей при помощи системы UPPAAL

В. В. Подымов, У. В. Попеско

Московский государственный университет им. М. В. Ломоносова

Аннотация: В последние несколько лет активное развитие получили программно-конфигурируемые сети (ПКС) – особый вид компьютерных сетей, в которых все коммутирующие устройства имеют централизованное управление. В статье изучены задачи формального описания и верификации ПКС. Для описания ПКС использована библиотека элементов UML в редакторе диаграмм Dia. Для верификации ПКС использовано программно-инструментальное средство UPPAAL. Основной результат исследований – разработка транслятора, позволяющего по диаграмме сети получить ее модель для верификации в виде сети конечных временных автоматов. Корректность трансляции строго обоснована. Проведен ряд экспериментов, показывающих применимость предложенного метода верификации для проверки свойств поведения ПКС, специфицированных посредством формул темпоральной логики реального времени.

Ключевые слова: программно-конфигурируемая сеть, верификация, временные автоматы, темпоральная логика.

УДК: 519.7