Логічний аналіз протоколів мереж ЕОМ на основі моделі взаємодіючих автоматів

Размещено на http://www.allbest.ru

ДОНЕЦЬКИЙ ДЕРЖАВНИЙ ТЕХНІЧНИЙ УНІВЕРСИТЕТ

05.13.13 - Обчислювальні машини, системи та мережі

Автореферат

дисертації на здобуття наукового ступеня

кандидата технічних наук

Логічний аналіз протоколів мереж ЕОМ

на основі моделі взаємодіючих автоматів

Потапов Ігор Геннадійович

Донецьк - 2001р

Дисертацією є рукопис.

Робота виконана в Інституті прикладної математики і механіки НАН України.

Науковий керівник: доктор технічних наук, доцент Скобцов Юрій Олександрович,

Інститут прикладної математики і механіки НАН України, відділ теорії керуючих систем, провідний науковий співробітник.

Офіційні опоненти: доктор технічних наук, профессор Слєпцов Анатолій Ілліч, Донецький інститут економіки і господарчого права, завідувач кафедри інформатики і інформаційних технологій;

кандидат технічних наук, доцент Болдак Андрій Олександрович, Національний технічний університет України “КПІ”, доцент кафедри обчислювальної техніки.

Провідна установа: Інститут кібернетики ім. В.М. Глушкова, відділ 100, НАН України, м. Київ.

Захист відбудеться " 26 " квітня 2001 р. о 14 годині на засіданні спеціалізованої вченої ради К 11.052.03 Донецького державного технічного університету за адресою : 3000, м. Донецьк, вул. Артема, 58, уч. корпус 1, ауд. 201.

З дисертацією можна ознайомитись у бібліотеці Донецького державного технічного університету за адресою :

83000, м. Донецьк, вул. Артема, 58, уч. корпус 2.

Автореферат розісланий " 23 " березня 2001 р.

Вчений секретар

спеціалізованої вченої ради Мокрий Г.В.

ЗАГАЛЬНА ХАРАКТЕРИСТИКА РОБОТИ

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

Однією з найважливіших задач, що виникають при проектуванні протоколів інформаційно-обчислювальних мереж, є аналіз їх логічної коректності. Задача аналізу логічної коректності вивчалась багатьма авторами та досліджувалась різними математичними апаратами. Ефективний аналіз різноманітних складних систем проводився за допомогою мереж Петрі В.Є.Котовим, А.І.Слєпцовим, C.Girault, J.Piterson. Методи аналізу логічної коректності протоколів, які розроблено в працях M.Gouda, R.Miller, W.Peng, S.Purshothaman, H.Schoot, основані на моделі взаємодіючих автоматів, введеною G.V.Bochmann. В подальшому ця модель стала базовою для мов специфікацій, таких як SDL і ESTELLE.

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

Зв'язок роботи з науковими програмами, планами, темами. Дисертацію виконано в 1996-2000 рр. у відповідності з планами науково-дослідницьких робіт лабораторії прикладних проблем дискретної математики ІПММ НАН України (м. Донецьк): НДР №0194U022564 "Дослідження зворотних задач теорії автоматів застосовно до ідентифікації та розпізнавання дискретних систем" (1994-1998), НДР №0199U001612 "Дослідження актуальних проблем моделювання, керування та ідентифікації дискретних систем" (1999).

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

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

Задачі роботи. У відповідності до поставленої мети в роботі вирішуються наступні основні задачі:

1)розробка методів та алгоритмів вирішення відкритих задач логічної коректності протоколів інформаційно-обчислювальних мереж;

2)розробка методів аналізу протоколів з обмеженою та необмеженою взаємодією через канали зв'язку;

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

Об'єкт дослідження - протокол інформаційно-обчислювальних мереж.

Предмет дослідження - перевірка логічної коректності комунікаційних протоколів.

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

Наукова новизна одержаних результатів визначається наступними положеннями:

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

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

3.Одержано умови обмеженої та необмеженої взаємодії протоколів, на основі введеного поняття визначності взаємодії. Ці умови визначають класи протоколів з заздалегідь відомими властивостями.

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

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

Особистий внесок здобувача. Основні положення і результати дисертаційної роботи отримані автором самостійно.

На захист виносяться:

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

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

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

