2. Отримали подальший розвиток алгебраїчні методи аналізу телекомунікаційних протоколів, новизна полягає у використанні формальних граматик, що дозволило вирішити задачу перевірки коректності поведінки та оцінки якості розподілу ресурсів телекомунікаційними протоколами.

3. Вперше розроблено метод верифікації телекомунікаційних протоколів, що дозволяє не тільки виділити набір станів, що не задовольняють специфікації, але й на основі побудови контрприкладу визначити необхідний набір змін у реалізації протоколу, щодо усунення невідповідності специфікації.

Практичне значення одержаних результатів. Практичне значення результатів досліджень полягає в тому, що запропоновані математичні моделі і методи можуть бути використані при створенні програмного середовища, підтримки, проектування та розробки телекомунікаційних протоколів. Запропонована методика була використана для перевірки коректності поведінки протоколу балансування загрузки сегмента мережі; пошуку помилок при сумісному функціонуванні різних версій протоколу ТСР; пошуку протиріч між реалізаціями протоколу RTP та верифікації протоколу Megaco/H.248. Крім того, результати дисертації використані в ході виконання науково-дослідної роботи №235-1 "Методи проектування телекомунікаційних мереж NGN та управління їх ресурсами" (№ДР 0109U000662), в якій дисертант виступав співвиконавцем.

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

Особистий внесок здобувача. Всі основні наукові результати, висвітлені в дисертаційній роботі, здобувач отримав самостійно. Крім того, в роботі [1] автором проведено аналіз основних критеріїв якості сучасних телекомунікаційних систем, зокрема IP-мереж. У роботі [2] здобувачем запропоновані модель протоколу TCP, побудована за допомогою апарата Е-мереж, та запропоновано використання формальних граматик як одного з методів структурного аналізу моделей телекомунікаційних протоколів; в роботі [3] автором запропонована використання формальних граматик для верифікації телекомунікаційних протоколів, запропонований метод дозволяє вдосконалити процес верифікації та зменшити вірогідність виникнення ефекту "комбінаторного вибуху" ; в роботі [4] автором розроблено метод синтезу формальних граматик на основі моделі протоколу, побудованої на базі апарату Е-мереж та проведено структурний аналіз протоколу балансування загрузки фрагменту мережі; у статті [5] здобувачем розроблено метод верифікації телекомунікаційних протоколів та проведено верифікацію протоколу TCP з його реалізацією у Unix-подібних мережах на стадії встановлення з'єднання .

Апробація результатів дисертації. Основні результати дисертації доповідались і були схвалені на наступних науково-технічних конференціях та семінарах: 12-му, 13-му, 14-му, 15-му Міжнародних молодіжних форумах "Радіоелектроніка та молодь у ХХІ сторіччі" (м. Харків, ХНУРЕ 2008-2011); 3-му Міжнародному радіоелектронному форумі "Прикладна радіоелектроніка. Стан та перспективи розвитку" МРФ-2008 (Харків, АНПРЕ, ХНУРЕ, 2008), науково-технічній конференції "Компьютерное моделирование в наукоемких технологиях" (м. Харків, ХНУ, 2010), 9-й Міжнародній науково-технічній конференції "Перспективные технологии в средствах передачи информации" (Володимир, Володим. держ. університет, 2011).

Публікації. За темою дисертації автором опубліковано 12 наукових праць, які включають 5 наукових статей та 7 тез доповідей. Усі статті опубліковані в журналах та наукових збірках праць, що входять до переліку видань, дозволенних ВАК України для публікацій матеріалів дисертації з технічних наук.

Обсяг та структура роботи. Дисертація складається із вступу, чотирьох розділів, висновків, списку використаних джерел. Загальний обсяг дисертації складається із 168 сторінок, з них перелік використаних скорочень на 1 сторінці, списку використаної літератури зі 109 джерел на 10 сторінках. Дисертація містить 40 ілюстрацій, 4 таблиці.

2. Основний зміст роботи

