Автореферат Методы анализа и синтеза моделей телекоммуникацонных систем на основе функциональных сетей Петри

МИНИСТЕРСТВО ТРАНСПОРТА И СВЯЗИ УКРАИНЫ ОДЕССКАЯ НАЦИОНАЛЬНАЯ АКАДЕМИЯ СВЯЗИ ИМ. А С. ПОПОВА

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

УДК 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; Программы создания встраиваемых модулей системы Tina автоматизированного анализа сетей Петри и временных сетей Петри лаборатории LAAS, Тулуза, Франция.

Цель и задачи исследования. Целью исследования является создание эффективных методов анализа и синтеза моделей Петри телекоммуникационных систем. Для достижения поставленной цели решены следующие задачи:

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

-    разработаны методы обеспечивающие существенное ускорение процессов верификации телекоммуникационных протоколов с помощью функциональных сетей Петри;

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

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

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

Объектом исследования являются процессы функционирования телекоммуникационных систем, в особенности, телекоммуникационные протоколы, представляющие собой наборы правил функционирования телекоммуникационных систем.

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

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

Научная новизна полученных результатов. Научная новизна полученных результатов состоит в том, что в работах соискателя впервые введены концепции функциональной сети Петри и клана линейной системы; построены основы теории функциональных сетей Петри и кланов линейных систем.

Получены следующие новые научные результаты:

-    разработаны методы синтеза моделей телекоммуникационных протоколов, заданных спецификациями в форме взаимодействующих последовательных процессов Хоара; выполнен синтез модели протокола IOTP;

-    разработаны методы верификации телекоммуникационных протоколов на основе композиционного анализа моделей Петри; выполнена верификация телекоммуникационных протоколов ECMA, Ethernet, BGP, TCP, IOTP с помощью композиционного анализа сетей Петри;

-    выполнено построение и исследование моделей Петри коммутируемых, маршрутизируемых сетей, сетей с коммутацией меток и мобильных сенсорных сетей; разработан метод измерительных фрагментов для оценки функциональных характеристик моделей в процессе имитации динамики раскрашенных временных сетей Петри.

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

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

-    получено представление передаточной функции временной сети Петри; разработаны методы эквивалентных преобразований и редукции сетей Петри для слабых типов эквивалентности на основе законов специально введенной для представления передаточной функции алгебры;

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

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

-    выполнено обобщение методов композиционного анализа для произвольных линейных систем в кольцах со знаком, представленное в терминах кланов линейных систем; предложена последовательная организация процессов композиции кланов, изучены свойства последовательной композиции на основе стягивания подграфов и стягивания рёбер; задача последовательной композиции формализована в терминах теории графов и названа оптимальным коллапсом взвешенного графа, получены оценки верхней и нижней границ ширины коллапса;

-    выполнено теоретическое обоснование и оценка вычислительной сложности метода Тудика решения линейных диофантовых систем в неотрицательных числах, традиционно применяемого для поиска инвариантов сетей Петри;

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

Разработано программное обеспечение декомпозиции и композиционного анализа сетей Петри Deborah и Adriana. Программное обеспечение предназначено для работы с сетями Петри большой размерности, обеспечивает существенные ускорения вычислений и распространяется как встраиваемые модули к известной системе Tina, используемой в качестве интерфейса для графического ввода и редактирования сетей Петри.

С помощью указанных модулей формально доказана корректность таких широко известных протоколов как 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 является суммой (объединением) конечного числа её минимальных функциональных подсетей (рис. 1);

-    разбиение множества T, заданное множеством минимальных функциональных подсетей, является порождающим семейством (базисом) множества функциональных подсетей сети Петри N.

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



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


Для представления декомпозиции на функциональные подсети предложено использовать: сеть функциональных подсетей (рис. 2а), ориентированный граф (рис. 2б), неориентированный граф (рис. 2в). Сеть функциональных подсетей является наиболее детализированной формой


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

б) ориентированный граф    в) неориентированный граф

а) сеть функциональных подсетей


функциональных подсетей    функциональных подсетей

Рис. 2. Представление декомпозиции

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

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