4)Метод ідентифікації ситуацій експоненціального переповнення мережі необробленими кадрами даних.

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

Апробація роботи. Основні положення та результати роботи доповідалися й обговорювалися на:

III Міжнародній конференції "Дискретні моделі в теорії керуючих систем", Красновідово, 1998;

XII Міжнародній конференції "Проблеми теоретичної кібернетики", Нижній Новгород, 1999;

6-й Українській конференціі з автоматичного управління "АВТОМАТИКА-99", Харків, 1999;

16th British Colloquium for Theoretical Computer Science, Liverpool, UK , 2000;

обласних семінарах "Актуальні проблеми комп'ютерних наук", Донецьк;

наукових семінарах "Дискретні системи і формальні мови" інституту прикладної математики і механіки НАН України, Донецьк, (1997-2000рр.).

Публікації. Основні результати дисертації опубліковано в 8 роботах, з яких 5 - статей в наукових виданнях, 3 - статті в трудах міжнародних конференцій.

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

Структура та обсяг роботи. Дисертаційна робота викладена на 154 сторінках і містить вступ, основну частину з чотирьох розділів, висновки, список літератури і один додаток, розташований на чотирьох сторінках. Дисертація також містить 39 рисунків, 13 таблиць. Список використаної літератури складається з 88 джерел і розташований на 8 сторінках.

ОСНОВНИЙ ЗМІСТ

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

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

В підрозділі 1.1 розглядаються питання організації взаємодії між пристроями в інформаційно-обчислювальних мережах. Основою структури комп'ютерних мереж є багаторівнева мережева архітектура ISO/OSI. Вона містить в собі дві групи рівнів: мереженезалежні, які орієнтовані на застосування та мало залежать від технічних особливостей побудови мережі, і мережезалежні, які зв'язані з технічною реалізацією мережі та з комунікаційним обладнанням, яке використовується.

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

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

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

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

Підрозділ 1.2 присвячено моделі взаємодіючих автоматів, яку найбільш широко використовують для тестування та сертифікації протоколів обчислювальних мереж. Вперше модель взаємодіючих автоматів була введена G.V.Bochmann і лежить в основі двох стандартних мов специфікацій, таких як SDL і ESTELLE.

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

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

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

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

Під автоматом A розуміється четвірка (SA,IAИOA,dA,s0), де SA- скінченна множина станів; IA (OA) - скінченний алфавіт символів, які приймаємо (посилаємо), при цьому IAЗOA=Ж ; dAНSAґ{IAИ OA}ґSA - множина переходів автомата А; s0 - початковий стан. Таким чином, автомат A представляє собою навантажений орграф з початковою вершиною s0 і двома типами дуг: приймаючими та посилаючими. Посилаючі (приймаючі) дуги помічені "-g", де gОOA ("+g", де gОIA) - символами на дугах з алфавіту IAИOA. Стан автомата називається приймаючим, якщо з нього визначені тільки приймаючі дуги.

Під каналом зв'язку Сij, через який пересилаються повідомлення із алфавіту Xij, і зв'язуючим автомат Ai з автоматом Aj, розуміємо чергу FIFO, яка організована таким чином, що в кожний момент часу в неї зберігається слово скінченної довжини, можливо пусте, в алфавіті Xij. Послідовність повідомлень, надісланих з Ai в Aj, яка міститься в каналі Сij, позначимо як cij.

В якості прикладу на рис.1 наведено діаграми станів взаємодіючих автоматів, які описують поведінку передавача та приймача у відповідності з протоколом Alternating-Bit Protocol з нумерацією по модулю 2.

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

Таким чином, для аналізу протоколів комунікаційних пристроїв мережезалежних рівнів, доцільно розглядати модель без обмежень на топологію з'єднань. В подальшому під протоколом Gm(A1,...,Ak) будемо розуміти мережу взаємодіючих автоматів, визначеною наступним чином: G - скінченний циклічний орграф з k вершинами, в яких розташовуються скінченні автомати A1,...,Ak, і з m дугами, які являють собою односпрямовані канали у вигляді черг повідомлень типу FIFO. Протокол Gk(A1,...,Ak), назвемо циклічним, якщо орграф G являє собою простий цикл.