У вступі розкрито стан проблеми, що досліджується, обґрунтовано актуальність теми дисертаційної роботи, сформульовано наукову задачу та визначено мету досліджень, представлено наукову новизну та практичне значення отриманих у роботі результатів. Наведено дані про публікації автора за темою дисертації.

У першому розділі сформульовані вимоги, до засобів та процесів розробки телекомунікаційних протоколів. Проведено дослідження існуючих проблем на кожному етапі життєвого циклу протоколу. На підставі проведених досліджень і аналізу виявлених проблем та їх чинників зроблено висновок про необхідність вирішення наукової задачі, що полягає в розробці методики аналізу та верифікації телекомунікаційних протоколів, яка дозволить підвищити ефективність методів аналізу телекомунікаційних протоколів за рахунок використання алгебраїчних засобів та методу верифікації, що базуються на Е-мережах та формальних граматиках.

Для підвищення ефективності процесу розробки та підтримки телекомунікаційних протоколів запропоновано використання каскадної моделі життєвого циклу протоколу. Відмінною властивістю каскадної моделі є те, що вона представляє собою формальний метод і складається з незалежних фаз, які виконуються послідовно. Відповідно до такої моделі кожна фаза має закінчуватися процедурами перевірки, що сприяє виявленню помилок на більш ранніх етапах, коли їх усунення вимагає відносно невеликих витрат.

Як показують результати дослідження, найбільша кількість помилок виникає на етапі збору вимог приблизно 14% від загальної кількості та при створенні специфікації протоколів - більш ніж 44%. Аналіз існуючих методів, що дозволяють розв'язати дану проблему дозволив встановити, що найбільш придатним засобом усунення помилок є формальне представлення специфікації. Формалізація специфікації дозволяє однозначно представити вимоги щодо протоколу, провести їх аналіз та виявити можливі суперечності. Аналіз засобів, що використовуються для формалізації специфікації телекомунікаційних протоколів показав, що найбільш ефективним методом є алгебраїчне представлення специфікації за допомогою темпоральних логік. Темпоральні логіки дозволяють чітко визначати причинно-наслідкові зв'язки між процесами, що відбуваються при функціонуванні протоколу, врахувати їх можливу паралельну природу, а також встановити хронологію їх появи, що є важливим при розробці алгоритму роботи протоколу. Використання методів аналізу темпоральних логік дозволяє виявити можливі протиріччя, що можуть міститься у специфікації.

Під час досліджень було встановлено, що помилки етапу реалізації протоколу можуть бути наслідками помилок кодування, компіляції та логічних помилок проектування, складають близько 16% від загальної кількості помилок. Логічні помилки призводять до непередбаченого розподілу ресурсів, некоректної поведінки протоколу, відсутності узгодженості при взаємодії з іншими системами та протоколами. Встановлено, що найбільш ефективним методом пошуку логічних помилок проектування є аналіз реалізації протоколів через модельний підхід. Аналіз існуючих засобів моделювання показав, що найбільш придатним математичним апаратом, для опису моделей телекомунікаційних протоколів є Е-мережі. Як апарат імітаційного моделювання Е-мережі дозволяють легко моделювати рівнобіжні взаємодіючі асинхронні процеси. Е-мережі допускають будь-яку змістовну інтерпретацію своїх складових, що дозволяє одночасно моделювати як інформаційні потоки, так і апаратну частину. Можливість використання різних рівнів абстракції (деталізації) дозволяє будувати ієрархічні моделі, у яких перехід може транслюватися в підмережу більш низького рівня деталізації. Зазначені особливості Е-мереж значно знижують суперечливість вимог щодо наочності й адекватності моделі протоколу, тим самим дозволяють вирішити задачу аналізу основних властивостей протоколу.

Аналіз помилок впровадження та сумісної роботи телекомунікаційних протоколів дозволив виявити, що їх загальна частка складає 26%, такі помилки є наслідком невідповідності реалізації протоколу його специфікації. Найбільш ефективним методом виявлення зазначених невідповідностей є верифікація. Встановлено, що існуючі методи верифікації мають ряд суттєвих недоліків, які полягають у трудомісткості процесу верифікації, визначенні обмеженої кількості помилок, "комбінаторного вибуху" простору станів та ін. З метою усунення недоліків запропонована розробка методу верифікації, що за рахунок послідовного аналізу станів, та використання алгебраїчних методів порівняння буде позбавлений вказаних недоліків.

