автореферат диссертации по радиотехнике и связи, 05.12.13, диссертация на тему:Анализ, моделирование и верификация высокоуровневых протоколов эффективного информационного взаимодействия открытых телекоммуникационных систем

Корнилов Александр Михайлович

Анализ, моделирование и верификация высокоуровневых протоколов эффективного информационного взаимодействия открытых телекоммуникационных систем

Специальность 05.12.13 - «Системы, сети и устройства телекоммуникаций»

Автореферат диссертации на соискание учёной степени кандидата технических наук

Научный руководитель -к.т.н., доцент В.Ю. Михайлов

Москва, 2010

7 6 т 2т

004617792

Работа выполнена на кафедре 402 «Радиосистемы управления и передачи информации» Московского авиационного института (государственного технического университета)

Научный руководитель: кандидат технических наук, доцент

Михайлов Владимир Юрьевич

Официальные оппоненты:

доктор технических наук, профессор Баринов Виктор Владимирович Заведующий кафедрой «Телекоммуникационные системы» Московского государственного института электронной техники (технического университета)

Ведущая организация:

кандидат технических наук Ватутин Сергей Иванович

Начальник, сектора ОАО «Российские космические

системы»

ОАО"НИИСА"

Защита диссертации состоится 28 декабря 2010 г. в зале учёного совета факультета № 4 на 3 этаже корпуса 24 Б (Ленинградское шоссе, д. 5) в 10 часов 00 минут на заседании диссертационного совета Д 212.125.02 при Московском авиационном институте (государственном техническом университете) по адресу 125993, г. Москва, Волоколамское шоссе д. 4.

С диссертацией можно ознакомиться в библиотеке МАИ.

Дата рассылки автореферата: 26 ноября 2010 г.

Ученый секретарь диссертационного coвeía Д 212.125.02 К.Т.Н., доц.

Петраков А. М.

Общая характеристика работы

Актуальность темы исследования.

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

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

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

также методов, существенно ускоряющих процесс тестирования по сравнению с существующими.

Цель работы.

Целью работы является разработка новых методов проектирования системных протоколов высокого уровня.

Объектом исследования в диссертационной работе являются распределённые системы, использующие ХМРР-протоколы, а предметом исследования - разработки методов проектирования высокоуровневых системных протоколов эффективного информационного взаимодействия.

Методы исследования.

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

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

Научная новизна работы.

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

2. Разработан метод проектирования системного протокола высокого уровня, имеющий высокую эффективность.

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

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

управления сменой логических каналов с сохранением сеанса.

Практическая значимость работы

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

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

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

4. Разработанные модели макрофункций и примитивов реализованы в виде стандартных ХМЬ-файлов, что позволяет использовать модели в различных средах проектирования.

Основные положения, выносимые на защиту.

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

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

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

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

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

Публикации.

Основные результаты изложены в 6 публикациях, в т.ч. 1 статья в изданиях, рекомендованных ВАК и двух монографиях.

Апробация работы.

Результаты исследования докладывались и обсуждались на Всероссийских конференциях и семинарах в 2004-2009 годах. Структура диссертационной работы.

Диссертация состоит из введения, 4 глав с 19 таблицами и 30 иллюстрациями, заключения, библиографического списка, состоящего из 54 наименований, и четырёх приложений. Общий объём работы составляет 167 страниц.

Основное содержание работы

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

В первой главе описаны основные принципы работы протокола ХМРР и протоколов, основанных на нём.

ХМРР (extensible Messaging Protocol and Presence) представляет собой открытый стандарт на основе языка XML (extensible Markup Language) для взаимодействия в режиме около реального времени (Instant Messaging) в распределённой гетерогенной среде. Протокол ХМРР реализуется на основе клиент/серверной архитектуре, где всё взаимодействие строится на базе четырёх типов сообщений:

- <stream:stream/> - открытие/закрытие ХМРР-сеанса;

- <iq/> - сообщение для получения, настройки настроек взаимодействия. Например, запрос списка контактов или осуществления звонков IP-телефонии (протокол Jingle);

- <message/> - обмен сообщениями между оконечными узлами (клиентами, программными агентами);

- <presence/> - обмен информацией о присутствии оконечных узлов.