Конфігурація протоколу Gm(A1,...,Ak) може бути представлена у вигляді пари , де - вектор станів черг необроблених повідомлень, а - вектор станів автоматів. Ініціальною конфігурацією K0 є конфігурація протоколу, коли усі автомати знаходяться в початкових станах, а усі черги повідомлень пусті.

Перехід із конфігурації K в конфігурацію Kў відбувається після виконання одиночного переходу в одному з автоматів і позначається як K®Kў. В результаті цього змінюється поточний стан даного автомата і стан одного із каналів зв'язку Cij або Cji, в залежності від типу події виникнутої в автоматі Ai (прийом або передача). Приймаючий перехід (si,+xj,sўi)ОdAi автомата Ai є виконанним, якщо приймальне повідомлення xj знаходиться на першому місці в черзі повідомлень каналу Cji. Посилаючий перехід (si,-xj,sўi)ОdAi автомата Ai із поточної конфігурації завжди є виконанним і не залежить від черг повідомлень. Множина усіх конфігурацій В, досяжних із ініціальної в протоколі Gm(A1,...,Ak) визначено рефлексивним, транзитивним замиканням відношення ® і утворює граф досяжності, який характеризує динаміку функціонування протоколу.

Властивості логічної коректності в термінах взаємодіючих автоматів визначаються наступним чином. Нехай K - досяжна конфігурація протоколу Gm(A1,...,Ak). Конфігурація K є тупиком, якщо усі черги повідомлень порожні, а стани в автоматах A1,...,Ak є приймаючими. Конфігурація K є конфігурацією з неспецифікованим прийомом, якщо sf є приймаючим станом, cif має вигляд xЧw і в автоматі Af не визначено перехід (sf,+xi,sfў) для усіх i: 1ЈiЈk.

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

Перехід (si,t,siў) в автоматі Ai є живим, якщо в графі досяжності мережі існують вершини K,KўОВ такі, що K®Kў та із вершини K в вершину Kў веде дуга, яку позначено символом переходу ((s1,…,si,…,sk), t , (s1,…,siў,…,sk)).

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

Таким чином, протокол логічно коректний тоді і тільки тоді, коли множина досяжних станів В є вільною від вищеперерахованих логічних помилок.

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

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

Підрозділ 2.1 присвячено характеристиці мови, яка породжується послідовністю переходів протокольних об'єктів, відносно традиційних класів мов.

Оскільки події протоколу представлено переходами автоматів, то його функціонування можно описати в термінах протокольних подій. Послідовність переходів може бути визначена у вигляді деякої формальної мови. Множину шляхів LG у вигляді вхід-вихідних слів, які породжуються подіями протоколу Gm(A1,...,Ak), будемо називати мовою траекторій. Множина усіх слів, складених із подій в алфавіті T=IA1И…ИIAkИOA1И…ИOAk, визначає множину T*, тоді LG являє собою підмножину виконанних переходів множини T*.

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

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

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

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

Орієнтований граф A<F> назвемо зрізаним, якщо A<F> одержано із навантаженого орієнтованого графа автомата A шляхом вилучення усіх дуг, позначених +g або -g, де g - елемент, який належить сингулярному алфавіту. Цикл графа G, утворений тільки з несингулярних каналів, назвемо несингулярним циклом. Несингулярний цикл графа G з маршрутом A1,…,Ai назвемо складним, якщо зрізані графи автоматів по даному маршруту є циклічними.

Центральним результатом розділу 2 є твердження 2.2.5, яке визначає межу алгоритмічної розв'язності відносно обмеження на потужність алфавітів каналів зв'язку, на основі якого в подальшому розроблено метод перевірки логічної коректності.

Твердження 2.2.5. Проблема тупика, проблема неспецифікованого прийому, проблема надмірності та проблема обмеженості протоколу Gm(A1,...,Ak) алгоритмічно розв'язні в тому та тільки в тому випадку, коли граф G не містить складного несингулярного циклу.

Необхідність твердження 2.2.5 випливає з нерозв'язності зазначених проблем для довільної протокольної пари. Доведення достатності проведено конструктивно, за допомогою побудови алгоритму перевірки логічної коректності протоколу. Алгоритм містить в собі дві основних частини. В першій частині відбувається побудова допоміжного автомата Aў по протоколу Gm(A1,...,Ak), моделюючого роботу мережі таким чином, що після кожної передачі в несингулярний канал зв'язку відбувається прийом із нього. Показано, що побудований автомат Aў зберігає властивості коректності протоколу Gm(A1,...,Ak). В другій частині проводиться аналіз логічної коректності допоміжного автомата на основі еквівалентності моделі мережі Петрі.

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

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

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

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

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