Затем исследована передаточная функция функциональной сети Петри. Функциональная сеть рассматривается как динамическая система, преобразующая входной поток фишек, направляемый во входные позиции в выходной поток фишек, наблюдаемый в выходных позициях. Целью исследования является получение представления передаточной функции для выполнения эквивалентных преобразований сетей. Редукция, используемая для анализа сетей Петри большой размерности, является частным случаем эквивалентных преобразований, сокращающих размерность сети.

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

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

Рис. 3. Эквивалентные преобразования временных сетей Петри

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

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

ФНЛ всегда принимает значение одного из своих аргументов либо его отрицания. Кроме того, значение функции полностью определяется способом упорядочения аргументов и их отрицаний с помощью отношения <. Таким образом, произвольная ФНЛ может быть однозначно представлена таблицей, в которой перечислены все варианты упорядочения аргументов и их отрицаний и указаны значения функции для каждого варианта. Такие таблицы называют таблицами выбора.

Введено понятие перекрывающихся строк таблицы выбора. Доказано, что таблица выбора, задаёт функцию непрерывной логики тогда и только тогда, когда она не содержит перекрывающихся строк. Введены понятия конституэнты минимума и конституэнты максимума строк таблицы выбора. Доказано, что произвольная таблица выбора T, не содержащая перекрывающихся строк, задает функцию непрерывной логики, равную дизъюнкции конституэнт максимума строк таблицы (конъюнкцию конституэнт минимума строк таблицы).

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

В 3 разделе - «Кланы систем линейных алгебраических уравнений» выполнено обобщение функциональной сети Петри для произвольных систем линейных алгебраических уравнений над кольцом со знаком. Соответствующее подмножество уравнений названо кланом. Применение композиции кланов позволяет ускорить решение линейных систем, что особенно важно для анализа сетей Петри, поскольку известные алгоритмы решения диофантовых систем в целых неотрицательных числах имеют экспоненциальную вычислительную сложность.

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

Пусть задана система линейных алгебраических уравнений вида:


где к - количество кланов, p - максимум среди размера клана и количества контактных переменных, M(p) - сложность решения линейной системы размера p. Для экспоненциальных методов решения систем M(q) = 2q получаем ускорения

AccE (q) = 2q-p .

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

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

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

Теорема. Ширина коллапса не превышает сумму веса максимального ребра остова и весов оставшихся рёбер:

Так как вопрос об NP-полноте задачи оптимального коллапса является открытым, далее предложен и статистически обоснован путём вычислительных экспериментов со случайными графами эвристический алгоритм коллапса, основанный на одношаговой стратегии стягивания ребра максимального веса.

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

Разработаны алгоритмы композиционного решения систем линейных алгебраических уравнений для вычисления общего решения системы в произвольном кольце со знаком; обеспечена их инвариантность по отношению к базовому методу решения системы, который представлен внешним модулем. Во внешний модуль также инкапсулированы алгоритмы вычисления результатов операций сложения, умножения и знака элемента. Для работы с системами большой размерности использован специальный формат хранения ненулевых элементов вместе с их индексами, обеспечивающий компактность информации; все промежуточные результаты вычислений хранятся во внешних файлах. Алгоритм использует четыре основных модуля: Deborah - декомпозиция; Solve - решение системы уравнений; Joint -построение объединённой матрицы решений для кланов; Contact - построение системы композиции; Mmul - умножения матриц. Представлены детализированные схемы алгоритмов работы модулей Contact и Joint на Си-подобном псевдоязыке, а также скрипт композиционного решения для системы Unix. Текст программы Adriana со встроенным модулем решения системы методом Тудика для нахождения инвариантов сетей Петри приведен в Приложении Д.