У другому розділі в рамках розв'язання загальної задачі розроблено метод формалізації специфікації телекомунікаційних протоколів за допомогою темпоральних логік, метод синтезу Е-мережі по темпоральній логіці, що є формалізацією специфікації та метод аналізу реалізації протоколу за допомогою формальних граматик. Для перевірки коректності розроблених методів побудована формальна граматика, яка була використана підчас аналізу протоколу балансування навантаження в сегменті телекомунікаційної мережі.

Відповідно до рекомендацій ITU-T на етапах специфікації і проектування протоколи можуть бути наведені засобами підмножини природної мови, SDL або UML діаграм. Для розв'язання задачі коректної побудови семантично вірних формул лінійної темпоральної логіки, що повністю відповідають специфікації телекомунікаційного протоколу, наведеної як у вигляді тексту, так і заданої SDL та UML діаграмами, розроблено відповідний метод. Розроблений метод дозволяє в повній мірі формалізувати специфікацію телекомунікаційного протоколу.

В специфікації протоколу можливе існування суперечливих вимог, що призводять до непередбачуваних наслідків при функціонуванні. Для виявлення таких помилок запропоновано введення деяких визначень, на основі перевірки яких здійснюється рішення щодо суперечності тверджень специфікації. Кожна формула темпоральної логіки задається в термінах відношення виконання ().

Визначення 1. Формула темпоральної логіки задає відношення між станом і елементом формули , який має бути істинним в цьому стані (). При цьому істинно тоді і лише тоді, коли істинні всі в стані .

Визначення 2. Дві формули темпоральної логіки є несуперечливими, якщо не існує таких станів, для яких формули є взаємовиключними.

Наведені визначення складають основу методу перевірки на протиріччя. Визначення 1 дозволяє порівняти дві формули темпоральної логіки, що відносяться до одного стану протоколу, на підставі визначення істинності кожного стану робиться висновок їх непротиріччя.

Для вирішення задачі побудови моделі протоколу в вигляді Е-мережі, що відповідає його специфікації розроблено метод синтезу Е-мережі по формулам темпоральної логіки. В основі методу, що пропонується, покладено можливість трансляції темпоральних логік в кінцеві автомати і табличний метод перетворення формули темпоральної логіки в граф станів. У рамках розробленого методу кожна позиція Е-мережі описується множиною Node:

Node= [ID: NodeID, CURRENT: meaning of node;

INCOMING: previous node, GOING: next node],

де ID - унікальний ідентифікатор позиції; CURRENT - поточний елемент алфавіту темпоральної логіки, що відповідає одній із вершин; INCOMING - множина вхідних позицій (беруть участь у формуванні функції прямої інцидентності); GOING - множина вихідних позицій (беруть участь у формуванні функції прямої інцидентності).

Виявлено, що при встановленні відношення інцидентності між вершинами, можуть виникнути наступні варіанти взаємозв'язків:

1. Поточний стан передує лише одному стану. Зв'язок між елементами визначено логічною в'язкою слідування (). За даних умов вершини-позиції сполучаються за допомогою Т-переходу.

2. Поточний стан передує декільком станам. Зв'язок між елементами алфавіту визначається логічними операторами. Зв'язок між елементами алфавіту визначається логічними операторами кон'юнкції або диз'юнкції ( або ). За даних умов вершини-позиції сполучаються за допомогою F-переходу. У випадку якщо набору формул темпоральної логіки відповідає формула шляху, то потокові позиції, що розглядаються сполучаються за допомогою MY-переходу.

3. Декілька станів передують поточному стану. Зв'язок між елементами алфавіту визначається логічними операторами кон'юнкції або диз'юнкції ( або ). За даних умов вершини-позиції сполучаються за допомогою J-переходу. У випадку якщо набору формул темпоральної логіки відповідає формула шляху, то потокові позиції, що розглядаються, сполучаються за допомогою MХ-переходу.