Обоснования для использования протокола ХМРР могут быть

следующие: открытость (стандарт ХМРР открыт для доступа (RFC 3920 и RFC 3921)), кроссплатформенность (модуль обработки XML встроен в любую операционную систему и в открытом доступе библиотеки для работы ХМРР на языках С, С#, Python и др.) и расширяемость. Последнее означает, что на основе ХМРР можно создавать новые протоколы. Например, для передачи картинки с одной станции на другую можно расширить сообщение <message/>:

<message to="ash@lindows" from="dust@jabber.ru">

<body>

<frame>FF78x7 ...kk</frame> </body>

</message>

Курсивом обозначен новый тип данных. В данном случае тег <frame/> содержит изображение, представленное в Base64 кодировке.

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

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

В случае если клиенту необходимо сменить логический канал взаимодействия (подключиться к другому серверу или перейти с TCP протокола на HTTP протокол), он должен отключиться от сервера (закрыть сеанс) и повторно аутентифицироваться. Условия для смены логического канала могут быть различными. Например, мобильный клиент вышел из зоны обслуживания корпоративной точки доступа и вошёл в зону точки публичного доступа. Другой пример, срабатывание системы DIDS (Distributed Intrusion Detection System) в локальной сети. В одних случаях, смена логического канала может быть малозаметной, однако есть приложения, которые чувствительны к разрывам связи: прерывание разговора в 1Р-телефонии.

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

прерывая связи и не передавая повторно "лишних" данных (данных аутентификации).

Выводы к Главе 1:

1. Обосновано использование протокола ХМРР для построения телекоммуникационных, измерительных и управляющих систем.

2. В результате анализа протокола ХМРР и существующих систем выделены основные этапы информационного взаимодействия в реальном времени по протоколу ХМРР.

3. Разработаны принципы создания новых протоколов (расширений) на основе ХМРР, а также пути оптимизации информационного обмена в части минимизации передаваемых сообщений.

4. В результате анализа транспортов (TCP, UDP, HTTP и др.) выбран протокол HTTP.

5. Исследованы существующие методы построения каналов на основе протокола HTTP, выделены недостатки. Предложен метод организации логического канала на базе HTTP, сосоятщий из Web-cepaepa, объектов файловой системы и технологий распределённых программных объектов.

6. Предлагается способ проектирования корректных протоколов на основе макрофункций и примитивов ХМРР

7. Обоснована необходимость декомпозиции протокола ХМРР для получения макрофункций и примитивов протокола ХМРР.

8. Обоснована необходимость разработки протокола смены логических каналов с сохранением сеанса.

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

-1. Отсутствие статических блокировок. Это означает, что в протоколе не существует такого состояния или набора состояний, из которых нет переходов в другие состояния;

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

- 3. Однозначность соответствия состояний, т.е. отсутствие таких протокольных объектов, у которых одно состояние может сосуществовать с несколькими различными состояниями какого-либо другого объекта;

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

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

- 6. Отсутствие динамических блокировок. Это значит, что в протоколе отсутствует бесконечный цикл функционирования, при котором не производится полезная работа. Различают динамические блокировки, выход из которых логически невозможен (свойство 6а), и динамические блокировки, являющиеся следствием определённых временных характеристик протокола, например темпа обмена сообщениями (66).

- 7. Завершаемость (развитие), т.е. протокол всегда достигает конечного (терминального) состояния. Для циклических протоколов это свойство несколько видоизменяется. Эти протоколы должны обладать свойством развития, которое состоит в том, что протокол достигает своего начального состояния;

- 8. Самосинхронизация (восстановление после ненормальной работы). Это свойство подразумевает, что после возникновения ненормальной ситуации протокол за конечное время восстановит свое корректное функционирование.

В качестве формального аппарата анализа и проектирования протокола на основе ХМРР выбран аппарат сетей Петри. Для проверки соответствия корректности проектируемого протокола используются известные свойства сетей Петри такие как живость или активность (liveness), безопасность (safe) и ограниченность (bound). Живость сети Петри показывает выполнение свойств 1,4, б, 7, 8. Ограниченность и безопасность сети Петри показывает выполнение свойства 5.

Переход t сети <N, М0>, N = <Р, Т, В, F>, называется живым, если из любой достижимой из МО маркировки существует последовательность срабатываний, содержащая t.

Сеть Петри <N, М0>, N=<P, Т, В, F>, называется живой, если все её переходы живые.

Позиция р-маркированной сети Петри <N, М0>, N=<P, Т, В, F>, называется k-ограниченной, если для любой достижимой из МО маркировки М найдётся целое неотрицательное число к такое, что М(р) <= к.

Маркированная сеть Петри <N. М0>, N=<P, Т, В; F>, называется ограниченной, если для каждой её позиции р найдётся такое число к > 0, что р - к-ограниченная. Если для всех р из Р к <= 1, сеть называется безопасной.

Выводы к Главе 2:

1. Определены параметры, характеризующие корректность высокоуровневых системных протоколов.

2. Произведён анализ существующих подходов к верификации (проверка корректности) протоколов. Рассмотрены темпоральные (временные, модели последовательностей) и автоматные формализмы.Выделены достоинства и недостатки.

3. Для проверки корректности и моделирования высокоуровневых системных протоколов, создаваемых на основе макрофункций и примитивов ХМРР, выбран аппарат теории сетей Петри.

4. Рассмотрены существующие способы формального описания спецификации протоколов, в том числе Promela, ESTELLE, Lotus, SDL и др.

5. Проведён анализ текущего состояния теории сетей Петри для разработки и верификации протоколов! В качестве основных выделены следующие недостатки:

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

- увеличение временных затрат для оценки корректности протокола по мере усложнения получаемой модели (эта проблема получила название взрыв состояний (state explosion));

- создание корректной и адекватной модели требует высокой квалификации разработчика.

6. Обоснована необходимость разработки методики создания моделей и их анализа средствами сетей Петри для высокоуровневых системных протоколов.

7. Исследованы автоматизированные программные инструменты для работы с сетями Петри. Предложно использование инструмента Platform Independent Petri Editor 3.0 (PIPE 3.0)

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

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

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

Для этого была произведена декомпозиция протокола ХМРР, в результате которой была получена типизированная компонентная база проектирования системного протокола высокого уровня, состоящая из макрофункций и примитивов протокола ХМРР.

Ниже приведены основные полученные макрофункции и их описания:

• ОрепХМРР. Макрофункция для открытия ХМРР-сеанса.

• Яе§ХМРР. Макрофункция для регистрации узлов (сторон).

• АиШХМРР. Макрофункция для аутентификации сторон.

• БиЬзТоХМРР. Макрофункция для односторонней подписи.

• БиЬзВоЙуХМРР. Макрофункция для двусторонней подписи.

• Хс1е1ауХМРР. Макрофункция для отложенной доставки.

• вгоирМгщХМРР. Макрофункция управления группами.

• ConfXMPP. Макрофункция организации работы по типу "конференции".

В силу того, что не всегда достаточно макрофункций для отображения всех процессов, происходящих в высокоуровневом системном протоколе, в компонентную базу проектирования включены примитивы ХМРР:

• И^Зпс!. Примитив отправки запроса.

• РозЯеБЗпё. Примитив отправки положительного ответа на запрос.

• PosR.esR.cv. Примитив получения положительного ответа.

• NegResSnd. Примитив отправки негативного ответа на запрос.

• NegResRcv. Примитив получения негативного ответа.

• Гу^Бпс!. Примитив отправки сообщения.

• Примитив приёма сообщения.

Таким образом, упомянутые примитивы вместе с макрофункциями составляют единую базу проектирования.

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

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

Тогда протокол взаимодействия клиента А и датчика будет состоять из макрофункций ОрепХМРР, АиШХМРР, ЗцЬбТоХМРР, БиЬзРготХМРР, а также примитивов ^^Бпс! и К^Ясу. Соответственно, протокол взаимодействия клиентов А и В будет включать в себя макрофункции ОрепХМРР, АиЛХМРР, СопОШРР.

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

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

Функциональная сеть X, У) называется функциональной