Протокол Gm(A1,...,Ak) назвемо визначним відносно прийому (передачі), якщо при взаємодії мережі автоматів A1,...,Ak існує таке ціле додатне число r, що будь-яка послідовність переходів a1,a2,…,ar однозначно визначає множину виконанних переходів по приймаючим (посилаючим) дугам із, може бути, неспостережуваної конфігурації мережі, в якій вона закінчується. Протокол Gm(A1,...,Ak) назвемо визначним, якщо його взаємодія одночасно визначена відносно прийому та передачі. Поняття визначності базується на аналізі вхід-вихідних повідомлень при протокольній взаємодії .

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

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

Властивість обмеженості черг повідомлень зв'язана не тільки з передбаченістю поведінки протоколу, але також і з проблемами управління потоками даних в інформаційно-обчислювальних мережах. Однією з таких проблем є незастосовність простих процедур управління потоками даних, заснованих на командах "припинити передачу" та "відновити передачу", які використовуються в стандарті IEEE 802.3x. Такий вид управління широко використовується в повнодуплексних версіях протоколу Ethernet, проте виявляється непридатним в мережах Gigabit Ethernet, так як повне зупинення прийому кадрів від суміжного вузла при швидкості 1 488090 кадр./c. викликає переповнення внутрішнього буфера у суміжних вузлів. При розробці більш тонких механізмів регулювання потоками даних необхідно аналізувати поведінку таких протоколів та ідентифікувати ситуації, при яких виникає переповнення мережі необробленими кадрами даних.

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

В силу того, що проблема обмеженості алгоритмічно нерозв'язна, основним питанням є знаходження достатніх умов необмеженості для загального класу протоколів. Задача знаходження достатніх умов необмеженої взаємодії вже досліджувалась при аналізі поведінки комунікаційних протоколів в роботах C.Jard, T.Jeron, A.Finkel. Проте умови, які одержано в них, відповідали досить простим видам необмеженості з регулярним зростанням черг повідомлень в каналах зв'язку. При цьому послідовності траекторій породжували лінійні або словниково-лінійні мови.

Аналіз представленого протоколу утруднений тим, що послідовність переходів утворює контекстно-чутливу мову LR, де , w={-а-c+c-b-d+d}, u={+a-a-c+c-a+b-c+c}, v={+a-a-c+c-b-d+d+a-a-c+c-b-d+d}, а також комбінаторним зростанням числа досяжних конфігурацій. В зв'язку з цим, визначено дві основні задачі: розширення достатніх умов і зменшення числа аналізованих конфігурацій.

Для скорочення числа аналізованих конфігурацій розроблено метод побудови часткового дерева досяжності PT спеціального виду. Аналіз часткового дерева досяжності проводиться на моделі протоколу Gm(A), який складається з одного автомата A і m каналів зв'язку C1,…,Сm. Дане припущення дозволяє більш явно розглянути причини необмеженості та точно сформулювати умови необмеженого зростання черг повідомлень в каналах зв'язку C1,…,Сm.

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

1)із ініціальної конфігурації виконується послідовність посилаючих переходів в канал Ci;

2)при досяжності конфігурації KўОPT із K=((w1,..,wi,…,wm),)ОPT відбувається прийом слова wi із каналу Ci і кожна послідовність переходів закінчується переходом прийому повідомлення із Ci.

На основі побудованого дерева PT визначено поняття виведеності конфігурацій. Будемо вважати, якщо за конфігурацією K1=(u1,s1) прямує конфігурація K2=(u2,s2), то з вектору слів u1 у стані s1 виводиться вектор слів u2 при переході у стан s2. Вивід конфігурації (u2,s2) із (u1,s1) в дереві PT позначимо через (u1,s1)Ю(u2,s2).

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

При аналізі часткового дерева досяжності виділено ряд властивостей, на основі яких одержано нову достатню умову необмеженого зростання черг повідомлень.