Отже, запропоновані позначення кожної вершини моделі протоколу та огляд можливих взаємозв'язків дозволяє побудувати адекватну модель Е-мережі, що повністю відповідає формулам темпоральної логіки.

З метою перевірки коректності функціонування протоколу та оцінки розподілу використовуваних ресурсів виконується аналіз основних алгоритмічних властивостей Е-моделі протоколу: обмеженість, жвавість, досяжність, безпечність, консервативність, покриваємість.

Існуючі методи аналізу алгоритмічних властивостей Е-мереж, такі як дерево досяжності та матричні рівняння, не дозволяють вирішити задачу перевірки коректності поведінки та оцінки ефективності розподілу ресурсів протоколу. Отже, виникає необхідність у розробці нового методу, який в алгебраїчному вигляді наводить поведінку моделі протоколу, що дозволить протоколу вирішити вказані задачі. В якості методу аналізу моделей Е-мереж на обрані алгоритмічні властивості запропоновано використовувати формальні граматики.

Формальна граматика, що описує модель, побудовану на базі апарату Е-мережі, задається наступним чином:

, (1)

де множина термінальних символів є множиною станів телекомунікаційного протоколу, що моделюється вершинами-позиціями та вершинами-переходами , - символьне позначення вершин-переходів, - символьне позначення вершин-позицій, зазначено, що - позначення основних типів переходів Е-мереж, не є вершинами-позиціями, - непорожня множина нетермінальних символів, . Множина нетермінальних символів складається з елементів , де символ позначає об'єднання декількох повних ціпочок язика, які мають спільний початковий стан, містить множину значень атрибутів, що впливають на правила спрацьовування переходів, - символ, що вказує на тип переходу (), - символ розділення.

Запропоноване визначення формальної граматики дозволяє враховувати всі особливості класичної Е-мережі, а також враховувати наявність атрибутів переходів. Поділ термінальних і нетермінальних символів дозволяє виділити основні стани протоколу, що беруть участь у формуванні різних сценаріїв його поведінки та їх причини.

При формуванні Е-мережі, коли в якості вихідних даних використовуються алгоритми роботи протоколу, за основу прийняте визначення мов, розроблене для апарата мереж Петрі. У існуючи визначення внесено зміни, що дозволяють врахувати специфіку Е-мереж (наявність розходжень у топології й описі апарата і т.п.). Для аналізу поведінки телекомунікаційних протоколів запропоновано використовувати мову - типу, яка дозволяє виявляти тупикові та конфліктні ситуації в процесі функціонування протоколів.

Мова - типу задається як:

, (2)

де - послідовність переходів, що запускаються; - множина усіх строк із алфавіту , с порожнім ланцюгом включно.

Розроблений метод синтезу формальної граматики дозволяє однозначно відобразити кожний активний перехід відповідним до нього символом, що, в свою чергу, дозволяє однозначно інтерпретувати зміну станів моделі Е-мережі за допомогою символів алфавіту.

У загальному вигляді правила породження продукції , для кожного типу переходів Е-мереж може бути наведений наступним чином:

- правило для T-переходу:

телекомунікаційний мережа верифікація

,

(3)

- правило для F -переходу:

(4)

- правило для J-переходу:

,

. (5)

- правило для MX-переходу:

(6)

або

(7)

де .

- правило для MY-переходу:

, (8)

де .

Застосування формальних граматик як одного з методів аналізу та формалізації поведінки телекомунікаційних протоколів дозволило розв'язати такі задачі, як аналіз досяжності необхідного стану, що відповідають вимогам специфікації, встановити, чи збережені основні алгоритмічні властивості, а також, на відміну від інших методів, встановити факт виникнення зациклень у процесі функціонування протоколу, вирішення яких до цього часу було досить ускладнене.

Третій розділ присвячено розробці методу верифікації телекомунікаційних протоколів, який базується на використанні Е-моделі протоколу та формальних граматик.

