ИСТИНА

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