верифікація, верификация ; розподілені системи, распределенные системы ; телекомунікаційні протоколи, телекоммуникационные протоколы ; OpenFlow

Застосування алгебри розподілених комутаційних ресурсів у якості інструменту побудови специфікації дозволяє виявити протиріччя між твердженнями специфікації. Задачу аналізу реалізації протоколу запропоновано звести до розв'язання задач перевірки відповідності таких функціональних та нефункціональних властивостей OpenFlow протоколу, як обмеженість, жвавість, досяжність, безпечність, покриваємість. З метою автоматизації процесу побудови моделі протоколу розроблений метод синтезу моделі Е-мережі за ACSR формалізмами тверджень специфікації. Запропоновано новий метод верифікації протоколів управління, в основу якого покладено класичний підхід «перевірки на моделях». Процес верифікації у випадку використання запропонованого методу базується на послідовній перевірці відповідності гілок дерева досяжності Е-мережі моделі реалізації та специфікації протоколу OpenFlow. На основі часткових розроблених методів сформовано комплексну методику аналізу та верифікації протоколів управління у програмно-конфігурованих мережах.

• УДК // Загальні питання електрозв' язку. Кібернетика.Теорія інформації. Теорія сигналів стосовно електрозв' язку