Проведені дослідження дозволили встановити, що для верифікації телекомунікаційних протоколів найбільш поширеним є метод "перевірки на моделях". Безперечна перевага цього методу полягає у можливості перевірки не впровадженого протоколу, а його моделі, що дозволяє виявити більшу кількість помилок на етапі розробки та усунути можливість їх виникнення в процесі експлуатації. Проте, цей підхід має істотний недолік - ефект "комбінаторного вибуху", який пов'язаний з великою кількістю станів, що розглядаються, і у моделях сучасних протоколів можуть складати понад 100. Наявний недолік робить неможливим використання методів верифікації для телекомунікаційних протоколів.

Для розв'язання задачі верифікації прийнято рішення щодо розробки нового методу, що завдяки використанню формальних граматик та правил їх еквівалентності зводить процес верифікації до послідовної перевірки відповідності поведінки реалізації протоколу його специфікації. Структурна схем розробленого методу наведена на рис. 1.

Рис. 1. Структурна схема методу верифікації телекомунікаційних протоколів

Використання Е-моделей протоколів у якості вхідних даних методу дозволяє істотно скоротити час його реалізації тому, що у якості вхідних даних можуть бути використані перевірені моделі попередніх етапів життєвого циклу.

Розроблений метод верифікації телекомунікаційних протоколів базується на перевірці еквівалентності двох формальних граматик, що відображають поведінку протоколів.

Метод передбачає наступну послідовність дій:

1. Будується мова специфікації протоколу . , де - один або декілька поведінкових ланцюгів, що породжені з початкового стану.

2. Виконується покрокова побудова мови реалізації протоколу:

- визначається поточний стан моделі реалізації протоколу (на першому кроці поточним станом є );

- визначається множина активних переходів моделі реалізації ;

- формуються можливі поведінкові ланцюги для ряду активних переходів: .

3. Виконується порівняння побудованих ланцюгів для мови моделі реалізації протоколу з активними ланцюгами моделі специфікації відбувається наступним чином:

(9)

4. У випадку, якщо мова моделі реалізації протоколу еквівалентна мові, що отримано для моделі специфікації протоколу, моделі вважаються еквівалентними. У випадку, якщо ж мовні ланцюги не еквівалентні відбувається побудова контрприкладу, який дозволяє встановити зніми поведінки реалізацій протоколу, що призводять до виникнення помилки.

Таким чином запропонований метод дозволяє уникнути ефекту "комбінаторного вибуху" простору станів моделі, що розглядаються, за рахунок того, що порівняння двох формальних граматик базується на послідовній перевірці еквівалентності мовних ланцюгів, що побудовані відповідно для реалізації та специфікації протоколу. Для розв'язання задачі визначення дій, що призводять до виникнення помилок запропоновано метод побудови контрприкладу, що базується на алгоритму подвійного обходу та пошуку. Застосування даного алгоритму дозволяє в алгебраїчному вигляді описати причини невідповідної поведінки протоколу та визначити шляхи їх усунення.

У четвертому розділі на основі часткових методів сформульована й описана загальна методика аналізу та верифікації телекомунікаційних протоколів (рис. 2). Методика базується на засадах каскадного життєвого циклу та розроблених методах аналізу та верифікації. Проведено аналіз ефективності розробленої методики.

У рамках загальної методики сформовані цілі кожного окремого етапу, засоби, що використовуються та позначені результати, що передбачаються. Кожний етап методики може бути використаний як самостійний метод, що практично не пов'язаний з попередніми. Таке уявлення дозволяє протоколу виконувати аналіз як протоколів, що розробляються, так і вже існуючих.

Запропонована методика дозволяє:

· формалізувати специфікацію протоколу, що полегшує процес її аналізу та виявлення суперечностей у твердженнях специфікації;

· виконати перевірку коректності поведінки та оцінку розподілу ресурсів реалізацій протоколу безпосередньо підчас розробки протоколу за рахунок використання Е-мереж;