подсетью сети N. если № является подсетью N. и кроме того, Ъ связана с оставшейся частью сети только посредством дуг, инцидентным контактным

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

Функциональные подсети Петри примитивов ХМРР состоят из позиций, характеризующих внутреннее состояние протокольной машины и контактных позиций.

Виды контактных позиций:

• внутренние контактные позиции. Отображают взаимодействие примитивов отдельной протокольной машины между собой;

• канальные контактные позиции. Отображают взаимодействие между собой протокольных машин.

• интерфейсные контактные позиции. Отображают связь с пользователем примитивов ХМРР (взаимодействие с внешним миром).

Все контактные позиции делятся на входные и выходные.

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

На основании теоремы Хэка о том, что если сеть Петри активная и безопасная, то она покрыта МО-компонентами, делается вывод о том, что при правильном совмещении соответствующих контактных позиций примитивов ХМРР, полученная сеть в результате агрегирования примитивов, моделирующая целевой протокол, будет активной и безопасной.

Показано, как проверить правильность агрегирования на основе Т-инвариантов (Т-циклов).

Выводы к Главе 3:

1. Произведена декомпозиция протокола ХМРР с целью формирования компонентной базы проектирования. В результате получен набор примитивов и макрофункций протокола ХМРР;

2. Разработаны эквивалентные корректные функциональные подсети Петри для моделирования и проверки корректности целевого высокоуровневого системного протокола, включающие внутренние, канальные и интерфейсные контактные позиции. Эквивалентные функциональные подсети Петри состоят из автоматных компонент и MG-компонент (Marked Graph, маркированные графы);

