Введение
1 Исследование свойств достижимости 21
1.1 Формальные методы в ПКС 21
1.2 Основные положения протокола OpenFlow
1.2.1 Коммутатор 23
1.2.2 Пакеты 24
1.2.3 Конвейер коммутации пакетов 24
1.2.4 Правило коммутации 25
1.2.5 Таблица коммутации пакетов 27
1.2.6 Контроллер 28
1.3 Требования к поведению ПКС 29
1.3.1 Классификация свойств поведения ПКС 30
1.3.2 Элементарные объекты ПКС 31
1.3.3 Локальные свойства пакетов и точек 33
1.3.4 Локальные свойства элементов коммутационного конвейера 35
1.3.5 Глобальные свойства 39
1.3.6 Статические свойства ПКС 40
1.3.7 Динамические свойства ПКС 41
1.3.8 Свойства реального времени 44
1.4 Выбор языка спецификаций поведения ПКС 45
1.4.1 Требования к языка спецификации 45
1.4.2 Темпоральные логики 46
1.4.3 Пропозициональное /х-исчисление 48
1.4.4 Логика транзитивного замыкания 48
1.4.5 Выводы 49
1.5 Выбор формальных моделей ПКС 50
1.5.1 Требования к формальным моделям ПКС 50
1.5.2 Выбор моделей для компонентов ПКС 53
1.5.3 Двоичные решающие диаграммы 55
1.5.4 Выводы 57
1.6 Формальная модель ПКС 57
1.6.1 Статическая модель ПКС 59
1.6.2 Динамическая модель ПКС 63
1.7 Язык спецификации политик маршрутизации 65
1.7.1 Со- язык описания состояний пакетов 66
1.7.2 С\. язык спецификации статических свойств 66
1.7.3 С,2- язык спецификации динамических свойств 68
1.8 Программная реализация верификатора ПКС 69
1.8.1 Построение модели ПКС по её конфигурации 70
1.8.2 Анализ спецификаций 75
1.8.3 Верификация конфигурации ПКС 80
1.9 Экспериментальное исследование 80
1.9.1 Генерация конфигураций ПКС 80
1.9.2 Эксперименты на синтетических конфигурациях 82
1.9.3 Эксперименты на реальных данных 85
1.10 Выводы 88
2 Оценка задержки передачи пакетов 90
2.1 Качество сервиса и методы его обеспечения 91
2.1.1 Требования качества сервиса 93
2.1.2 Метрики качества сервиса 95
2.1.3 Связь между обеспечением качества и управлением ресурсами 95
2.1.4 Методы обеспечения качества 96
2.1.5 Выводы 100
2.2 Организация обработки пакетов на коммутаторе 101
2.2.1 Компоненты коммутатора 101
2.2.2 Анализатор пакетов 102
2.2.3 Буферный блок 104
2.2.4 Коммутационная матрица 107
2.2.5 Методы буферизации 108
2.3 Оценка задержки с помощью сетевого исчисления 111
2.3.1 Основы теории сетевого исчисления 112
2.3.2 Отставание и задержка передачи данных 114
2.3.3 Описание обработчиков с помощью кривых сервиса 115
2.3.4 Описание потоков с помощью кривых нагрузки 118
2.3.5 Основные понятия Min-Plus алгебры 120
2.3.6 Регуляторы 121
2.3.7 RL-обработчики 124
2.3.8 Эффективная композиция обработчиков: принцип РВОО 125
2.3.9 Моделирование ПКС 127
2.4 Мультиплексирование нескольких потоков 128
2.4.1 Индивидуальное и агрегированное планирование 130
2.4.2 Стабильность при агрегированном планировании 131
2.4.3 Анализ Суммарного Потока (Total Flow Analysis) 133
2.4.4 Анализ Отдельного Потока (Separated Flow Analysis) 134
2.4.5 Анализ пересечения потоков (РМОО) 136
2.5 Обобщение алгоритмов вычисления задержки 137
2.5.1 Схемы вычисления функции свёртки 138
2.5.2 Схема вычисления функции обратной свёртки 140
2.6 Оценка задержки с помощью линейного программирования 143
2.6.1 Модель сети 143
2.6.2 Упорядочивание значений функции поступления 145
2.6.3 Стабилизация узлов ограничительной сетки 148
2.6.4 Задание целевой функции 149
2.7 Реализация и экспериментальное исследование 151
2.7.1 Модуль оценки задержки 151
2.7.2 Имитационная модель сети 152
2.7.3 Модели потоков данных 154
2.7.4 Тестовые сценарии 159
2.7.5 Результаты экспериментов 161
Заключение 165
Список рисунков 185
Список таблиц 187
Литература