· здійснити аналітичний опис сценаріїв поведінки протоколу за допомогою формальних граматик для уточнення чи перевірки результатів імітаційного моделювання;

· скоротити час та зменшити множину станів протоколу, який аналізується.

Рис. 2. Методика аналізу та верифікації телекомунікаційних протоколів

Ефективність розробленої методики аналізу та верифікації телекомунікаційних протоколів оцінювалася шляхом порівняння загальної трудомісткості розробки, виміряною в нормогодинах (людина*час). Для вирішення задачі оцінки ефективності двом групам розробників було запропоновано проект, націлений на розробку протоколу, задачею якого є балансування трафіка у сегменті телекомунікаційної мережі. Перша група розробників в якості специфікації та вхідних даних для подальших етапів розробки використовувала діаграми класів SDL. Другій групі підчас розробки було запропоновано використання розробленої у роботі методики.

Після виконання проекту було проаналізовано дані щодо часу, витраченого на кожному з етапів життєвого циклу та визначено, що загальна кількість нормагодин, втрачених на розробку першою групою, склала 280, другою - 224. На рис. 3 наведено графік порівняння даних по загальній кількості нормогодин, що витрачені на кожному з етапів життєвого циклу.

Зазначено, що кількість часу, витраченого у процесі впровадження та верифікації була суттєво знижена (на етапі верифікації виграш склав 24 нормогодини, на етапі впровадження -25), це пов'язано з відсутністю зворотних зв'язків у розробленій методиці (рис.2). Отримані дані дозволили встановити, що використання розробленої методики аналізу та верифікації дозволяє підвищити ефективність розробки телекомунікаційних протоколів на 20%.

Також розглянуто практичне використання розробленої методики для проведення верифікації різних реалізацій протоколу ТСР на етапі з'єднання. Встановлено, що стадія з'єднання протоколу ТСР у Unix подібних системах реалізована у повній відповідності з вимогами стандарту.

Рис. 3. Графік порівняння отриманих даних сумарної кількості нормогодин

Аналіз та формалізація специфікації протоколу Megaco/H.248 за допомогою лінійної темпоральної логіки показала, що в специфікації існує ряд протиріч, зокрема різна інтерпретація терміну TerminationID. Даному факту повинна бути приділена увага розробників з метою усунення помилок на етапі з'єднання обладнання, реалізованого за допомогою протоколу Megaco/H.248.

Верифікація двох різних реалізацій протоколу RTP RFC 3550 и RFC 1889 допомогла встановити, що при сумісній роботі обладнання, що реалізує вказані RFC можливе виникнення помилок, пов'язаних з відмінністю в алгоритмах виявлення циклів та конфліктів, за рахунок використання однакових SSRC або CSRC ідентифікаторів.

Висновки

У дисертаційній роботі розв'язано актуальну наукову задачу, яка полягає є підвищенні ефективності методів аналізу та верифікації телекомунікаційних протоколів за рахунок використання Е-мереж та формальних граматик, що дозволять скоротити час розробки та впровадження як нових телекомунікаційних протоколів, так і виявити помилки у роботі існуючих.

В процесі розв'язання поставленої наукової задачі зроблено такі висновки:

1. Аналіз стану та перспектив розвитку сучасних телекомунікаційних протоколів показав, що ключове значення при впровадженні нових сервісів, які передбачають модернізацію або розробку нових протоколів, мають час розробки протоколів та рівень їх якості. Однак існуючі методи розробки та аналізу телекомунікаційних протоколів не задовольняють сучасним вимогам. З метою вирішення виявленої проблеми проведено аналіз основних етапів розробки телекомунікаційних протоколів, та визначені характерні для кожного етапу помилки та їх чинники. На підставі проведеного дослідження встановлено, що збільшення часу розробки протоколів обумовлюється недоліками при формуванні специфікації протоколу, відсутністю математичних засобів опису та перевірки реалізації протоколу.

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

