МІНІСТЕРСТВО ТРАНСПОРТУ ТА ЗВ’ЯЗКУ УКРАЇНИ

ОДЕСЬКА НАЦІОНАЛЬНА АКАДЕМІЯ ЗВ’ЯЗКУ ім. О.С. ПОПОВА

ЗАЙЦЕВ ДМИТРО АНАТОЛІЙОВИЧ

УДК 621.39, 004.7

МЕТОДИ АНАЛІЗУ І СИНТЕЗУ МОДЕЛЕЙ

ТЕЛЕКОМУНІКАЦІЙНИХ СИСТЕМ НА ОСНОВІ

ФУНКЦІОНАЛЬНИХ СІТОК ПЕТРІ

05.12.02 – телекомунікаційні системи та мережі

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

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

Одеса – 2006

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

Робота виконана в Одеській національній академії зв’язку ім. О.С. Попова,

Міністерство транспорту та зв’язку України

Науковий консультант –

д.т.н, професор Воробієнко Петро Петрович

Одеська національна академія зв’язку ім. О.С. Попова, ректор

Офіційні опоненти:

доктор технічних наук, професор Савченко Олексій Якович, член-кореспондент НАН України, Інститут телекомунікацій і глобального інформаційного простору НАН України, заступник директора з наукової роботи.

доктор технічних наук, професор Поляков Петро Федорович, Харківська державна академія залізничного транспорту, завідувач кафедри транспортного зв’язку.

доктор технічних наук, професор Ящук Леонід Омелянович, Одеська національна академія зв’язку ім. О.С. Попова, професор кафедри мереж та систем поштового зв’язку.

Провідна установа –

Харківський національний університет радіоелектроніки,

Міністерство освіти України, м. Харків

Захист відбудеться 6 жовтня 2006 р. о 10 годині на засіданні спеціалізованої вченої ради Д 41.816.02, Одеська національна академія зв’язку ім. О.С. Попова, вул. Кузнечна 1, 65029, м. Одеса.

З дисертацією можна ознайомитися у бібліотеці

Одеської національної академії зв’язку ім. О.С. Попова, вул. Кузнечна 1, 65029, м. Одеса.

Автореферат розісланий 31.08.2006 р.

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

спеціалізованої вченої ради _________ Ложковський А.Г.

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

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

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

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

Зв'язок роботи з науковими програмами, планами, темами. Роботу виконано в рамцях Робочих програм IETF з удосконалювання протоколів Інтернет, специфікованих у RFC; Програми розвинення протоколу Bluetooth суспільства Bluetooth-SIG; Програми створення вбудованих модулів для системи Tіna автоматизованого аналізу сіток Петрі та часових сіток Петрі лабораторії LAAS, Тулуза, Франція.

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

розроблено методи синтезу сіток Петрі за стандартними специфікаціями протоколів; виконано синтез моделей Петрі та верифікацію протоколів, від коректності яких залежить надійність глобального й корпоративного інформаційного обміну, таких як TCP, BGP, IOTP;–

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

розроблено основи теорії функціональних сіток Петрі та кланів систем лінійних алгебраїчних рівнянь;–

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

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

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

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

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

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

Здобуто такі нові наукові результати:–

розроблено методи синтезу моделей телекомунікаційних протоколів, заданих специфікаціями у формі взаємодіючих послідовних процесів Хоара; виконано синтез моделі протоколу IOTP;–

розроблено методи верифікації телекомунікаційних протоколів на основі композиційного аналізу моделей Петрі; виконано верифікацію телекомунікаційних протоколів ECMA, Ethernet, BGP, TCP, IOTP за допомогою композиційного аналізу сіток Петрі;–

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

доведено, що породну сім'ю (базис) функціональних підсіток складає множина мінімальних функціональних підсіток, а також що сітка функціональних підсіток є маркірованим графом; –

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

здобуто подавання передатної функції часової сітки Петрі; розроблено методи еквівалентних перетворень та редукції сіток Петрі для слабких типів еквівалентності на підставі законів спеціально впровадженої для подавання передатної функції алгебри;–