3. Разработаны правила агрегирования функциональных подсетей Петри макрофункций и примитивов ХМРР для получения модели целевого высокоуровневого протокола. В результате агрегирования гарантированно корректный протокол;

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

5. Созданы стандартные XML-файлы, содержащие модели примитивов и макрофункций, которые могут экспортироваться в другие среды разработки.

В четвёртой главе был разработан корректный высокоуровневый системный протокол смены логических каналов с сохранением сеанса на основании методов, приведённых в главе 3.

Первые шаги разработанного протокола (создание С1 и S1, аутентификация, обмен сообщениями) являются стандартными для ХМРР. Далее при возникновении необходимости перехода на новый логический, канал С2, клиент или сервер отправляет команду смены логического канала через С1. После создания и тестирования С2 все сообщения сеанса S1 будут

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

Сообщения разработанного системного протокола смены логических каналов с сохранением сеанса приведены в таблице 1.

Таблица 1. Сообщения и события системного протокола смены логических каналов.

: ч Сообщение/::; к событие Описание

! ш1 команда смсны каналов, исполиустся Иншямтором =

т2 команда лоддержкн службы смены каналов, используется Ответчиком 'и:1

команда о выбранном логическом канале, используется Ответчиком .¿г

" 11Й команда тестирования логического канала и передачи

■ЛкЧД"" ш5 команда тестирования логического канала и подтверждения получения::» параметров сеанса; используется ОтветчикомV

!Г)6 команда закрытая логического канала Инициатором з ян?

, ш7 ■ ' команда закрытия логического канала Ответчиком ■■ ■ :

команда, сигнализирующая об ошибке использовали» службы смены и; логического капала с сохраненном сеанса; используется Ответчиком?*®

команда отказ!! от использования предложении* каналов, ^пользуется: :й й; Ответчиком

г-Шк^3 * команда, сшналширующая о некорректном функционировании соч:ишного логического канала' ■ Л ■

событие, вызов сервиса смены логических каналов.

...... й : событие, параметры логического канала согласованы л

■ ............ *з- . событие, логический капал функционирует:«

■ :,...:: .«4- • событие, закрытие прежнего логического кашла

На основании методов, предложенных в главе 3 построена модель

протокола управления сменой логических каналов с сохранением сеанса (рис. 1.).

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

Разработаны сообщения на основе протокола ХМРР для протокола управления сменой логических каналов с сохранением сеанса.

Рис. 1. Модель протокола управления сменой логических каналов с сохранением сеанса.

Разработана структура системы, реализующей смену логических каналов с сохранением сеанса на основе технологии .NET Remoting (рис. 2а и 26).

Рис. 2а. Структура системы на основе технологии .NET Remoting.

Рис. 26. Структура системы на основе технологии .NET Remoting и файловой системы.