3. З метою усунення помилок, що виникають безпосередньо на етапі реалізації протоколу запропоновано використовувати модельний підхід щодо аналізу функціонування протоколу. Використання моделі протоколу дозволяє встановити коректність поведінки протоколу та наявність усіх необхідних властивостей, що має містити протокол. Такий підхід дозволяє зменшити ймовірність виникнення помилок підчас експлуатації протоколу. Проведений аналіз засобів математичного моделювання телекомунікаційних протоколів дозволив встановити, що найбільш доцільним засобом вирішення поставлених задач є апарат Е-мереж. Його застосування обумовлене низкою переваг: можливість моделювання паралельних процесів як синхронної так й асинхронної природи, можливість вводу розширеного значення міток, що дозволяє враховувати особливості функціонування протоколу, універсальність та високий рівень деталізації. З метою вирішення задачі побудови адекватної моделі протоколу розроблено метод відображення формул темпоральної логіки в Е-мережу. Розроблений метод дозволяє на основі формальної специфікації протоколу побудувати відповідний граф Е-мережі.

4. У рамках перевірки коректності функціонування протоколу й оцінки розподілу ресурсів запропоновано проведення структурного аналізу моделей протоколів та розглянута можливість використання основних алгоритмічних властивостей Е-мереж таких як обмеженість, жвавість, досяжність, безпечність, консервативність, покриваємість. В результаті прийнято рішення щодо доцільності аналізу моделі на наступні алгоритмічні властивості: обмеженість, жвавість, досяжність, безпечність.

5. Виявлено, що існуючі методи аналізу алгоритмічних властивостей Е-мереж, такі як дерево досяжності та матричні рівняння, не дозволяють вирішити задачу формального опису поведінки протоколів та аналізу ефективності розподілу ресурсів. З метою усунення вказаного недоліку в якості методу аналізу запропоновано використовувати формальні граматики, які дозволяють представити в алгебраїчному вигляді поведінку протоколу, що, в свою чергу, дозволить провести оцінку коректності поведінки і вирішити завдання оцінки ефективності розподілу ресурсів, а також провести аналіз алгоритмічних властивостей протоколу. Розроблено метод синтезу формальної граматики, що дозволяє однозначно відобразити кожний активний перехід моделі протоколу на основі Е-мережі відповідним до нього символом, що дозволяє однозначно інтерпретувати зміну станів моделі протоколу за допомогою символів алфавіту. Застосування формальних граматик як одного з методів аналізу телекомунікаційних протоколів та розроблених на їх основі правил на відміну від інших методів дозволило встановити факт виникнення зациклень та виникнення надлишковості у процесі функціонування протоколу.

6. Процес верифікації полягає у встановленні відповідності розробленого протоколу його специфікації. Дослідження основних методів верифікації дозволили встановити, що їх використання для телекомунікаційних протоколів досить ускладнене у силу наступних недоліків: можливість використання лише на впроваджених моделях, необмежений час проведення верифікації, виявлення тільки шаблонного набору помилок, ефект "комбінаторного вибуху" та ін. З метою усунення наведених недоліків розроблено метод верифікації, що ґрунтується на методі "перевірки на моделях". Запропонований метод дозволяє уникнути ефекту "комбінаторного вибуху" простору станів моделі за рахунок того, що порівняння двох формальних граматик базується на послідовній перевірці еквівалентності мовних ланцюгів, що побудовані відповідно для реалізації та специфікації протоколу. Також запропоновано метод побудови контрприкладу, що базується на алгоритму подвійного обходу та пошуку. Застосування даного алгоритму дозволяє в алгебраїчному вигляді описати причини невідповідностей поведінки реалізації протоколу його специфікації та виявити шляхи їх усунення.

7. На основі розроблених часткових методів аналізу та верифікації телекомунікаційних протоколів сформульована й описана загальна методика аналізу та верифікації телекомунікаційних протоколів, яка базується на принципах каскадного життєвого циклу. У рамках загальної методики сформовані цілі кожного окремого етапу, засоби, що використовуються та позначені результати, що передбачаються. Ефективність розробленої методики аналізу та верифікації телекомунікаційних протоколів оцінювалася шляхом порівняння загальної трудомісткості виконання проекту двома групами розробників (виміряна в норма годинах: людина * час). Отримані дані дозволили встановити, що використання розробленої методики аналізу та верифікації дозволяє скоротити тривалість процесу розробки телекомунікаційних протоколів на 20%.