Твердження 3.3.5. Якщо в частковому дереві досяжності протоколу Gq(A) одержано конфігурацію (ut,s), де utО((u1)*Ч(u2)*Ч(u3)* … Ч(ut-1)* )* і визначено послідовність виводів: (u1,s) Ю(u2,s), (u2,s) Ю(u3,s) ,…, (ut-1,s) Ю(ut,s), тоді існує нескінченна послідовність виводів із конфігурації (ut,st), які визначають траекторію протоколу з необмеженою взаємодією.

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

В підрозділі 3.4 проведено аналіз складності досліджуваних класів протоколів на основі теорії формальних мов, а також установлено ієрархію класів протоколів.

Розділ 4 присвячено розробці прикладних методів аналізу комунікаційних протоколів з довільною топологією. В підрозділі 4.1 показано застосовність моделі взаємодіючих автоматів до конструкцій мови описів і специфікацій SDL. Перевірку коректності протокольних специфікацій може бути здійснено шляхом перетворення їх в більш прості структури. Модель взаємодіючих автоматів є найбільш придатною на етапі аналізу, в зв'язку з розкладанням процесів будь-якої складності на елементарні операції передачі та прийому повідомлень через канали зв'язку.

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

Нехай T - множину каналів мережі Gm(A1,...,Ak), визначено таким чином, що кожний цикл орграфа G містить хоч би один канал, який належить множині T. Будемо вважати T ў мінімальним, якщо вилучення будь-якого елемента із множини T приводить до існування циклу в графі G, який містить дугу, вилучену із T. На основі еквівалентних перетворень протокольних специфікацій розроблено метод побудови допоміжного автомата A', на основі якого проводиться аналіз комунікаційного протоколу. Дане перетворення полягає у перетворенні протоколу, в топології якого існує q простих циклів, в допоміжний об'єкт Gq(A) через об'єднання подій прийому та передачі при взаємодії з каналами, які не належать множині Tў.

Розглянемо функцію h, яка визначає потенціальну кількість аналізованих конфігурацій у графі досяжності для протоколу Gm(A1,...,Ak), а також для протоколу Gq(Aў), одержаного методом стиснення початкового протоколу по спряженим переходам:

, ,

де k - число протокольних автоматів в мережі, Ni - число станів в i-ому автоматі, m - число черг, r - максимальний розмір черги, F - потужність передаваного алфавіту повідомлень, q - число простих циклів в топології мережі.

Помітимо, що після перетворення експонента функції h обмежена числом простих циклів в топології протоколу Gm(A1,...,Ak). Експериментальні дані застосування методу стиснення логічної структури показали, що в напівдуплексних і повнодуплексних протоколах метод стиснення поліпшує існуючі методи на 25-30%, а при застосуванні до протоколів з симплексною передачею даних скорочує число аналізованих конфігурацій більш ніж на 80%.

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

Експерименти з паралельними процесами було проведено в мережі робочих станцій Hewlett Packard 720 Unix через 10Mb Ethernet використовуючі PVM (parallel virtual machine) версії 3.4.5 і показано, що в результаті застосування паралельного методу аналізу протоколів з довільною топологією мережі ефективність методу зростає при збільшенні числа протокольних об'єктів у циклах топології мережі.

Підрозділ 4.3 є продовженням підрозділу 3.4. На основі перетворення, запропонованого в 4.2, і достатньої умови необмеженості графа досяжності із 3.4, будується алгоритм ідентифікації ситуацій експоненціального переповнення мережі необробленими кадрами даних. Алгоритм пошуку необмеженості з експоненціальним зростанням черг повідомлень одержано вперше. При цьому досягнено скорочення числа аналізованих конфігурацій більш ніж на 70% відносно загального числа конфігурацій.

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

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

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

В додатку А наведено Акт впровадження результатів дисертаційної роботи в ВАТ Донецький головний обчислювальний центр і Довідка про використання результатів диссертації в учбовому процесі кафедри “Комп'ютерні технології” Донецького державного університету.

ВИСНОВКИ

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

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

2.Розроблено конструктивний метод аналізу протокольних специфікацій на основі стиснення логічної структури еквівалентними перетвореннями, застосування якого до напівдуплексних і повнодуплексних протоколів скорочує число аналізованих ситуацій, відносно існуючих методів, на 25-30%, а при застосуванні до протоколів з симплексною передачею даних - більш ніж на 80%. Показано застосовність методу при аналізі дерева досяжності протоколу незалежними паралельними процесами.