Разработаны программные модули и алгоритмы, реализующие протокол управления сменой логических каналов с сохранением сеанса на основе технологии .NET Remoting.

Выводы к Главе 4:

1. Определены цели, задачи и области применения системного протокола высокого уровня с сохранением сеанса;

2. Определены основные (глобальные) состояния и условия переходов между ними для протокольных машин системного высокоуровневого протокола смены логических каналов с сохранением сеанса;

3. Определены типы сообщений системного высокоуровневого протокола смены логических каналов с сохранением сеанса;

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

5. Доказана корректность системного высокоуровневого протокола смены логических каналов с сохранением сеанса;

6. Разработана спецификация системного высокоуровневого протокола смены логических каналов с сохранением сеанса.

В заключении приведены основные теоретические и практические результаты диссертационной работы.

В приложениях приведены: программный код на языке С# компонент системы, реализующих системный протокол высокого уровня смены логических каналов с сохранением сеанса, описание основных элементов платформы .NET Remoting.

Основные результаты работы

1. Разработана типизированная компонентная база проектирования системных протоколов высокого уровня, позволяющая эффективно использовать готовые модули (агрегаты).

2. Предложена методика тестирования системных протоколов высокого уровня, состоящая в оценке полноты и конечности протокольных процедур на основе инвариантов в терминах

сетей Петри, которая обеспечивает повышение быстродействия тестирования.

3. Предложен метод проектирования корректных системных протоколов высокого уровня, имеющего высокую эффективность по сравнению с существующими.

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

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

Основные результаты диссертации изложены в следующих публикациях:

1. Корнилов A.M. Разработка структуры системы безопасного управления информационным обменом подвижных объектов в реальном времени // Журнал «Вестник Московского авиационного института», т. 17, №5,2010 г. -М.: МАИ, 2010.-е. 154-157

2. Корнилов А. М. Использование современных технологий распределённого взаимодействия в задачах оперативного информационного обмена// Всероссийская конференция молодых ученых и студентов «Информационные технологии в авиационной и космической технике-2008». 21-24 апреля 2008 г. Москва. Тезисы докладов. - М.: Изд-во МАИ-ПРИНТ, 2008.-124с.-с. 65

3. Корнилов A.M. Принципы проектирования информационных систем взаимодействия в реальном времени // Информационные технологии и радиоэлектронные системы. Сборник докладов научно-технической

конференции, посвященной 100-летию со дня рождения И. С. Гоноровского. Москва, 19 апреля 2007 г. - М.: МАИ, 2007. - 276 с. - с. 88-93

4. Корнилов А.М. Анализ использования высокоуровневых протоколов информационного обмена // Информатизация и связь. Москва, №1,2005 г. -М.: Редакция журнала «Информатизация и связь», 2005. - 52 с. -с. 32-35

5. Корнилов A.M. Разработка и внедрение методов виртуализации каналов обмена данными клиент-серверных систем для информационного взаимодействия в реальном времени // Информационно-телекоммуникационные технологии. Всероссийская научно-техническая конференция. 19-26 сентября 2004 г. Сочи. Тезисы докладов. - М.: Издательство МЭИ, 2004. - 244 с. - с. 225 - 227

6. Корнилов A.M. Оптимизация информационного обмена в реальном времени // Информатизация и связь. Москва, №2,2004 г. - М.: Редакция журнала «Информатизация и связь», 2004. - 32 с. - с. 19-22

' Множительный центр МАИ (ГТУ) Заказ от££ //У.201 От. Тиражэкз.

Список терминов и условных сокращений.

Введение.

1. Постановка задачи.

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

1.2. Принципы и особенности использования протокола ХМРР.

1.3. Типовые задачи взаимодействия по протоколу ХМРР.

1.4. Принципы создания системных протоколов высокого уровня на основе ХМРР.

1.5. Способы доставки ХМРР сообщений.

1.6. Существующие способы построения распределённых систем на основе высокоуровневых протоколов и обоснование разработки альтернативных подходов.

1.7. Выводы к Главе 1.

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

2.1. Общий подход к разработке протоколов.

2.2. Свойства корректности протоколов.

2.3. Формальные методы построения моделей для оценки свойств корректности разрабатываемых протоколов.

2.4. Моделирования протоколов на основе аппарата сетей Петри.