В 4 разделе - «Синтез моделей Петри и верификация телекоммуникационных протоколов» предложено использовать сети Петри как универсальный язык спецификации телекоммуникационных протоколов. Выполнено построение модели Петри протокола BGP с различимым отображением отдельных сообщений и модели Петри протокола TCP с различимым отображением полей заголовка пакетов протокола. Разработаны методы синтеза моделей Петри протоколов по стандартным спецификациям с использованием промежуточного языка взаимодействующих последовательных процессов (ВПП) Хоара. Представлен метод композиционного вычисления инвариантов в параметрическом виде для бесконечных сетей Петри с регулярной структурой на примере верификации протоколов Ethernet. Выполнен синтез модели Петри протокола электронной коммерции IOTP. Выполнена верификация протоколов ECMA (Приложение А), BGP, TCP, IOTP в процессе композиции функциональных сетей Петри, что обеспечило существенные ускорения вычислений.

Построенная модель протокола TCP изображена на рис. 6.

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

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

позволяет сделать вывод, что модель р-инвариантна, так как, например, сумма всех базисных решений содержит только натуральные компоненты. Аналогичным образом с использованием декомпозиции двойственной сети Петри доказана t-инвариантность модели. Для подтверждения результатов выполнено вычисление инвариантов обычным способом, а также построение и исследование свойств графа достижимых маркировок сети Петри.

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

Отмечено, что в связи с ростом сложности стандартных спецификаций протоколов, что косвенно подтверждается ростом объема спецификаций, трудоёмкость верификации протоколов всё более обуславливается трудоёмкостью построения моделей, имеющих объёмы порядка тысяч элементов сети Петри. Выполнен анализ традиционных языков спецификации протоколов.

Рис. 8. Варианты последовательной композиции модели протокола TCP

Предложено использовать в качестве промежуточного языка, в который естественным образом трансформируются исходные вербальные спецификации протоколов, ВПП. Последовательный процесс описывается с помощью трёх базисных операций: следования (^); рекурсии и выбора (|); Для представления взаимодействия Хоаром введена операция параллельной композиции процессов (||).

Доказано, что представлением последовательного процесса является конечный автомат, предложена формализация задачи синтеза сети Петри, заданной конечным автоматом в виде системы

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

Доставка:

ConsumerDelivery — WhatDeliverDecision ^ PutWhatDeliver ^ GetHowDeliver ^

CheckDeliverylnfo ^ PutDelivery Re quest ^ GetDelivery Re sponse ^ CheckDeliveryNote. MerchantDelivery — GetWhatDeliver ^ CheckWhatDeliver ^ PutHowDeliver. DeliveryHandlerDelivery — GetDelivery Re quest ^ CheckDelivery Re quest ^

PutDelivery Re sponse.

Delivery — ConsumerDelivery || MerchantDelivery || DeliveryHandlerDelivery.

HowDeliver — Delivery || Organization || Order.

Delivery Re quest — Status || Delivery || Organization || Order.

Delivery Re sponse — Status || DeliveryNote .

Приобретение:

TransPerchase — Offer ^ Payment ^ Deliver ^ TransPurchase.

Затем синтезирована модель Петри транзакции, представленная на рис. 8. Верификация

модели Петри выполнена с помощью программы Adriana (раздел 5, Приложение Д), представлен

граф функциональных подсетей.

Метод композиционного вычисления инвариантов в параметрической форме предназначен

для вычисления инвариантов бесконечных сетей Петри с регулярной структурой. Особенности

применения метода рассмотрены на примере верификации протоколов Ethernet с архитектурой

общей шины. На рис. 10 приведен пример модели, для четырёх рабочих станций:

Получено её параметрическое решение:

Так как, например, при выборе суммы всех базисных решений получаем инвариант со всеми натуральными компонентами, то модель Ethernet с топологией общей шины и произвольным количеством к рабочих станций является р-инвариантной сетью Петри.

В 5 разделе - «Модели телекоммуникационных систем и сетей» представлена методология построения моделей в форме раскрашенных сетей Петри в среде моделирующей системы CPN Tools с помощью композиции моделей компонентов, являющихся функциональными подсетями, либо подсетями с контактными позициями. Для измерения функциональных характеристик модели в процессе имитации динамики сети Петри предложен метод измерительных фрагментов. Выполнено построение моделей коммутируемой Ethernet, маршрутизируемых IP-сетей, сетей с коммутацией меток MPLS, мобильных сенсорных сетей Bluetooth. Разработаны измерительные фрагменты для оценки времени отклика сети для Ethernet, измерения трафика для IP и MPLS сетей, эффективности использования адресного пространства для сетей Bluetooth.