3.Одержано умови обмеженої та необмеженої взаємодії протоколів, на основі введеного поняття визначності взаємодії. Ці умови визначають класи протоколів з заздалегідь відомими властивостями.

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

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

СПИСОК ОПУБЛІКОВАНИХ ПРАЦЬ ЗА ТЕМОЮ ДИСЕРТАЦІЇ

1.Потапов И.Г. Об алгоритмической разрешимости проблем корректности взаимодействия сети автоматов // Труды института прикладной математики и механики НАН Украины. - т2. - Донецк, ИПММ. -1998. -С.128-136.

2.Курганский А.Н., Потапов И.Г. О границе алгоритмической разрешимости проблем корректности взаимодействия автоматов через каналы связи // Кибернетика и системный анализ. - 1999.-№3.- С. 49-58.

3.Грунский И.С., Потапов И.Г. Автоматные методы анализа протоколов // Вестник Харьковского государственного политехнического университета, серия "Системный анализ, управление и информационные технологии".-т73.-Харьков.-1999.-С.43-48.

4.Скобцов Ю.А., Потапов И.Г. Анализ взаимодействующих систем со сложной управляющей логикой // Наукові праці Донецького державного технічного університету. Серія Обчислювальна техніка та автоматизація, Випуск 20: - Донецьк: ДонДТУ, - 2000. - С.208-216.

5.Потапов И.Г. Характеристика определимых взаимодействующих систем // Труды института прикладной математики и механики НАН Украины. - т4. - Донецк, ИПММ. -1999. -С. 134-141.

6.Потапов И.Г. Об алгоритмической разрешимости проблем корректности взаимодействия сети автоматов // Труды III Международной конференции "Дискретные модели в теории управляющих систем". - М. МГУ. - 1998. - C. 93-96.

7.Потапов И.Г. О классе определимых циклических протоколов // Тезисы докладов XII Международной конференции "Проблемы теоретической кибернетики".- М. МГУ.- 1999. - С.190.

8.Potapov I. Logical analysis of communicating finite-state machines (CFSM) model under additional local conditions // Bulletin of European Association in Theoretical Computer Science. v.72- 2000. - P. 211.

Особистий внесок здобувача у публікаціях: в [2,3] автором одержано критерій розв'язності проблем логічної коректності відносно обмеження на алфавіти каналів зв'язку; в [3] визначено класи протоколів, для яких проблеми коректності алгоритмічно розв'язні; в [4] розроблено метод перевірки експоненціального переповнення черг повідомлень.

АНОТАЦІЇ

Потапов І. Г. Логічний аналіз протоколів мереж ЕОМ на основі моделі взаємодіючих автоматів. - Рукопис.

Дисертація на здобуття наукового ступеня кандидата технічних наук за спеціальністю 05.13.13 - обчислювальні машини, системи та мережі. - Донецький державний технічний університет, Донецьк, 2001.

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

Ключові слова: протоколи, мережі ЕОМ, автомати, коректність протоколів, формальні методи, еквівалентні перетворення, переповнення мережі, аналіз, черги типу FIFO.

Потапов И.Г. Логический анализ протоколов сетей ЭВМ на основе модели взаимодействующих автоматов. - Рукопись.

Диссертация на соискание ученой степени кандидата технических наук по специальности 05.13.13 - вычислительные машины, системы и сети. - Донецкий государственный технический университет, Донецк, 2001.

На основе теоретических и экспериментальных исследований в диссертационной работе предложены новые формальные методы решения открытых проблем логической корректности протоколов информационно-вычислительных сетей. Показано, что существование в каждом цикле топологии сети хотя бы одного канала связи с сингулярным алфавитом сообщений является критерием алгоритмической разрешимости при проверке логической корректности протоколов со сложной топологией сети. С помощью этого критерия разработан метод анализа логической корректности, расширяющий класс проверяемых протоколов. При решении проблемы комбинаторного роста числа анализируемых конфигураций разработан метод сжатия логической структуры эквивалентными преобразованиями, применение которого сокращает число анализируемых ситуаций относительно существующих методов более чем на 25-30%. При анализе протоколов с ограниченным и неограниченным взаимодействием, через очереди типа FIFO, получены условия определяющие классы протоколов с заранее известными свойствами. Найдено достаточное условие экспоненциального переполнения сети необработанными кадрами данных, на основе которого разработан метод идентификации проблем в управлении потоками данных в больших сетях. Предложенные методы программно реализованы и позволяют расширить класс проверяемых протоколов, а также существенно сократить затраты времени и памяти в процессе их анализа.

