верифікація, верификация ; телекомунікаційні протоколи, телекоммуникационные протоколы ; темпоральні логіки, темпоральные логики ; формальні граматики, формальные грамматики ; Transmission Control Protocol, TCP ; Session Initiation Protocol, SIP ; Real-time Transport Protocol, RTP ; Open Systems Interconnection, OSI ; Model Checking ; Media Gateway Control Protocol, MGCP ; Leaner Temporal Logic, LTL ; International Organization for Standardization, ISO ; Institute of Electrical and Electronics Engineers, IEEE ; E-networks

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

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