Список опублікованих праць за темою дисертації

1. Сабурова С.А. Методика моделирования и расчетов оценки параметров качества IP-технологий / Сабурова С.А., Коровченко Е.Б. // Радиотехника. - 2008. - №155. - С. 111-115

2. Коровченко Е.Б. Применение формальных грамматик как метода анализа моделей ТКС, построенных на основе Е-сетей / Коровченко Е.Б., Салман Амер Мусхин // Радиотехника. - 2009. - №159. - С.104-109.

3. Дуравкин Е.В. Использование формальных грамматик для верификации алгоритмов управления / Дуравкин Е.В., Коровченко Е.Б. // Радиотехника. -2010. - №163. - С. 61-65.

4. Дуравкин Е.В. Формализация поведения протоколов информационного обмена, представленных моделями на основе аппарата Е-сетей [электронный ресурс] / Е.В. Дуравкин, Е.Б. Коровченко // Проблеми телекомунікацій. - 2011. - №1(3). - С. 28-38 - Режим доступу до журн.: http://pt.journal.kh.ua/2011/1/1/111_duravkin_verification.pdf.

5. Дуравкин Е.В. Верификация протоколов информационного обмена на основе формальних граматик/ Дуравкин Е.В., Дуравкина Т.В. Коровченко Е.Б. // Системи управління, навігації та зв'язку: зб. наук. пр ЦНДІНУ. - 2011. - Вип.2(18). - С. 244-247.

6. Сабурова С.А. Критерии качества обслуживания в IP сетях / Коровченко Е.Б., Сабурова С.А. // Материалы XII Международного молодежного форума "Радиоэлектроника и молодежь в XXI веке", 1-3 апреля 2008 - Часть 1. - Харьков: ХНУРЭ - С. 134

7. Коровченко Е.Б. Интеграция мобильных коммуникаций в бизнес-процессы предприятий и бизнес услуг / Коровченко Е.Б., Сабурова С.А. // Сборник научных трудов 3-го Международного радиоэлектронного форума "Прикладная радиоэлектроника. Состояние и перспективы развития". - Том 2 - 2008 г - С. 197-198.

8. Коровченко Е.Б. Применение формальных языков сетей Петри для моделирования распределенных систем/ Коровченко Е.Б. // Материалы XIII Международного молодежного форума "Радиоэлектроника и молодежь в XXI веке". - 30 марта - 1 апреля - Часть 1. - Харьков: ХНУРЭ, 2009 - С. 176

9. Коровченко Е.Б. построение единой городской информационной системы на основе сервис ориентированной архитектуры СОА / Коровченко Е.Б. // Материалы XIV Международного молодежного форума "Радиоэлектроника и молодежь в XXI веке". -18-20 марта - Часть 1. - Харьков: ХНУРЭ, 2010 - С. 153

10. Коровченко Е.Б. Применение теории формальных грамматик как метода качественного анализа Е-сетей / Коровченко Е.Б., Гладий Л.В // Материалы международного молодежного форума "Компьютерное моделирование в наукоемких технологиях" - Часть 2 - Харьков: ХНУ, 2010 - С. 124-127.

11. Коровченко Е.Б. Метод верификации протоколов информационного обмена на базе формальных грамматик // Материалы 15-го Международного молодежного форума "Радиоэлектроника и молодежь в XXI веке". - Том 4. - Харьков: ХНУРЭ, 2011 - С. 44-45.

12. Коровченко Е.Б. Применение теории формальных грамматик как метода верификации протоколов информационного обмена / Коровченко Е.Б. // IX Международная научно-техническая конференция "Перспективные технологии в средствах передачи информации - ПТСПИ?2011". - 29 мая - 1 июня - Владимир: ВлГУ, 2011 - Том. 1 - С. 163-165.

Размещено на Allbest.ru