Опис документа

В роботі розв'язуються задачі підвищення ефективності існуючих методів аналізу і верифікації телекомунікаційних протоколів шляхом розробки математичних моделей та методів аналізу на різних етапах життєвого циклу протоколу. Розроблено методи, що дозволяють скоротити вірогідність виникнення помилок та скоротити їх вплив на різних етапах розробки протоколів. У якості формалізації специфікації запропоновано використання формул темпоральної логіки, що дозволяють однозначно інтерпретувати твердження специфікації та враховувати причинно-послідовні міх ними. Застосування формул темпоральної логіки в якості математичного апарату побудови специфікації дозволяє виявити протиріччя, що мають місце у специфікації. Розроблено метод аналізу основних алгоритмічних властивостей Е-моделей протоколу, що базується на застосуванні формальних граматик. Доведено, що застосування формальних граматик дозволяє розв'язати задачу аналізу таких властивостей протоколу, як обмеженість, досяжність, живість, збережуваність, а також, на відміну від існуючих методів виявити факт та причини виникнення за циклювань. У якості апарату моделювання телекомунікаційних протоколів запропоновано ви користування Е-мереж. Розроблено метод синтезу формальної граматики по моделі протоколу, що побудована за допомогою апарату Е-мереж. Запропоновано модифікацію методу верифікації "перевірка на моделях" (Model Checking), яка базується на використанні формальних граматик і дозволяє уникнути ефекту "комбінаторного вибуху" простору стані при проведенні верифікації. У рамках пошуку засобу усунення розбіжностей між реалізацією протоколу та його специфікацією запропоновано метод побудови контр прикладу, який дозволяє виявити поведінку протоколу, яка призводить до розбіжності зі специфікацією. Отримані в дисертації результати були застосовані при виконанні НДР і в учбовому процесі.