розроблено методи синтезу функцій непереривної логіки, заданих табличне; –

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

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

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

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

Розроблено програмне забезпечення декомпозиції та композиційного аналізу сіток Петрі Deborah та Adrіana. Програмне забезпечення призначене для роботи з сітками Петрі великої розмірності, забезпечує істотні прискорення обчислень і поширюється як вбудовані модулі до відомої системи Tіna, використовуваної як інтерфейс для графічного введення й редагування сіток Петрі.

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

Розроблено методику побудови моделей на основі композиції розфарбованих сіток Петрі з контактними позиціями, що може бути застосована для довільних телекомунікаційних систем. Побудовано типові моделі компонентів та вимірювальних фрагментів для комутованих, маршрутизованих мереж, мереж з комутацією міток, мобільних сенсорних мереж, призначених для автоматизованого синтезу моделей конкретних мереж та вимірювання їхніх характеристик. Методику застосовано при проектуванні магістральних мереж ОАО “Укртелеком”, а також при проектуванні локальних мереж диспетчерських центрів залізниці, оснащених програмним забезпеченням “ГИД-Урал ВНИИЖТ”.

Особистий внесок здобувача. Основи теорії функціональних сіток Петрі, які включають методи й алгоритми декомпозиції на функціональні підсітки, композиційний аналіз та його узагальнення, теоретичне обґрунтування й оцінку складності методу Тудіка, метод вимірювальних фрагментів, композиційний аналіз протоколів ECMA, Ethernet, синтез моделей та композиційний аналіз протоколів TCP, BGP є особистим результатом здобувача. Методи синтезу функцій непереривної логіки заданих табличне, розроблено разом з А.І.Слєпцовим та В.Г.Сарбеєм. Подавання передатної функції структурно-безконфліктних сіток Петрі дістано разом з А.І.Слєпцовим. У побудові моделей комутованих мереж, мереж з комутацією міток, моделей протоколів Bluetooth та IOTP брали участь Т.Р.Шмельова, А.Л.Сакун, М.В.Березнюк, Е.Я.Чорногала.

Апробація результатів дисертації. Результати роботи представлені на семінарі з Дискретної математики, Одеса, Україна, 1995; 10-м семінарі "Алгоритми і програми для сіток Петрі", Айхштадт, Німеччина, 2003; Європейській конференції з моделювання, Неаполь, Італія, 2003; 25-ій міжнародній конференції із застосовувань й теорії сіток Петрі, Болонья, Італія, 2004; Міжнародній конференції з кібернетики та інформаційних технологій, систем та застосувань, Орландо, США, 2004; Міжнародній науково-технічній конференції "Штучний інтелект. інтелектуальні та багатопроцесорні системи". Таганрог, 2004; 11-му семінарі "Алгоритми й програми для сіток Петрі", Падерборн, Німеччина, 2004; 12-му щорічному симпозіумі IEEE / ACM з моделювання та аналізу комп'ютерних і телекомунікаційних систем, Фолендам, Нідерланди, 2004; 5-му семінарі та школі з практичного використовування розфарбованих сіток Петрі та CPN Tools, Орхус, Данія, 2004; спеціальних лекціях-семінарах в університеті Париж-Дофін і в лабораторії LAAS, Тулуза, Франція, 2005; симпозіумі з проектування, аналізу та моделювання розподілених систем, Сан Діего, США, 2005; 10-ій ювілейній конференції з Фізики та технології тонких плівок, Яремче, Україна, 2005; Міжнародній конференції "Моделювання і комп'ютерна графіка", Донецьк, Україна, 2005.

Публікації. Результати опубліковано в одній монографії, 38 статтях у наукових журналах та збірниках наукових праць, з них 29 у зазначених в переліку ВАК України, 9 – у матеріалах та тезах конференцій.

Дисертація складається з уведення, п'яти розділів, додатків; повний обсяг дисертації становить 382 сторінки; 79 ілюстрацій (32 с.), 22 таблиць (9 с.) і 5 додатків (99 с.) займають 140 сторінок; список використаних літературних джерел містить 192 найменування.

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

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

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

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

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

