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

• Автор: Корнилов, Александр Михайлович
• Шифр специальности: 05.12.13
• Научная степень: Кандидатская
• Год защиты: 2010
• Место защиты: Москва
• Количество страниц: 175 с. : ил.

Оглавление

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

Введение

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

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

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

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

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

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

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

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

2. Обоснование и выбор математического аппарата для описания и анализа свойств системных протоколов высокого уровня
2.1. Общий подход к разработке протоколов
2.2. Свойства корректности протоколов
2.3. Формальные методы построения моделей для оценки свойств корректности разрабатываемых протоколов
2.4. Моделирования протоколов на основе аппарата сетей Петри
2.5. Формирование математической базы методики разработки и тестирования ворректных высокоуровневых протоколов
2.6. Выводы к Главе
3. Разработка методики проектирования высокоуровневых протоколов информационного взаимодействия на основе ХМРР
3.1. Определение макрофункцнй и примитивов протокола ХМРР
3.2. Компонентная база проектирования
3.3. Представление примитивов протокола ХМРР в виде функциональных подсетей Петри

3.3. Формальное описание высокоуровневых протоколов на основе ХМРР с помощью агрегирования функциональных подсетей примитивов протокола ХМРР
3.4. Проверка корректности протоколов, полученных в результате агрегирования
3.5. Выводы к Главе
Глава 4. Пример разработки системного протокола смены логических каналов с сохранением сеанса на основе ХМРР
4.1. Обоснование необходимости в разработке протокола смены логических каналов безопасного информационного взаимодействия с сохранением сеанса
4.2. Определение примитивов системного протокола высокого уровня смены логических каналов с сохранением сеанса
4.3. Представление примитивов системного протокола высокого уровня смены логических каналов с сохранением сеанса в виде корректных функциональных подсетей Петри
4.4. Модель протокола смены логических каналов с сохранением сеанса, полученная с помощью агрегирования функциональных подсетей Петри
4.5. Доказательство корректности работы протокола смены логических каналов с сохранением сеанса на основе полученной модели
4.6. Архитектура системы безопасного взаимодействия в реальном времени с использованием протокола ХМРР на базе Microsoft .NET Remoting и проекта Mono
4.7. Виды сообщений протокола смены логических каналов с сохранением сеанса.

4.3. Выводы к Главе
Заключение
Список используемой литературы
Приложение
Приложение
Приложение

Список терминов и условных сокращений
ASP.Net (Active Server Pages dot Net) - технология построения вебприложений, предлагаемая Microsoft;
Base64 - позиционная система счисления с основанием 64;
EFSM (Extended Finite State Machine) - расширенный конечный автомат;
FSM (Finite State Machine) — конечный автомат;
HTTP (Hypertext Transport Protocol) - протокол передачи гипертекста;
GPS (Global Positioning System) — глобальная система спутникового позиционирования;
IMAP (Internet Message Access Protocol) - протокол дос тупа к электронной почте Интернета;
Java — объектно-ориентированный язык программирования, разрабатываемый компанией Sun Microsystems;
IM (Instant Messaging) - обмен сообщениями в реальном времени;
MSMQ (Microsoft Message Queuing) — технология очередей сообщений;
MG (Marked Grapgh) - маркированный граф;
.Net - программная технология, предназначенная для создания как обычных программ, так и веб-приложений, предложенная компанией Microsoft;
PHP (Hypertext Preprocessor) - процессор гипертекста (интерпретатор программ, написанных на одноименном языке);
PKI (Public Key Infrastructure) - Инфраструктура открытых ключей;
PN (Petri Nets) - сети Петри;
PNML (Petri Nets Markup Language) - язык разметки сетей Петри;
POP3 (Post Office Protocol Version 3) - протокол почтового отделения, версия 3;
RFC (Request for Comments) - запрос комментариев (общепринятый вид представления электронных спецификаций);
RPC (RPC - Remote Procedure Call) - вызов удаленных процедур;

2.1.2. Язык описания спецификаций ESTELLE.
Язык ESTELLE (Extended State Transition Language) описывает архитектуру системы множеством модулей и структурой их взаимосвязей, которая задаётся двунаправленными каналами [13]. Спецификация канала включает:
- перечисление возможных примитивов взаимодействия, допускаемых каналом данного типа;
- имена ролей, которые играет каждая из сторон канала, например «поставщик» или «пользователь» сервиса;
- перечисления типов параметров каждого используемого примитива.
Спецификация модуля включает:
- перечисление всех точек взаимодействия с указанием для каждой из них типа канала;
- описание действий модуля в виде переходов расширенного конечного автомата.
Для описания конечного автомата протокола используется язык программирования Pascal. Пример фрагмента спецификации на ESTELLE: trans
when XMPPAuthResponseOK resp from WaitingAuthResult to AuthOK
begin
XMPPSendPresence(" Online ”)
CloseStreamQ

При поступлении положительного ответа сервера на ранее посланные клиентом данные аутентификации XMPPAuthResponseOK, протокольная машина клиента переходит из состояния WaitingAuthResult в состояние AuthOK. Затем вызывается функция отправки сообщения о состоянии клиента и сеанс завершается вызовом функции CloseStreamQ.