2.5. Формирование математической базы методики разработки и тестирования ворректных высокоуровневых протоколов.

2.6. Выводы к Главе 2.

3. Разработка методики проектирования высокоуровневых протоколов информационного взаимодействия на основе ХМРР.

3.1. Определение макрофункцнй и примитивов протокола ХМРР.

3.2. Компонентная база проектирования.

3.3. Представление примитивов протокола ХМРР в виде функциональных подсетей Петри.

3.3. Формальное описание высокоуровневых протоколов на основе ХМРР с помощью агрегирования функциональных подсетей примитивов протокола ХМРР.

3.4. Проверка корректности протоколов, полученных в результате агрегирования.

3.5. Выводы к Главе 3.

Глава 4. Пример разработки системного протокола смены логических каналов с сохранением сеанса на основе ХМРР.

4.1. Обоснование необходимости в разработке протокола смены логических каналов безопасного информационного взаимодействия с сохранением сеанса.

4.2. Определение примитивов системного протокола высокого уровня смены логических каналов с сохранением сеанса.

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

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

4.5. Доказательство корректности работы протокола смены логических каналов с сохранением сеанса на основе полученной модели.

4.6. Архитектура системы безопасного взаимодействия в реальном времени с использованием протокола ХМРР на базе Microsoft .NET Remoting и проекта Mono.

4.7. Виды сообщений протокола смены логических каналов с сохранением сеанса.

4.3. Выводы к Главе 4.

Актуальность темы.

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

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

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

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

Целью работы является разработка новых методик проектирования и тестирования высокоуровневых протоколов, более эффективных по сравнению с существующими методиками.

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

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

Практическая значимость исследования. В ходе работы разработаны модели макрофункций и примитивов компонентной базы проектирования в виде ХМЬ-документов на языке Р1ММЬ, что позволяет использовать модели на различных платформах и не зависеть от инструментария моделирования сетей Петри.

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

Разработанный высокоуровневый протокол реализован в виде набора программных модулей и тестового приложения на основе языка С# и технологии Microsoft .NET Remoting. Архитектура программных модулей позволяет легко добавлять новые логические каналы.

Положения, выносимые на защиту.

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

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

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

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

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

Достоверность полученных результатов обоснована использованием аппарата сетей Петри, конечных автоматов и теории систем и системного анализа.

Структура диссертационной работы.

В разделе 1 проведён анализ существующих методов организации взаимодействия открытых телекоммуникационных систем на основе высокоуровневых протоколов. Выявлены недостатки этих методов, сформулирована задача создания новых методик проектирования и тестирования высокоуровневых протоколов, обоснована необходимость декомпозиции протокола ХМРР на макрофункции и примитивы.

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

В разделе 3 произведена декомпозиция протокола ХМРР на макрофункции и примитивы. Осуществлено отображение макрофункций и примитивов на эквивалентные подсети Петри. Разработаны правила агрегирования примитивов и макрофункций ХМРР в целевой корректный высокоуровневый протокол. Разработана методика тестирования высокоуровневого протокола на основе Р- и Т-инвариантов.

В разделе 4 разработан и протестирован протокол управления сменой логических каналов на основе предложенной методики.

1. Постановка задачи.

4.3. Выводы к Главе 4.

1. Определены цели, задачи и области применения системного протокола высокого уровня с сохранением сеанса;

2. Определены основные (глобальные) состояния и условия переходов между ними для протокольных машин системного высокоуровневого протокола смены логических каналов с сохранением сеанса;

3. Определены типы сообщений системного высокоуровневого протокола смены логических каналов с сохранением сеанса;

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

5. Доказана корректность системного высокоуровневого протокола смены логических каналов с сохранением сеанса;

6. Разработана спецификация протокола смены логических каналов с сохранением сеанса.

Заключение.

В диссертации получены следующие результаты:

1. Разработана компонентная база проектирования высокоуровневых протоколов высокого уровня, позволяющая эффективно использовать готовые модули.

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

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

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

3. Предложен метод проектирования корректных системных протоколов высокого уровня, имеющего высокую эффективность по сравнению с существующими.

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

122 эквивалентных подсетей Петри для макрофункций и примитивов существенно ниже, чем время инвариантов всей модели протокола.

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

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

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