У 2 розділі – "Функціональні сітки Петрі" – подано основи розробленої здобувачем теорії функціональних сіток Петрі. Прикладне значення теорії функціональних сіток полягає у прискоренні аналізу моделей Петрі методами лінійної алгебри. Декомпозиція є один із традиційних підходів до аналізу сіток Петрі великої розмірності, але впроваджений здобувачем клас функціональних сіток істотно відрізняється від відомих S- і T- компонентів, I/O-сіток та інших. Здійснено класифікацію сіток Петрі з контактними позиціями, показано, що функціональні сітки є класом сіток з найбільш строгими обмеженнями на вхідні й вихідні дуги контактних позицій.

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

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

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

Функціональна сітка є функціональною підсіткою сітки N і позначається як , якщо є підсіткою N, породженою множиною : і, окрім того, Z з’єднана з частиною сітки, котра залишилася, лише за допомогою дуг, інцидентних до контактних позицій, в такий спосіб, що вхідні позиції мають лише вхідні дуги, а вихідні позиції – лише вихідні:

, ,

.

Зазначені умови можна також подати як

, , .

Далі досліджено властивості функціональних підсіток; результати подано у вигляді послідовності тверджень, лем, теорем і коротко можуть бути сформульовані в такий спосіб:–

підсітка , є функціональною підсіткою тоді й лише тоді, коли виконується умова ;–

множина мінімальних функціональних підсіток , задає розбивку множини T на неперетинні підмножини такі, що , , ;–

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

сітка функціональних підсіток заданої сітки Петрі є маркірованим графом;–

будь-яка функціональна підсітка заданої сітки Петрі N є сумою (об'єднанням) скінченого числа її мінімальних функціональних підсіток (рис. 1);–

розбивка множини T, задана множиною мінімальних функціональних підсіток, є породною сім’єю (базисом) множини функціональних підсіток сітки Петрі N.

а) сітка Петрі | б) декомпозиція | в) композиція

Рис. 1. Функціональні підсітки

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

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

,

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

а) сітка функціональних підсіток | б) орієнтований граф функціональних підсіток | в) неорієнтований граф функціональних підсіток

Рис. 2. Подавання декомпозиції

Запропоновано такий алгоритм:

Крок 0. Обрати довільний перехід сітки N і долучити його до множини обраних переходів .

Крок 1. Побудувати підсітку Z, породжену множиною R: .

Крок 2. Якщо Z є повна в N, то Z – шукана підсітка, стоп.

Крок 3. Побудувати множину поглинаних переходів:

.

Крок 4. Покласти і перейти до кроку 1.

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

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

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

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

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

Доведено, що передатна функція описується системою: |

(1)

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

Для виконання еквівалентних перетворень віднайдено алгебраїчне подавання передатної функції (1) за допомогою спеціальної алгебри, яка містить арифметичні, логічні операції та операцію часової затримки: |

, | (2)

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

Сітки та названо слабо еквівалентними стосовно класу вхідних послідовностей та моментів спостерігання й позначено , якщо для будь-якої вхідної послідовності множини їхніх вихідних послідовностей в моменти часу збігаються: , де – заданий клас вхідних послідовностей, а – послідовність (можливо нескінченна) моментів часу спостерігання.

Еквівалентні перетворення сіток (рис. 3) виконуються шляхом перетворення формул (2), які описують їхню передатну функцію.

Рис. 3. Еквівалентні перетворення часових сіток Петрі

Розглянемо один з прикладів перетворень для слабкого типу еквівалентності:

Періодична вхідна послідовність та періодичне спостерігання.

,

, , :

.

.

.

.

У подаванні передатної функції та формул рівняння станів часової сітки Петрі з кратними дугами використано операції багатозначної (непереривної) логіки. Далі розв’язано задачу синтезу функцій непереривної логіки (ФНЛ) заданих табличне.

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

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

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

