Коровченко, О. Б.2016-07-182016-07-182011Коровченко О. Б. Моделі і методи аналізу та верифікації телекомунікаційних протоколів на основі е-мереж та формальних граматик : автореф. дис. ... канд. техн. наук : 05.12.02 "Телекомунікаційні системи та мережі" / О. Б. Коровченко ; МОНМС України, Харк. нац. ун-т радіоелектроніки. – Х. : ХНУРЕ, 2011. – 19 с.http://openarchive.nure.ua/handle/document/1551Дисертаційну роботу присвячено розв’язанню задачі підвищення ефективності існуючих методів аналізу і верифікації телекомунікаційних протоколів шляхом розробки математичних моделей та методів аналізу на різних етапах життєвого циклу протоколу. Розроблено ряд методів, що дозволяють скоротити вірогідність виникнення помилок та скоротити їх вплив на різних етапах розробки протоколів. У якості формалізації специфікації запропоновано використання формул темпоральної логіки, що дозволяють однозначно інтерпретувати твердження специфікації та враховувати причинно-послідовні між ними. Застосування формул темпоральної логіки в якості математичного апарату побудови специфікації дозволяє виявити протиріччя, що мають місце у специфікації. Розроблено метод аналізу основних алгоритмічних властивостей Е-моделі протоколу, що базується на застосуванні формальних граматик. Доведено, що застосування формальних граматик дозволяє розв’язати задачу аналізу таких властивостей протоколу, як обмеженість, досяжність, живість, збережуваність, а також, на відміну від існуючих методів виявити факт та причини виникнення зациклювань. У якості апарату моделювання телекомунікаційних протоколів запропоновано використання апарату Е-мереж. Уперше розроблено метод синтезу формальної граматики по моделі протоколу, що побудована за допомогою апарату Е-мереж. Запропоновано модифікацію методу верифікації «перевірка на моделях» (Model Checking), яка базується на використанні формальних граматик і дозволяє уникнути ефекту «комбінаторного вибуху» простору стані при проведенні верифікації. У рамках пошуку засобу усунення розбіжностей між реалізацією протоколу та його специфікацією запропоновано метод побудови контрприкладу, який дозволяє виявити поведінку протоколу, яка призводить до розбіжності зі специфікацією. As the proposed formalization of the specification using temporal logic formulas that allow one to interpret the specifications and take into account the statement of cause and consistent between them. The use of temporal logic formulas as a mathematical representation of the device specification makes it possible to identify the contradictions that are inherent in the specification. Developed a method for analyzing the basic algorithmic properties of the protocol model, based on the use of formal grammars. It is proved that the use of formal grammar allows more rigorous analysis of properties of the model protocol, as the limitations, accessibility, agility, safety, and, unlike existing techniques to identify the fact and cause of the loop. As the machine simulation of telecommunication protocols proposed to use the E-machine networks. For the first time developed a method for synthesizing a grammar for the protocol model, constructed using the apparatus of the E-networks. A modification of the method of verification Model Checking, based on the use of formal grammar as a verifier. Using this formalism allows to avoid the effect of "combinatorial explosion" of the state space during verification. In the search for ways to resolve differences between the implementation of the protocol and its specification a method of constructing a counter example that reveals the behavior of the Protocol, which leads to a discrepancy with the specification. Obtained results were applied in scientific-research projects with communication statements as well as in the teaching of students.ukтелекомунікаційний протоколЕ-мережаформальні граматикиверифікація протоколівтемпоральні логікиtelecommunications protocolE-netformal grammarsverification protocolstemporal logicOther