Изменения среды окружения могут быть обусловлены рядом причин. В частности, при изменении контекста безопасности, когда с менее безопасного протокола, например, TCP необходимо перейти на более безопасный HTTPS. Также решается актуальная задача роуминга в условиях разнородности среды. Например, пользователь мобильного устройства переходит из зоны обслуживания WiFi в зону WiMAX.

1. Компьютерные сети. 4-е изд. / Э. Таненбаум. — СПб.: Питер, 2003. 992 е., ил.

2. Распределённые системы. Принципы и парадигмы / Э. Таненбаум, М. ван Стен. СПб.: Питер, 2003. - 877 е., ил.

3. Гарольд Э., Мине С. XML. Справочник. / Пер. с англ. СПб.: Символ-Плюс, 2002. - 576 е., ил.

4. List of XML markup languages электронный ресурс. / Wikipedia, the free encyclopedia. — Режим доступа:http://en.wikipedia.org/wiki/ListofXMLmarkuplanguages, свободный. — Загл. с экрана. — Яз. англ.

5. ХМРР Standards Foundation электронный ресурс. Режим доступа: http://xmpp.org/, свободный. — Загл. с экрана. — Яз. англ.

6. Фундаментальные основы хакерства. Искусство дизассемблирования / К. Касперски M : COJIOH-Пресс, 2005. — 448с., ил.

7. Чирилло Дж., Обнаружение хакерских атак. Для профессионалов. /Пер. с англ. СПб.: Питер, 2003. - 864 е.: ил.

8. Протоколы информационно-вычислительных сетей: Справочник / С. Аничкин, С. Белов и др. — М.: Радио и связь, 1990. 504 е.: ил.

9. Мещеряков C.B., Иванов В.М. Эффективные технологии создания информационных систем. М.: Политехника, 2005. — 312 е.: ил.

10. Шапошников И. В. Справочник Web-мастера. XML. СПб.:БХВ-Петербург, 2001. - 304 е.: ил.

11. Рэй Э. Изучаем XML / Пер. с англ. СПб.: Символ-Плюс, 2001. -408 е., ил.

12. ISO 7498. Information Processing Systems Open Systems Interconnection - Basic Reference Model. — 1983.

13. ISO/DP 8807. Information Processing Systems — Open System Interconnection — ESTELLE A Formal Description Technique Based on an Extended State Transition Model. - 1985.

14. Functional specification and description language SDL. In: CCITT Yellow Book, Vol. VI recommendations Z. 101 -Z. 104, CCITT, Geneva, 1981.

15. Josang A. Security Protocol Verification using Spin / Proc. SPIN Workshop, 1995.

16. Sajkowski M. Protocol Verification Techniques // Proc. IV Int. Workshop on Protocol Specification, Testing and Verification -Amsterdam: North-Holland Publishing Co., 1985 P. 697 - 720.

17. C. Lin, D.C. Marinescu. Translation of Modified Predicate Transition Nets Models of Communication Protocols into Simulation Programs, Proceeding of the 1986 Winter Simulation Programs, Dec. 1986, USA, PP. 760 768.

18. Feiertag R.J., Shostak R.E., Lamport L.B. Verification of Communication-Oriented Language Problems // SRI International — 1978.-P. 749-756.

19. Functional specification and description language SDL. In: CCITT Yellow Book, Vol. VI recommendations Z. 101 -Z. 104, CCITT, Geneva, 1981.

20. Лекции по теории сложных систем. / Бусленко Н.П., Калашников

21. B.В. М.: Советское радио, 1973. - 440 е.: ил.

22. Протоколы информационно-вычислительных сетей: Справочник/

23. C. Аничкин, С. Белов и др. М.: Радио и связь, 1990. - 504 е.: ил.

24. Буч Г., Рамбо Дж., Джекобсон A. UML. Руководство пользователя. М.: «ДМК», 2001.

25. Лешек А. Анализ и проектирование информационных систем с ' помощью UML 2.0. М.: Вильяме, 2008. - 816 е.: ил.

26. Weilkiens Т. Systems Engineering with SysMLUML Modeling, Analysis, Design. // Denise E. M. Penrose, 2007. 320 pp.