У 3 розділі – "Клани систем лінійних алгебраїчних рівнянь" – здійснено узагальнення функціональної сітки Петрі для довільних систем лінійних алгебраїчних рівнянь над кільцем зі знаком. Відповідну підмножину рівнянь названо кланом. Застосування композиції кланів дозволяє прискорити розв’язання лінійних систем, що є надто важливо для аналізу сіток Петрі, оскільки відомі алгоритми розв’язання диофантових систем у цілих невід’ємних числах мають експонентну обчислювальну складність.

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

Нехай задано систему лінійних алгебраїчних рівнянь вигляду |

, | (3)

Припустімо, що є відомий метод, котрий дозволяє розв’язати таку систему й подати загальний розв’язок однорідної системи () у формі |

,

де – матриця базисних розв’язків, а – вектор-стовпець вільних змінних. І загальний розв’язок неоднорідної системи () подано у формі |

,

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

Подамо систему (3) у вигляді предиката |

,

де – рівняння системи:

,

– i-й рядок матриці . Позначимо множину невідомих системи. Розглянемо множину рівнянь системи . Впровадимо відношення на множині .

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

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

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

.

Нехай – загальний розв’язок системи для клану .

Теорема. Подана нижче система еквівалентна до вихідної однорідної системи (1):

Здобуто подавання результатів у матричній формі: |

, .

де – загальний розв’язок системи композиції кланів ; – об'єднана матриця, побудована з , ; – об'єднана матриця, побудована з розв’язків систем для усіх кланів.

Для неоднорідної системи отримано |

, , .

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

,

де – кількість кланів, – максимум серед розміру клану й кількості контактних змінних, – складність розв’язання лінійної системи розміру . Для експонентних методів розв’язання систем отримуємо прискорення

.

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

Рис. 4. Колапс підграфів

Оптимізаційну задачу формалізовано як

I. | II.

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

Далі розроблено методи розв’язання задачі оптимального реберного колапсу (рис. 5) зваженого графа. Процес колапсу графа подано як

,

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

Рис. 5. Реберний колапс

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

Теорема. Ширина колапсу не перевищує суму ваги максимального ребра кістяка і ваг ребер, які залишилися:

, где – кістяк графа .

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

, .

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

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

Розроблено алгоритми композиційного розв’язання систем лінійних алгебраїчних рівнянь для обчислення загального розв’язку системи в довільному кільці зі знаком; забезпечено їхню інваріантість стосовно базового методу розв’язання системи, поданого зовнішнім модулем. До зовнішнього модуля також інкапсульовано алгоритми обчислення результатів операцій додавання, множення та знака елемента. Для роботи із системами великої розмірності використано спеціальний формат зберігання ненульових елементів разом з їхніми індексами, що забезпечує компактність інформації; усі проміжні результати обчислень зберігаються у зовнішніх файлах. Алгоритм використовує чотири основних модулі: Deborah – декомпозиція; Solve – розв’язання системи рівнянь; Joіnt – побудова об'єднаної матриці розв’язків для кланів; Contact – побудова системи композиції; Mmul – множення матриць. Подано деталізовані схеми алгоритмів роботи модулів Contact та Joіnt Сі-подібною псевдомовою, а також скрипт композиційного розв’язання для системи Unіx. Текст програми Adrіana із вбудованим модулем розв’язання системи методом Тудіка для знаходження інваріантів сіток Петрі наведено в Додатку Д.

У 4 розділі – "Синтез моделей Петрі та верифікація телекомунікаційних протоколів" – запропоновано використовувати сітки Петрі як універсальну мову специфікації телекомунікаційних протоколів. Виконано побудову моделі Петрі протоколу BGP з помітним відображенням окремих повідомлень і моделі Петрі протоколу TCP з помітним відображенням полів заголовка пакетів протоколу. Розроблено методи синтезу моделей Петрі протоколів за стандартними специфікаціями з використанням проміжної мови взаємодіючих послідовних процесів (ВПП) Хоара. Подано метод композиційного обчислювання інваріантів у параметричній формі для нескінченних сіток Петрі з регулярною структурою на прикладі верифікації протоколів Ethernet. Виконано синтез моделі Петрі протоколу електронної комерції IOTP. Виконано верифікацію протоколів ECMA (Додаток А), BGP, TCP, IOTP у процесі композиції функціональних сіток Петрі, що забезпечило істотні прискорення обчислень.