Исходной информацией для построения моделей Ethernet является структурная схема сети (рис.11).

Scheme of sample switched LAN

Рис. 11. Структурная схема ЛВС По структурной схеме собирается главная страница модели (рис. 12).

Model of LAN

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

Основным компонентом является подмодель коммутатора, набираемая необходимым количеством моделей порта:

Рис. 13. Модель порта коммутатора Компонентами модели являются подмодели рабочей станции и сервера:

а)рабочая станция

б) сервер

Рис. 14. Модели оконечных устройств

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

color mac = INT timed; color portnum = INT; color nfrm = INT;

color sfrm = product nfrm * INT timed;

color frm = product mac * mac * nfrm timed;

color seg = union f:frm + avail timed;

color swi = product mac * portnum;

color swf = product mac * mac * nfrm * portnum timed;

color remsv = product mac * nfrm timed;

var src, dst, target: mac;

var port: portnum;

var nf, rnf: nfrm;

var t1, t2, s, q, r: INT;

color Delta = int with 1000..2000;

fun Delay() = Delta.ran();

color dex = int with 100..200;

fun Dexec() = dex.ran();

color dse = int with 10..20;

fun Dsend() = dse.ran();

color nse = int with 10..20;

fun Nsend() = nse.ran();

fun cT()=IntInf.toInt(!CPN'Time.model_time);


Рис. 15. Описания типов данных, переменных и функций

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

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

Для 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.    Зайцев Д.А. Последовательная композиция моделей Петри телекоммуникационных протоколов // Зв'язок. - 2006. - Т. 61, №1. - С. 45-50.

9.    Зайцев Д.А. Последовательная композиция кланов линейных систем // Системш дослщження та шформацшш технологи. - 2006. - №2. - С. 121-137.

10.    Зайцев Д.А. Композиционный анализ сетей Петри // Кибернетика и системный анализ. - 2006.

- № 1. - С. 143-154.

11.    Зайцев Д.А. О реализации композиционных алгоритмов решения систем линейных уравнений // Управляющие системы и машины. - 2006. - №3. - С. 32-41.

12.    Зайцев Д.А., Шмелёва Т.Р. Измерение характеристик одноуровневой коммутируемой сети с помощью параметрической модели Петри // Радиотехника: Всеукр. межведомств. науч.-техн. сб. - 2005. - Вып. 142. - C. 40-47.

13.    Зайцев Д.А., Шмелёва Т.Р. Параметрическая модель Петри одноуровневой коммутируемой сети // Труды Одесской национальной академии связи им. А.С.Попова. - 2005. - № 1. - C. 3340.

14.    Зайцев Д.А. Программное обеспечение для декомпозиции двудольных орграфов // Научные труды Донецкого национального технического университета, серия "Информатика, кибернетика и вычислительная техника". - 2005. - Вып. 93. - C. 68-79.

15.    Зайцев Д.А. Решение линейных систем с помощью декомпозиции // Системш дослщження та шформацшш технологи. - 2005. - №2. - C. 131-143.

16.    Зайцев Д.А. Измерительные фрагменты в моделях Петри телекоммуникационных сетей // Зв'язок. - 2005. - Т. 54, №2. - C. 65-71.

17.    Зайцев Д.А. Верификация телекоммуникационных протоколов с помощью декомпозиции сетей Петри // Зв'язок. - 2005. - Т. 53, №1. - C. 41-47.

18.    Зайцев Д.А. Решение фундаментального уравнения сетей Петри в процессе композиции функциональных подсетей // Искусственный интеллект. - 2005. - № 1. - C. 59-68.

19.    Зайцев Д.А. Последовательная композиция функциональных подсетей // Труды Одесской национальной академии связи им. А.С.Попова. - 2004. - № 3. - C. 33-40.

20.    Зайцев Д.А. Декомпозиция сетей Петри // Кибернетика и системный анализ. - 2004. - №5. -C. 131-140.

21.    Зайцев Д.А. Инварианты временных сетей Петри // Кибернетика и системный анализ. - 2004. -Т. 40, № 2. - C. 92-106.

22.    Зайцев Д.А., Шмелёва Т.Р. Моделирование коммутируемой локальной сети раскрашенными сетями Петри // Зв'язок. - 2004. - Т. 46, № 2. - C. 56-60.

23.    Зайцев Д.А. Инвариантность модели Петри протокола TCP // Труды Одесской национальной академии связи им. А.С.Попова. - 2004. - № 2. - C. 19-27.

24.    Зайцев Д.А. К вопросу о вычислительной сложности метода Тудика // Искусственный интеллект. - 2004. - № 1. - C. 29-37.

25.    Зайцев Д.А. Теоретическое обоснование метода Тудика // Научные труды Донецкого национального технического университета, серия "Информатика, кибернетика и вычислительная техника". - 2004. - Вып. 74. - C. 286-293.

26.    Зайцев Д.А. Декомпозиция протокола ECMA // Радиотехника: Всеукр. межведомств. науч. -техн. сб. - 2004. - Вып. 138. - C. 75-82.

27.    Зайцев Д.А. Верификация протоколов Ethernet // Труды Одесской национальной академии связи им. А.С.Попова. - 2004. - № 1. - C. 42-48.

28.    Зайцев Д.А. Инварианты функциональных подсетей // Труды Одесской национальной академии связи им. А.С.Попова. - 2003. - № 4. - C. 57-63.

29.    Зайцев Д.А., Сарбей В.Г., Слепцов А.И. Синтез функций непрерывной логики заданных таблично // Кибернетика и системный анализ. - 1998. - № 2. - C. 47-56.

30.    Зайцев Д.А., Слепцов А.И. Уравнение состояний и эквивалентные преобразования временных сетей Петри // Кибернетика и системный анализ. - 1997. - № 5. - C. 59-76.

31.    Зайцев ДА., Шмелёва Т.Р. Основы построения параметрических моделей Петри коммутируемых сетей // Моделирование и компьютерная графика: Материалы 1 -й международной научно-технической конференции. - Донецк: ДонНТУ. - 2005. - С. 207-215.

32.    Zaitsev D.A. Verification of Protocol BGP via Decomposition of Petri Net Model into Functional Subnets // Proc. of the Design, Analysis, and Simulation of Distributed Systems Symposium. - San Diego (USA). - 2005. -P. 72-78.

33.    Zaitsev D.A. An Evaluation of Network Response Time using a Coloured Petri Net Model of Switched LAN // Proc. of Fifth Workshop and Tutorial on Practical Use of Coloured Petri Nets and the CPN Tools. - Aarhus (Denmark). - 2004. - P. 157-167.

34.    Zaitsev D.A. Verification of protocol TCP via decomposition of Petri net model into functional subnets // Proc. of the Poster session of 12th Annual Meeting of the IEEE / ACM International Symp. on Modeling, Analysis, and Simulation of Computer and Telecommunication Systems. - Volendam (Netherlands). - 2004. - P. 73-75.

35.    Zaitsev D.A. Solving the fundamental equation of Petri net using the decomposition into functional subnets // 11th Workshop on Algorithms and Tools for Petri Nets. - Paderborn (Germany). - 2004. -P. 75-81.

36.    Zaitsev D.A. Decomposition-based calculation of Petri net invariants // Proc. of Workshop on Token based computing of the 25-th International conf. on application and theory of Petri nets. - Bologna (Italy). - 2004. - P. 79-83.

37.    Zaitsev D.A. Switched LAN Simulation by Colored Petri Nets // Mathematics and Computers in Simulation. - 2004. - Vol. 65, № 3. - P. 245-249.

38.    Zaitsev D.A. Formal grounding of Toudic method // Proc. of the 10th Workshop "Algorithms and Tools for Petri Nets". - Eichstaett (Germany). - 2003. - P. 184-190.

39.    Zaitsev D.A. Subnets with input and output places // Petri Net Newsletter. - Vol. 64, April 2003. -P. 3-6. Cover Picture Story.

Зайцев Д.А. Методи аналiзу та синтезу моделей телекомушкацшних систем на основi функцюнальних сггок Петрь - Рукопис.

Дисертащя на здобуття наукового ступеня доктора техшчних наук за спещальшстю

05.12.02 - телекомушкацшш системи та мережь - Одеська нацюнальна академiя зв’язку iм. О.С.Попова, Одеса, 2006.

Для аналiзу деталiзованих моделей Петрi телекомушкацшних протоколiв розроблено основи теорп функцюнальних аток Петрь Побудовано методи редукци часових аток Петрi на основi е^валентних перетворень формул передатно'1 функцп; дослщжено слабю типи е^валентносп аток. Розроблено методи синтезу функцш непереривно'1 логiки заданих табличне. Розроблено основи теорп клашв систем лшшних алгебршчних рiвнянь, якi дозволяють прискорити розв’язання систем в кiльцях зi знаком, а також вiдповiднi алгоритми та програмне забезпечення. Розроблено методи синтезу моделей Петрi за стандартними специфшащями телекомушкацшних прототшв з використанням допомiжноi мови взаeмодiючих послiдовних процеав Хоара. Синтезовано модель Петрi протоколу електронноi комерцii IOTP. Виконано верифшацш протоколiв ECMA, BGP, TCP, IOTP. Розроблено метод композицшного обчислення iнварiантiв нескiнченних сiток Петрi з регулярною структурою; метод застосовано для доказу iнварiантностi моделi Петрi мереж1 Ethernet з тополопею спiльноi шини. Розроблено методи побудови моделей телекомушкацшних систем через композищю моделей компонентив, оцшки функцiональних характеристик моделей; дослiджено: комутовану Ethernet, мереж1 з комутацiею м^ок MPLS, мережi Bluetooth.

Ключов1 слова: телекомушкацшна система, телекомунiкацiйний протокол, функцюнальна сiтка Петрi, клан, аналiз, синтез.

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

Диссертация на соискание учёной степени доктора технических наук по специальности

05.12.02 - телекоммуникационные системы и сети. - Одесская национальная академия связи им. А.С.Попова, Одесса, 2006.

Для анализа детализированных моделей Петри телекоммуникационных протоколов разработаны основы теории функциональных сетей Петри. Построены методы редукции временных сетей Петри на основе эквивалентных преобразований формул передаточной функции; исследованы слабые типы эквивалентности сетей. Разработаны методы синтеза функций непрерывной логики заданных таблично. Разработаны основы теории кланов систем линейных алгебраических уравнений, позволяющие ускорять решение систем в кольцах со знаком, а также соответствующие алгоритмы и программное обеспечение. Разработаны методы синтеза моделей Петри по стандартным спецификациям телекоммуникационных протоколов с использованием промежуточного языка взаимодействующих последовательных процессов Хоара. Синтезирована модель Петри протокола электронной коммерции IOTP. Выполнена верификация протоколов ECMA, BGP, TCP, IOTP. Разработан метод композиционного вычисления инвариантов бесконечных сетей Петри с регулярной структурой; метод применён для доказательства инвариантности модели Петри сети Ethernet с топологией общей шины. Разработаны методы построения моделей телекоммуникационных систем путем композиции моделей компонентов, оценки функциональных характеристик моделей; исследованы: коммутируемая Ethernet, сети с коммутацией меток MPLS, беспроводные сети Bluetooth.

Ключевые слова: телекоммуникационная система, телекоммуникационный протокол, функциональная сеть Петри, клан, анализ, синтез.

Zaitsev D.A. Methods of analyses and synthesis of telecommunication systems models on the base of functional Petri nets. - The manuscript.

The dissertation is competing for the degree of Dr. Sci. Tech. on a speciality 05.12.02 -telecommunication systems and networks. - Odessa National Telecommunication Academy named after A.S.Popov, Odessa, 2006.

Petri net models of real-life telecommunication protocols have a large scale but all known algebraic methods of Petri net analysis possess an exponential computation complexity. There is a problem of large-scale Petri nets analysis. To solve this problem the basis of functional Petri nets theory has been developed. Functional net has strongest restrictions on incidental arcs of contact places: input places have only output arcs and output places have only input acrs. Functional subnet is introduced in symmetric way. It was proved that: set of minimal functional subnet defines a partition of transitions’ set;

each functional subnet of a given Petri net may be obtained as composition (union) of finite number of minimal functional subnets; each contact place has no more than one incidental input functional subnet and not more than one output functional subnet; the net of functional subnets is a marked graph. For the representation of decomposition the net of functional subnets and graphs of decomposition (directed and undirected) were used. Two ways of decomposition were suggested: via logical equations solution and via ah-hoc algorithm of linear complexity. The software for decomposition named Deborah was developed.

The transmission function of functional net was studied for the class of timed Petri nets with multiply arcs. On the base of state equation the representation of transmission function was obtained. The transmission function was written as an expression in the special algebra, which contains arithmetic, logic operations and operation of timed delay. Weak functional equivalence of nets was introduced and studied with respect to special types of input sequences and moments of observation. The equivalent transformations of nets were implemented on the base of algebraic transformations of transmission function formulae. It allows the reduction of large-scale Petri nets. The task of continuous logic function given by choice table synthesis was solved. Special concepts of constituents of maximum and minimum were introduced and applied.

It was shown that the majority of tasks of Petri nets analyses may be reduced to solution of linear Diophantine equations in nonnegative integer numbers. The methods for speed-up of solution of an arbitrary linear algebraic system of equation under ring with sign were developed. The concept of functional subnet was generalized for linear systems on the base of clan concept. Clan was introduced as a subset of equations united with a transitive closure of closeness relation consisting in possessing a variable with a coefficient of the same sign. Clans define the specific block structure of system’s matrix and provide the system’s solving via composition of clans’ general solutions. Speed-up of computation is guaranteed in the case the system is decomposed in more than one clan and at the usage of basic solution method with complexity larger than cube.

For the additional speed-up in the case the number of contact variables is greater than the maximal size of clans the sequential way of decomposition was proposed. The speed-up is obtained at the expense of solution of a series of composition systems with lesser dimension. For implementation of sequential composition the undirected graph of decomposition was considered. Two ways of sequential composition were studied: via contracting subgraphs and via contracting of edges. The corresponding optimization task was named an optimal collapse of weighted graph. For solution of edge collapse task by the method of branches and bounds the estimations of upper and lower bound for the width of collapse were obtained. A heuristic algorithm of optimal collapse on the base of one-step strategy of maximal weight edge contracting was introduced and statistically grounded. The software for compositional solution of systems named Adriana was developed. As an auxiliary task the formal grounding and detailed estimation of computation complexity for Toudic method were obtained.

The specification languages of telecommunication protocols were studied. It was proposed to use Petri net as a universal language of protocols specification. To control the level of models abstraction it was proposed to represent either the whole message or headers’ fields by separate tokens. The models of protocols BGP and TCP were constructed and verified using composition of functional subnets.

With the growth of protocols number and their complexity the construction of Petri net model on a given standard specification of a protocol becomes most laborious. To solve this problem the usage of intermediate language of Hoare’s communicating sequential processes (CSP) was suggested. Then the task of Petri net synthesis on a given CSP formulae was solved. This approach was illustrated on the example of Petri net synthesis for electronic commerce protocol IOTP. The verification of protocol was implemented via developed compositional methods.

The model-driven development of telecommunication systems becomes a prospective direction. It was suggested to compose colored Petri net models of telecommunication systems and networks via the composition of components’ models represented with functional subnets and subnets with contact places. The library of components for switched Ethernet, MPLS and Bluetooth was constructed. For express estimation of functional characteristics the method of measuring fragments was introduced. With such fragments the tasks of switched Ethernet response time, MPLS effectiveness and Bluetooth address space usage effectiveness estimation were solved.

For analysis of infinite Petri nets with regular structure the method of compositional calculation of invariants in parametric form was developed. The method was illustrated on the example of Ethernet with bus topology verification. The invariance of the protocol was proved for an arbitrary number of workstations on the bus.

Keywords: telecommunication system, telecommunication protocol, functional Petri net, clan, analysis, synthesis.