27. Беккер П., Йенсен Ф. Проектирование надежных электронных схем. / Пер. с англ. М.: «Сов. радио», 1977.

28. Теория автоматов / Ю. Карпов — СПб.: Питер, 2003. 208 е.: ил.

29. Model Checking. Верификация параллельных и распределённых программных систем. / Ю. Карпов. — СПб.: БХВ-Петербург, 2010. — 560с.: ил.

30. G. Bochman. Finite state description of communication protocols / Comput. Networks, v.2, 1978, pp. 361-371

31. Рейуорд-Смит В.Дж. Теория формальных языков. Вводный курс. -М.: Мир, 1988.

32. Основы теории графов./ Зыков А.А. — М.: Наука, гл. ред. физ.-мат. лит., 1987.-384 с.

33. Минский М. Вычисления и автоматы. — М.: Мир, 1978.

34. Гэри М., Джонсон Д. Вычислительные машины и труднорешаемые задачи. М: Мир, 1982.

35. Лескин А.А., Мальцев П.А., Спиридонов A.M. Сети Петри в моделировании и управлении. М.: Наука, 1989.

36. Питерсон Дж. Теория сетей Петри и моделирование систем. М.: Мир, 1984.-264 с: ил.

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

38. Berthlot G., Terrat R., Petri Nets Theory for the Correctness of Protocols // IEEE Trans. 1982. - Vol. COM-30, N 12. - P 2497 -2505.

39. G. Galbo, S. Bruell, and S. Ghanta. Combining queuing Networks and generalized stochastic Petri nets for the solution of complex models ofsystem behavior. IEEE Transactions on Computers, 37(10): 1251 — 1268, 1988.

40. Toudic J.M. Linear Algebra Algorithms for Structural Analisys of Petri Nets//Rev. Tech. Thomson CSF, 1982.-No. l.-Vol. 14.-p. 136156.

41. Diaz M. Modelling and Analysis of Communication and Cooperation Protocols Using Petri Net Based Model // Computer Networks, no 6, 1982,419-441.

42. Zaitsev D.A. On question of calculation complexity of Toudic's method // Artificial Intelligence, no. 1, 2004, 29-37. In Russ.

43. Murata T. Petri Nets: Properties, Analysis and Applications // Proceedings of the IEEE, April 1989. Vol. 77. - p. 541-580.

44. Zaitsev D.A. Decomposition of protocol ECMA // Raditekhnika: All-Ukr. Sci. Interdep. Mag. 2004, Vol. 138, 130-137. In Russ.

45. Методология программирования. / Турский В. M.: Мир, 1981. -263 е.: ил.

46. Корнилов A.M., Мазепа Р.Б., Михайлов В.Ю. Проблемы безопасного информационного взаимодействия в распределенной среде. М.: МАИ-ПРИНТ, 2009. - 260 е.: ил.

47. Олифер В.Г., Олифер Н.А. Сетевые операционные системы. — СПб.: Питер, 2001. 672 е.: ил.

48. Гамма Э., Хелм Р., Джонсон Р., Влиссидес Дж. Приемы объектно-ориентированного проектирования. Паттерны проектирования. — СПб.: Питер, 2007. 366 е.: ил.

49. Рихтер Дж. Программирование на платформе Microsoft .NET Framework /Пер. с англ. — 2-е изд., испр. — М.: Издательско-торговый дом «Русская Редакция», 2003. — 512 стр.: ил.

50. Маклин С., Нафтел Дж., Уильяме К. Microsoft .NET Remoting /Пер. с англ. — М.: Издательско-торговый дом «Русская Редакция», 2003. 384 е.: ил. - ISBN 5-7502-0229-1

51. Орлов JI. Разработка интерактивных Web-сайтов. — М.: Бук-пресс, 2006.-512 с.

52. Троелсен Э. С# и платформа .NET. Библиотека программиста. — СПб.: Питер, 2007. 796 е.: ил.

53. Шапошников И. Web-сервисы Microsoft .NET. — СПбю: БХВ-Петербург, 2002. 334 е.: ил.

54. Web-протоколы. Теория и практика. / Б. Кришнамурти. М.: ЗАО «Издательство БИНОМ», 2002. - 592 е.: ил.