Побудовану модель протоколу TCP зображено на рис. 6. Віднайдено декомпозицію моделі на функціональні підсітки, подану на рис. 7; різні варіанти послідовної композиції моделі зображено на рис. 8. Показано, що колапс графа декомпозиції Z1+Z4; Z2+Z3; Z1,4+Z2,3 є оптимальним і має ширину, яка дорівнює чотирьом. Виконано обчислення інваріантів моделі протоколу в процесі послідовної композиції з деталізованим подаванням проміжних результатів. Здобута матриця базисних розв’язків

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

Рис. 6. Модель протоколу TCP

Рис. 7. Декомпозиція моделі протоколу TCP

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

Рис. 8. Варіанти послідовної композиції моделі протоколу TCP

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

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

Розглянуто критерії мінімізації кількості позицій та кількості дуг відповідно: |

,

.

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

Подані методи синтезу моделей Петрі застосовано для верифікації протоколу IOTP. За стандартними специфікаціями побудовано формулу ВПП трансакції Придбання:

Пропозиція:

.

.

.

.

Оплата:

.

.

.

.

.

Рис. 9. Модель трансакції Придбання протоколу IOTP

Доставка:

.

.

.

.

.

Придбання:

.

Потім синтезовано модель Петрі трансакції, подану на рис. 9. Верифікація моделі Петрі виконано за допомогою програми Adrіana (розділ 3, Додаток Д), подано граф функціональних підсіток.

Метод композиційного обчислювання інваріантів у параметричній формі призначений для обчислення інваріантів нескінченних сіток Петрі з регулярною структурою. Особливості застосування методу розглянуто на прикладі верифікації протоколів Ethernet з архітектурою спільної шини. На рис. 10 наведено приклад моделі для чотирьох робочих станцій.

Рис. 10. Модель шини Ethernet с чотирма робочими станціями

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

Віднайдено її параметричний розв’язок:

.

І, на завершення, віднайдено параметричний розв’язок для p-інваріантів:

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

У 5 розділі – "Моделі телекомунікаційних систем та мереж" – подано методологію побудови моделей у формі розфарбованих сіток Петрі в середовищі моделюючої системи CPN Tools за допомогою композиції моделей компонентів, що вони є функціональними підсітками або підсітками з контактними позиціями. Для вимірювання функціональних характеристик моделі в процесі імітації динаміки сітки Петрі запропоновано метод вимірювальних фрагментів. Виконано побудову моделей комутованої Ethernet, маршрутизованих IP-мереж, мереж з комутацією міток MPLS, мобільних сенсорних мереж Bluetooth. Розроблено вимірювальні фрагменти для оцінки часу відгуку мережі для Ethernet, вимірювання трафіка для IP та MPLS мереж, ефективності використання адресного простору для мереж Bluetooth.

Вихідною інформацією для побудови моделей Ethernet є структурна схема мережі (рис.11).

Рис. 11. Структурна схема локальної обчислювальної мережі

За структурною схемою збирається головна сторінка моделі (рис. 12).

Рис. 12. Головна сторінка моделі

Основним компонентом є підмодель комутатора, яка набирається необхідною кількістю моделей порту (рис. 13):

Рис. 13. Модель порту комутатора

Компонентами моделі є підмоделі робочої станції та сервера (рис. 14).

а) робоча станція | б) сервер

Рис. 14. Моделі прикінцевих пристроїв

Для задавання атрибутів елементів сітки Петрі в CPN Tools застосовано мову CPN ML; далі наведено опис використовуваних типів даних, змінних та функцій:

Рис. 15. Опис типів даних, змінних та функцій

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

