Предложен новый подход к верификации протоколов управления, в основу которого положен классический метод "проверки на моделях". Процесс верификации в данном случае базируется на последовательной проверке соответствия ветвей дерева достижимости Е-сети модели реализации и ветвей дерева достижимости спецификации протокола OpenFlow. Разработан алгоритм формирования контрпримера, который обеспечивает вывод и позволяет локализировать последовательность состояний модели реализации протокола, приводящих к возникновению ошибок. Сформировано несколько сценариев процесса верификации: частичная верификация на основе шаблонов и полная верификация реализации протокола. Применение такого подхода позволяет уменьшить вероятность возникновения эффекта "комбинаторного взрыва" пространства состояний. Ha основе частных моделей и методов сформирована комплексная методика анализа и верификации протоколов управления в программно-конфигурируемых сетях.