Решение задачи диссертационного исследования состоит в повышении эффективности методов анализа телекоммуникационных протоколов за счет использования математических средств и метода верификации, который основывается на аппарате E-сетей и формальных грамматиках. Применение формул темпоральной логики в качестве математического аппарата позволяет выявить противоречия, возникающие при формировании спецификации на подмножестве естественного языка. Разработан метод анализа основных алгоритмических свойств моделей телекоммуникационных протоколов, базирующийся на применении формальных грамматик. Благодаря применению формальных грамматик удалось визуализировать возможные сценарии поведения протокола. Впервые разработан метод синтеза формальной грамматики по модели E-сети. Предложена модификация метода верификации "проверка на моделях" (Model Checking), которая основывается на использовании формальных грамматик в качестве средства верификации.