Побудовано моделі локальних мереж диспетчерських центрів залізниці, оснащених програмним забезпеченням “ГИД Урал-ВНИИЖТ”. За специфікаціями використовуваних програмних та апаратних засобів обчислено характеристики елементів моделі; подано методику масштабування часів. В процесі імітації динаміки моделі обчислюється час відгуку мережі, який відрізняється від результатів вимірювань на реальних мережах, поданих у дисертаційній роботі, не більше ніж на шість відсотків (трасування проходження фреймів у моделі наведено у Додатку В).

Для IP та MPLS мереж побудовано типові моделі IP-маршрутизатора, LSR-маршрутизатора, LSR/LER-маршрутизатора, а також термінальних мереж. На прикладі фрагмента Європейської магістралі Інтернет виконано порівняльну оцінку ефективності IP та MPLS мереж. Здобуто збільшення пропускної здатності мережі в 1,7 раза для фрагмента, який нараховує 7 маршрутизаторів та 24 термінальні мережі.

Рис. 16. Модель вимірювальної робочої станції

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

ВИСНОВКИ

Для розв’язання наукової проблеми доведення коректності і оцінки ефективності телекомунікаційних систем у дисертаційній роботі подано методи синтезу моделей Петрі телекомунікаційних протоколів за стандартними специфікаціяхми, методи композиції моделей Петрі телекомунікаційних систем та мереж, методи оцінки функціональних характеристик побудованих моделей, а також методи композиційного аналізу моделей Петрі великої розмірності. Окрім того, розроблено ефективні алгоритми композиційного аналізу сіток Петрі, подано їхню програмну реалізацію. Здійснено верифікацію протоколів ECMA, BGP, TCP, IOTP; побудовано й досліджено моделі мереж Ethernet, MPLS, Bluetooth.

Розв’язано такі задачі:

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

2. Синтез моделей Петрі за стандартними специфікаціями протоколів: розроблено методи синтезу моделей Петрі протоколів з використанням проміжної мови взаємодіючих послідовних процесів Хоара; виконано синтез моделі Петрі протоколу електронної комерції IOTP; виконано верифікацію протоколів BGP, TCP, IOTP.

3. Побудова моделі Петрі за заданою структурною схемою телекомунікаційної системи або мережі й оцінка її функціональних характеристик: запропоновано виконувати синтез моделі Петрі за структурною схемою системи (мережі) у процесі композиції компонентів, які є функціональними підсітками чи підсітками з контактними позиціями; виконано побудову моделей мереж Ethernet, MPLS, Bluetooth; для експрес-оцінки функціональних характеристик побудованих моделей запропоновано метод вимірювальних фрагментів.

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

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

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

1. Zaitsev D.A. Functional Petri Nets. – Universite Paris-Dauphine, Cahier du Lamsade 224, Avril 2005. – 62 p.

2. Зайцев Д.А., Чорногала Е.Я. Синтез модели Петри и верификация протокола электронной коммерции IOTP // Радиотехника: Всеукр. межведомств. науч.-техн. сб. – 2006. – Вып. 144. – С. 28-35.

3. Зайцев Д.А. Передаточная функция сети Петри // Искусственный интеллект. – 2006. – №1. – С. 23-30.

4. Зайцев Д.А., Березнюк М.В. Исследование эффективности использования адресного пространства протокола Bluetooth // Радиоэлектроника. Информатика. Управление. – 2006. – №1. – C. 57-63.

5. Зайцев Д.А., Сакун А.Л. Исследование эффективности технологии MPLS с помощью раскрашенных сетей Петри // Зв'язок. – 2006. – Т. 65, №5. – С. 49-55.

6. Зайцев Д.А. Синтез моделей Петри телекоммуникационных протоколов // Труды Одесской национальной академии связи им. А.С.Попова. – 2005. – №2. – С. 36-42.

7. Зайцев Д.А. Верификация протокола TCP в процессе последовательной композиции модели Петри // Зв'язок. – 2006. – Т. 64, №4. – С. 49-58.

8. Зайцев Д.А. Последовательная композиция моделей Петри телекоммуникационных протоколов