Анализ, моделирование и верификация высокоуровневых протоколов эффективного информационного взаимодействия открытых телекоммуникационных систем тема диссертации и автореферата по ВАК РФ 05.12.13, кандидат технических наук Корнилов, Александр Михайлович

• Корнилов, Александр Михайлович
• кандидат технических наук
• 2010

Оглавление диссертации кандидат технических наук Корнилов, Александр Михайлович

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

Введение.

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.

Список литературы диссертационного исследования кандидат технических наук Корнилов, Александр Михайлович, 2010 год

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 е.: ил.