Ключевые слова : протоколы, сети ЭВМ, автоматы, корректность протоколов, формальные методы, эквивалентные преобразования, переполнение в сети, анализ, очереди типа FIFO.

Potapov I.G. Logical analysis of network protocols on the basis of communicating finite state machines model. - Manuscript.

Thesis for a candidate's degree (technical sciences) by specialty 05.13.13 - computers, systems and networks. - Donetsk State Technical University, Donetsk, 2001.

New methods that decide open problems of logical correctness of communication protocols in informational-computing networks were proposed on the basis of theoretical and experimental investigations in dissertation.

Distributed systems, high-level software designs, software for parallel processors, and communications protocols can be specified as collections of communicating processes. It is very hard to analyse software for such systems, whether it is expressed abstractly (“specifications”) or concretely (“code”) since there are two interfering limitations, namely, undecidability and state explosion.

We focus on verifying progress properties of communication protocols, such as absence of deadlocks, unspecified receptions, liveness and unbounded channel growth on the basis of a Communicating Finite State Machines (CFSM) model. A network of CFSM consists of a set of finite state machines, which communicate asynchronously with each other over (potentially) unbounded FIFO channels by sending and receiving typed messages. As a concurrency model, CFSM has been widely used to specify and validate communications protocols. Moreover, the CFSM model with unbounded FIFO channels is ideal for modelling and analysing the behaviour of mobile communication systems.

The work presented in dissertation proposes a new reachability technique that is applicable to protocols with complicated topology graphs. The new reachability analysis is based on transformation of protocol structure to examine progress properties using some limited sequence of equivalent transitions.

We show that the analysis of protocol can be reduced to the analysis of a single CFSM with a q-queue, where q is a number of cycles in the network topology. This leads to decidability results of correctness problems for a class CFSM network with at least one singular alphabet channel in each cycle of the network topology. It is shown that this limitation on alphabet of messages is a criterion of algorithmic decidability. As a result, the method of the logical correctness analysis expanding class of checked up protocols is developed on the basis of algorithmic decidability criterion.

The new relief strategy that refrains from any syntactic restriction is proposed to decide a problem of combinatory growth of number of the parsed configurations. This strategy leads to constructing equivalent transformation model and reduces number of parsed situations concerning existing methods more than to 25-30 %.

The method of structure compression of protocol allows not only to reduce the number of parsing configurations but also to choose some classes of protocols with algorithmic decidability of problems of correctness, but also enables us to parse a reachability tree by independent parallel processes.

The correctness problems of protocols with potentially unbounded and bounded FIFO channels were investigated. Conditions defining classes of protocols with beforehand known properties are obtained in the process of protocol analysis with bounded and unbounded communication.

In order to extend the testing approach of unbounded problem we propose the new type of partial reachability tree for the protocols that free from sending cycles and the sufficient condition of unbounded channel growth that includes the regular and exponential growth of messages queue in FIFO channels. The new sufficient condition of "exponential growth" is more powerful than the previous condition for word-linear languages, since could recognise unboundedness for context-free trajectories as well as some context-sensitive trajectories. On the basis of new sufficient condition the unboundedness test can easily be constructed and mixed with on-line model-checking algorithms. The unboundedness test can be very useful for protocol designers in verification phase of protocol specifications.

In order to conclude our investigation from the practical point of view, we show that a few modifications of the relation make the methods available for SDL specifications. The offered methods are realised as software and allow to expand the class of checked up protocols, and also it is essential to reduce expenses of time and memory during their analysis.

As a result, offered methods appear as an effective and efficient state exploration technique as well as developed formal methods, able to handle the verification of protocols that are substantially "larger" than those manageable before.

Key words: protocols, communications networks, automata, correctness of protocols, formal methods, equivalent transformations, overflow in network, analysis, FIFO queues.

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

...