Содержание к диссертации
Введение
1 Коммуникационные транспортные протоколы 8
1.1 Современные коммуникационные сети 8
1.2 Модель взаимодействия открытых систем 9
1.3 Семейство протоколов TCP/IP 11
1.4 Transmission Control Protocol (TCP) 13
1.5 Протокол ARTCP 36
1.6 Модели коммуникационных протоколов и сетевого трафика 38
2 Моделирование транспортных протоколов с помощью раскрашенных сетей Петри 40
2.1 Раскрашенные сети Петри 40
2.2 Моделирование служебных структур протокола 56
2.3 Иерархическая структура модели 62
2.4 Построение модели функциональной части протокола 65
2.5 Моделирование обработки пользовательских вызовов 66
2.6 Моделирование передачи сегментов в сеть 71
2.7 Моделирование обработки пришедших сегментов 78
2.8 Модификация модели 85
2.9 Общая схема модельных экспериментов 91
2.10 Заключение 92
3 Анализ свойств коммуникационных транспортных протоколов 94
3.1 Проблема верификации транспортных протоколов 94
3.2 Верификация предоставляемого протоколом сервиса 95
3.3 Верификация иерархических раскрашенных сетей Петри 114
3.4 Верификация моделей протоколов 115
3.5 Анализ работы протокола ARTCP при множественных потерях сегментов 120
3.6 Исследование производительности транспортных протоколов 124
3.7 Заключение 138
Заключение 140
Литература 141
- Модели коммуникационных протоколов и сетевого трафика
- Моделирование служебных структур протокола
- Моделирование обработки пришедших сегментов
- Анализ работы протокола ARTCP при множественных потерях сегментов
Введение к работе
Предмет исследования
Одним из важнейших достижений научно-технического прогресса в настоящее время являются коммуникационные системы, представляющие собой сети передачи информации. Успешное внедрение Интернет- и интранет-технологий приводит к тому, что человечество становится все более зависимым от надежности функционирования вычислительных устройств.
Транспортные протоколы являются важным элементом коммуникационной архитектуры сети Интернет (согласно исследованиям [72], около 95% всех переданных байтов и 85-95% всех переданных пакетов). Основной задачей протокола транспортного уровня является предоставление сервиса программным процессам для надежного и эффективного обмена информацией через ненадежную среду передачи — коммуникационную сеть. С точки зрения транспортного протокола сеть представляется в виде «черного ящика , где информация может теряться, переупорядочиваться, искажаться и, возможно, дублироваться. Под эффективностью работы транспортного протокола понимается прежде всего эффективное использование сетевых ресурсов — таких как, например, пропускная способность каналов передачи и буферов маршрутизаторов.
Предметом нашего исследования является транспортный протокол TCP (Transmission Control Protocol), который является основным транспортным протоколом коммуникационной архитектуры сети Интернет. Так как этот протокол постоянно изменяется и дополняется, то можно говорить о семействе протоколов TCP.
Исследование свойств транспортных протоколов, в частности различных версий протокола TCP, является важной и актуальной задачей, которая рассматривалась в ряде работ. Основным объектом исследований являлись алгоритмы управления потоком транспортных протоколов, а основным методом исследований, который использовался в этих работах — имитационное моделирование. Яркими представителями таких работ являются: [66], где рассматривались различные версии алгоритма управления потоком протокола TCP; [67], где представляется новый протокол TCP Westwood, и на ряде примеров обосновывается его эффективность; [1], где представляется новый протокол ARTCP (Adaptive Rate TCP) и на ряде модельных экспериментов обосновывается его преимущество перед стандартным TCP.
Другим популярным методом исследования является построение аналитических моделей. Например, в работе [68] рассматривается модель алгоритма управления потоком и вопросы порождения протоколом TCP самоподобного трафика. Методы имитационного моделирования могут быть весьма экономичными для выявления многих ошибок, однако проверить все возможные взаимодействия и пути выполнения протокола вряд ли представляется возможным.
Одним из подходов к решению задачи корректности транспортных протоколов может быть построение формальных моделей и их последующий анализ с помощью формальных методов (например, методов model checking). Значительный интерес в этом направлении представляют работы И. А. Ломазовой (напр., [10]), посвященные формализму сетей Петри и методам анализа их свойств. Вопросы корректности коммуникационных протоколов рассматривались также, например, в [15, 11]. Основным подходом в работе [15] является построение моделей протоколов с помощью автоматов и их последующая верификация, а в работе [11] приводится метод построения моделей Estelle-спецификаций с помощью раскрашенных сетей Петри. Применение этих подходов затруднено тем, что стандартные документы, задающие спецификацию семейства транспортных протоколов TCP, изложены на неформальном языке. Был представлен ряд работ по построению моделей протокола TCP в терминах раскрашенных сетей Петри (например, [77, 78]). В работе [77] представляются результаты моделирования процесса обмена данными ряда версий протокола TCP, а в работе [78] рассматривается модель процессов установки и завершения соединений. Как видно, эти работы рассматривают некоторые фрагменты оригинального протокола; перед нами же стояла задача промоделировать стандарт протокола целиком. Другой особенностью этих работ является то, что основной акцент они делают именно на построении моделей, а не на разработке методов их исследования. В нашей работе кроме задачи построения моделей, рассматриваются вопросы анализа различных свойств протоколов, таких как производительность и корректность. Очевидно, что корректность, как характеристика, имеет несомненный приоритет над производительностью.
Научная новизна работы
Основные научные результаты работы состоят в следующем:
• В терминах раскрашенных сетей Петри разработана модель последнего варианта официального стандарта спецификации протокола TCP;
• Предложены методы модификации этой модели для представления новых версий про
токола TCP;
• На основе построенной модели протокола TCP предложена модель протокола ARTCP (Adaptive Rate TCP);
• Предложены алгоритмы восстановления от множественных потерь сегментов для протокола ARTCP;
• Формально верифицированы процессы открытия и закрытия транспортного соединения;
• На ряде сценариев проведена сравнительная оценка производительности последней версии протокола TCP и предложенных модификаций протокола ARTCP.
Практическая ценность результатов
Предложенная модель была реализована в системе моделирования Design/CPN, что позволяет ее использовать для автоматизированного моделирования и анализа свойств протоколов TCP и ARTCP. Предложенные методы модификации позволяют строить формальные модели новых версий этих протоколов и проводить их анализ с помощью автоматических средств. При этом показано, как можно проводить не только анализ производительности протоколов, но верификацию.
Апробация работы
По результатам, полученным в ходе работы, были сделаны доклады на следующих конференциях:
1. Международная конференция «Parallel Computer Technologies» (Нижний Новгород, 2003 год);
2. Всероссийская научная конференция «Методы и средства обработки информации» (Москва, 2003 год);
3. Международной конференции по вычислительной математике (Новосибирск, 2004 год);
4. Междисциплинарной конференции НБАТТ-21 (Петрозаводск, 2004 год);
Результаты также обсуждались на семинаре «Моделирование и анализ информационных систем» ЯрГУ.
Содержание работы
В главе 1 демонстрируется положение транспортного протокола TCP в коммуникационной архитектуре TCP/IP и подробно рассматриваются все его компоненты, принципы работы и алгоритмы. Один из основных результатов работы — модель транспортных протоколов, представляется в главе 2. В начале главы рассматривается формализм раскрашенных сетей Петри и приводятся основные методы анализа моделей, построенных в терминах этого формализма. Глава продолжается описанием модели транспортных протоколов семейства TCP. Там же рассматриваются методы модификации этой модели и возможные варианты использования в модельных экспериментах. Вопросы анализа свойств протоколов рассматриваются в главе 3. В начале главы рассматриваются вопросы верификации транспортных протоколов. Для этого рассматривается набор темпоральных формул, с помощью которых верифицируется процесс обработки пользовательских вызовов транспортным протоколом. Там же приводятся результаты экспериментов по верификации процессов открытия и закрытия транспортного соединения. Далее приводятся результаты анализа поведения протокола ARTCP в условиях множественных потерь сегментов и рассматриваются алгоритмы, которые направлены на увеличение производительности протокола при этих условиях. В конце главы приводятся экспериментальные данные по сравнительному анализу новых версий протоколов TCP и предложенного усовершенствования алгоритма протокола ARTCP. Работа завершается выводами.
Модели коммуникационных протоколов и сетевого трафика
Важность сетей передачи данных и мультимедиа невозможно переоценить сегодня, в начале информационной эпохи развития человечества. Современное определение сети передачи данных такое: сеть —это набор автономных вычислительных устройств, физически и логически связанных между собой. Иными словами, набор равноправных узлов, имеющих возможность обмениваться информацией. Такое определение относится к, так называемой, сети передачи данных, однако, не ограничивается только компьютерными данными и может быть расширено для любой сети, построенной по принципу коммутации пакетов. В том числе и для универсальной сети с интеграцией сервисов. Любая коммуникационная система состоит из двух основных компонентов: аппаратной и логической частей.
Аппаратная часть —это физическая инфраструктура, посредством которой осуществляется распространение физических сигналов, кодирующих информационные сообщения. Физическая инфраструктура может либо осуществлять информационный обмен между всеми участниками сети одновременно (широковещательная сеть), либо между двумя узлами (сеть типа «точка-точка ). В зависимости от масштаба и топологии сетевой инфраструктуры производят ее дальнейшую классификацию: локальные вычислительные сети (LAN — Local Area Network), территориальные сети (WAN — Wide Area Network), сотовые сети и т.д.
Логическую часть сети составляют коммуникационные протоколы. Многие свойства протоколов для коммуникационной системы находятся в прямой зависимости от ее физической среды и топологии. Поэтому параметры физической инфраструктуры сети тщательно учитываются при разработке протоколов для нее.
В качестве неформального определения протокола можно привести следующее: протокол представляет собой соглашение по процедуре обмена информацией в распределенной системе. Задачей любого протокола является управление совместным использованием ресурсов. Разработка, описание и верификация протоколов составляют наиболее сложную задачу в решении проблемы создания коммуникационных систем. 1.2. Модель взаимодействия открытых систем
Одним из методов, помогающим при проектировании или исследовании сложной системы, является разбиение системы на части меньшей сложности, которые можно изучать или разрабатывать по отдельности. Упорядочивая эти части в соответствии с принципами их взаимодействия, можно получить иерархическую структуру всей системы. Системы протоколов в современных коммуникационных сетях имеют иерархическую структуру и образуют коммуникационную архитектуру. Каждый протокол в такой системе представляет собой определенный уровень абстракции. Основыми приемуществами подобной организации являются: Поуровневое проектирование помогает указать логическую структуру системы с помощью разделения задач, выполняемых на высоких уровнях, от низкоуровневых деталей; Когда систему нужно расширить или модифицировать, гораздо легче изменить или заменить отдельный модуль, чем переделать ее заново. Преимуществами проектирования и построения независимых уровней можно воспользоваться лишь в том случае когда границы между уровнями четко определены. Главной задачей каждого уровня является предоставление определенных сервисов вышележащему уровню. С одной стороны, уровень N для выполнения своей задачи использует сервис, предоставляемый уровнем N—1, с другой стороны, уровень N может предоставлять сервис уровню N + 1. Взаимодействие между пользователем сервиса и поставщиком услуг описываются с помощью примитивов сервиса. К 1980 году Международная Организация Стандартизации (ISO) в целях унификации методов разработки протоколов была предложена так называемая эталонная модель взаимодействия открытых систем (OSI Reference Model). Рекомендация ISO определяет иерархическую систему из семи уровней, показанных на рисунке 1.1 и имеющих следующие функции. Физический уровень содержит аппаратное обеспечение, а иногда и некоторые программные драйверы — компоненты, которые работают с предачей и приемом битов или групп битов, таких как байты. Этот уровень также осуществляет межуровневые преобразования. В этой области физический уровень может конвертировать цифровые битовые потоки, передаваемые в электронном виде, в аналоговые сигналы (как в модеме, беспроводной или спутниковой связи) или в сигналы, представленные в световом виде (в оптоволоконных или инфракрасных системах передачи). Зачастую физический уровень реализуется непосредственно на чипах.
Канальный уровень является первым из шести уровней программного обеспечения в стеке OSI. Он реализует механизм отправки сообщений по физическому соединению соседнему устройству и захвата сообщений, которые поступают по тому же самому физическому соединению от соседнего устройства. В модели OSI канальный уровень должен гарантировать корректную передачу данных. Кроме того, канал соединения, который используется канальным уровнем, не обязан быть двусторонним: например, он может быть частью кольцевой системы.
Сетевой уровень выполняет маршрутизацию пакетов по множеству каналов в одной сети и через шлюзы — между двумя и большим числом сетей. Если в пакетах информации нужно произвести изменения, давая этим пакетам возможность «попутешествовать по сети, то такие изменения (например, изменение данных в заголовке или расщепление пакетов, чтобы они соответствовали пропускной способности маршрута передачи) производятся на этом уровне.
Транспортный уровень обеспечивает работу соединения вида «конечное устройство-конечное устройство» между двумя определенными устройствами в сети. Соединение может заключаться в потоке данных или, может быть, в форме единичного обмена сообщениями без установления логического соединения. Транспортный уровень является самым низким из уровней, на котором привлекаются только равноправные системы, находящиеся на компьютере-источнике сообщения и на компьютере-получателе сообщения, и не привлекаются ни одна из систем — промежуточных станций, используемых сетевым уровнем для передачи сообщений по сети. Протоколам на транспортном уровне приходится беспокоиться о качестве обслуживания, который они предоставляют более высоким уровням. Этот уровень, как правило, в наибольшей степени связан с коррекцией ошибок передачи.
Сеансовый уровень определяет формат данных, которые будут переданы по соединению транспортного уровня, а также задает способ обмена данными. Удачным примером протокола сеансового уровня может служить протокол Remote Procedure Call (RPC, протокол вызова удаленной процедуры). Этот протокол расширяет концепцию вызова функции или подпрограммы на случай среды многих машин, допуская при этом, что программа, находящаяся в одной системе, вызывает функцию или подпрограмму, находящуюся в другой системе. Протокол сеанса клиента (модуль вызова) осуществляет вызов удаленной процедуры и передает параметры. Протокол сеанса сервера (отвечающий модуль) выполняет удаленную процедуру и возвращает ответ на вызов.
Уровень представления предназначен для решения вопроса шифрования. Этот уровень осуществляет кодирование данных, обеспечивая совместимость для различных форматов представления информации.
Уровень приложений отличается от остальных тем, что его объектами являются непосредственно приложения, исполняемые на вычислительном узле. Функция этого уровня заключается в определении клиентов, которым необходимо взаимодействие, синхронизации взаимодействия и определения наличия ресурсов для проведения сеанса коммуникации.
Моделирование служебных структур протокола
Этот протокол использует временные характеристики потока, такие, как время возврата и значение оценки пропускной способности сети, в качестве аргументов. Как показано в [1], алгоритм ARTCP имеет следующие приемущества по сравнению со стандартным алгоритмом управления потоком: алгоритм ARTCP не создает состояния перегрузки сети для определения свободной пропускной способности. Поэтому в стабильном состоянии потоки, управляемые алгоритмом ARTCP, не испытывают потерь сегментов из-за наступления перегрузки. Таким образом, повышается эффективность использования сетевой инфраструктуры; алгоритм ARTCP не интерпретирует факт потери сегмента как следствие перегрузки сети. Таким образом, ARTCP может показать лучшую производительность, чем стандартный TCP, на каналах с высокой вероятностью искажения данных; алгоритм ARTCP использует минимальный объем буферного пространства маршрутизаторов (в среднем, один сегмент для каждого потока); алгоритм ARTCP допускает совместную с протоколом TCP реализацию. Подробное описание алгоритма работы протокола ARTCP можно найти в [1]. Основная задача алгоритма состоит в управлении скоростью передачи сегментов в сеть. Вычисление скорости передачи сегментов зависит, в частности, от оценки пропускной способности сети. В работе [1] предлагается производить эту оценку следующим образом. Получатель сегментов с данными производит измерение скорости прибывающих сегментов и передает это значение отправителю в сегментах с подтверждениями. В работе [1] обосновывается, что это значение, полученное отправителем, будет являться оценкой свободной пропускной способности сети. Для передачи значения оценки пропускной способности в сегмент вводятся новые дополнительные опции, с помощью которых этот процесс реализуется.
Адаптация скорости передачи потока протоколом ARTCP происходит в пяти режимах, показанных на рисунке 1.10. Режим ускоренного старта имеет цель максимально быстро увеличить скорость потока от минимального значения до значения, равного или превосходящего пропускную способность сети после инициализации соединения.
После того как установленная скорость превосходит пропускную способность сети, алгоритм использует мультипликативный сброс для установления скорости значением, гарантированно меньшим, чем пропускная способность сети. Так как некоторое время протокол ARTCP отправлял сегменты со скоростью, большей чем пропускная способность сети, в это время происходила перегрузка сети, сегменты могли накапливаться в буферах маршрутизаторов или теряться. Алгоритм ARTCP уменьшает скорость передачи сегментов затем, чтобы снизить потребление ресурсов сети и постараться вывести сеть из состояния перегрузки.
После мультипликативного сброса протокол начинает работу в режиме восстановления. Этот режим используется для постепенного увеличения скорости передачи до уже известной, не допуская перегрузки сети. Далее следует режим тонкой настройки. В этом режиме скорость передачи сегментов медленно изменяется таким образом, чтобы реагировать на малейшие изменения нагрузки сети. В случае каких-то аномальных ситуаций, которые вызывают резкое понижение пропускной способности сети, производится мультипликативный сброс. Завершение работы алгоритма может произойти в любом из следующих трех состояний: ускоренный старт, режим восстановления и режим тонкой настройки. Основным методом исследования сетевых транспортных протоколов можно назвать моделирование. При этом основное внимание уделяется проблеме исследования различных аспектов производительности. Так, Кумар в своей работе [79] использовал стохастическую модель для прогнозирования производительности различных версий протокола TCP с учетом потерь в ненадежном беспроводном канале связи. Фолл и Флойд в [66] представляли достоинства работы алгоритма выборочных подтверждений на основе выводов из имитационных экспериментов в системе Ns-2 [74]. Ост и Хаверкорт в [80] на основе исследования модели в терминах стохастических сетей Петри оценивали производительность оконного алгоритма при работе веб-приложений. В работе [77] центральное место занимает демонстрация возможностей использования раскрашенных сетей Петри для исследования алгоритма управления потоком некоторых версий протокола TCP. Позднее, раскрашенные сети Петри использовались в работе [78] для моделирования процессов открытия и закрытия соединений. Однако, в последних двух работах не рассматривались вопросы верификации транспортных протоколов. Другим перспективным направлением исследования является моделирование трафика, который передается через коммуникационную сеть. Здесь необходимо отметить работы [70, 71], в которых показано, что сетевой трафик обладает фундаментальным свойством самоподобия и приведены методы построения синтетических трасс трафика. В нашей работе мы используем эти результаты при исследовании производительности транспортных протоколов.
Моделирование обработки пришедших сегментов
Если задана начальная разметка сети, то путем срабатывания всех означивающих элементов можно найти все достижимые состояния сети. Построение графов достижимости не является чем-то новым —идея построения и анализа множеств достижимых состояний для систем с переходами является классическим методом исследования.
После построения графа достижимости возможно с помощью разработанного математического аппарата проводить анализ свойств следующих свойств (формальное определение этих свойств можно найти в [84, 87]): достижимость. Свойство достижимости позволяет определить, существует ли от некоторого заданного состояния сети (например, начальной разметки) последовательность срабатываний означивающих элементов, ведущая к некоторому другому заданному состоянию; тупиковые состояния. Если в некотором состоянии сеть не имеет активных означивающих элементов, то такое состояние называют тупиковым. Нежелательные тупиковые состояния называют дедлоками. Корректные тупиковые состояния называют терминальными. Таким образом корректная система в процессе работы должна достигать только терминальных тупиковых состояний, и не достигать дедлоков; бесконечные циклы. Бесконечный цикл представляет собой цилический фрагмент графа достижимых состояний. Для раскрашенной сети Петри, граф достижимости которой содержит бесконечный цикл, можно построить бесконечную последовательность срабатываний. Очевидно, что реальные системы должны заканчивать свою работу за конечное число шагов и бесконечный цикл это нежелательное свойство моделей этих систем; ограниченность. В любом состоянии сети каждая позиция имеет некоторую разметку. Свойство ограниченности помогает узнать, каким значением ограничена4 разметка данной позиции.
Если мы имеем построенный граф достижимости, то с помощью него можно вычислить граф сильно связных компонент (Strongly Connected Components Graph, SCC-граф). Компонентами SCC-графа являются такие максимальные по размеру подмножества вершин
Здесь понимается не только то, какое максимальное количество маркеров может содержать позиция, но и какое максимальное значение мультимножества маркеров может находиться в позиции графа достижимых состояний, что каждая вершина достижима от любой другой из этого же подмножества. Построение SCC-графа полезно для проверки модели на наличие бесконечных циклов. Так, если SCC-граф и граф достижимости изоморфны и граф достижимости не содержит дуг, которые начинаются и заканчиваются в одном состоянии, то тогда граф достижимости не содержит бесконечных циклов. Построение SCC-графов также используется при исследовании моделей с помощью темпоральной логики (см. раздел 2.1.6).
Раскрашенная сеть Петри, которая моделирует работу туннеля Клейтона, имеет граф достижимости5, состоящий из 72 вершин и 184 дуг. Граф сильно связных компонент имеет 72 вершины и 112 дуг. Граф достижимости не содержит терминальных разметок. Действительно, в нашей системе переход ExchangeMsg может срабатывать бесконечное число раз. Было проверено, что от начального состояния достижимо состояние, которое моделирует что все поезда успешно миновали туннель.
Анализ свойств графов достижимости может много сказать нам о моделируемой системе, однако этот метод имеет два практических ограничения, особенно при исследовании сложных систем: 1. множество достижимых состояний может быть очень большим, чтобы его можно было хранить в памяти компьютеров (эта проблема также известна под названием «взрыв числа состояний»); 2. множество достижимых состояний зависит от начальных параметров модели (задаваемых, например, начальной разметкой сети). Существуют два метода преодоления первого препятствия: редукция множества достижимых состояний и создание более эффективных алгоритмов построения и хранения графов достижимости. В частности, при исследовании транспортных протоколов может быть полезен Sweep-Line метод, представленный в [89]. Использование темпоральной логики Темпоральные логики, такие как CTL [82, 9], являются мощным инструментом для исследования свойств параллельных и распределенных систем. Задачу проверки модели с помощью темпоральных логик можно сформулировать следующим образом. Пусть задана формальная модель, некоторое состояние модели и формула темпоральной логики у?. Необходимо выяснить, удовлетворяет ли это состояние модели формуле темпоральной логики 3десь и далее анализ представленной модели туннеля Клейтона проводился с помощью системы CPNTools. Как мы видели в предыдущем разделе, граф достижимых состояний хранит не только информацию о состоянии сети, но и об означивающих элементах. Соответственно, хорошо бы было иметь темпоральную логику, формулы которой могли задавать свойства не только на множестве позиций, но и на множестве означивающих элементов. Логика для раскрашенных сетей Петри, позволяющая это делать, предлагается в [88], и называется ASK-CTL.
Как и в CTL, формулы логики ASK-CTL интерпретируются на множестве путей графов достижимых состояний (причем пути могут состоять как из разметок, так и из означивающих элементов). Логика ASK-CTL имеет две категории формул: состояний и переходов. Эти две категории взаимно рекурсивны и определяются следующим образом: Формулы состояний: A ::= tt \ а - Л Лі V А21 {В) \ EU(Ai,A2) \ AU(A\, А2) где tt это константа, соответствующая значению «истина , а это формула элементарных высказываний, сопоставляющая каждой разметке булевское значение, а В это формула переходов, синтаксическое задание которой следующее: Формулы переходов: В ::= U \ 0 -.8 Вх V В21 (А) \ EU(BUB2) \ AU{BUВ2) где Р это формула элементарных высказываний, сопоставляющая булевское значение каждому означивающему элементу, а А это формула состояния.
Итак, в формулы состояний и переходов могут входить не только логические операторы - и V, но и темпоральный оператор U (until), комбинированый вместе с кванторами путей Е и А (соответственно кванторы существования и всеобщности). То есть оператор EU(Bi,B2) вычисляет существование такого пути от заданной разметки, что формула В\ выполняется до тех пор, пока не будет достигнута разметка, где выполняется В2. Оператор AU{B\,B2) вычисляет то же самое, но свойство должно выполняться на всех путях от заданной разметки. Логика ASK-CTL похожа на логику CTL за исключением оператора (...). Этот оператор позволяет переходить между формулами состояний и переходов. Т.е. делает возможным в формулы состояний включать формулы переходов. Так, если (В) это формула состояний, то она истинна на заданной разметке тогда и только тогда, когда при этой разметке в сети существует означивающий элемент, в котором выполнена формула В. Аналогично этот оператор определяется и для формул переходов6.
Анализ работы протокола ARTCP при множественных потерях сегментов
После анализа официальных документов, описывающих стандарт транспортного протокола TCP, было решено разбить модель на ряд функциональных модулей, каждый из которых моделирует определенную часть оригинального протокола. В терминах раскрашенных сетей Петри это разбиение можно представить в виде иерарахического дерева, каждый элемент которого представляет собой модель некоторой части оригинального протокола. Связи между элементами этого дерева показывают взаимосвязь подмоделей. Иерархия подмоделей показана на рисунке 2.2.
Корневой является подсеть TCPLayer, которая представляет собой модель протокола TCP. Любой протокол является промежуточным звеном и, с одной стороны, предоставляет некоторый сервис протоколам более высокого уровня, а с другой стороны, использует сервис, предоставляемый протоколами более низкого уровня. Так как основной задачей транспортного протокола является предоставление сервиса пользовательским процессам, то одной из важнейших частей модели является подмодель обработки вызовов пользовательских процессов, которая представлена на рис. 2.2 как UserCallProcessor. В процессе анализа этого аспекта работы протокола TCP мы сделали вывод, что любой пользовательский вызов может либо открыть транспортное соединение, либо быть обработанным, либо сбросить уже существующее транспортное соединение. Открытие транспортных соединений моделируется с помощью подсети OpenConnection. Эта подсеть моделирует как создание новых соединений, так и открытие в активном режиме уже созданных соединений. Подсетью AbortConnection моделируется сброс уже существующих соединений с помощью пользовательских вызовов. Для моделирования обработки остальных вызовов используется подсеть ProcessCall. В этом случае вызов либо обрабатывается сразу, либо помещается в буфер, где обрабатывется, когда наступают необходимые для этого условия. Необходимо также заметить, что все три подсети моделируют обработку ошибочных ситуаций.
Другой важной частью протокола TCP является организация процесса обмена сегментами через коммуникационную сеть. Это моделируется с помощью подсети TCPTransfer, которая функционально разделяется на две части — подсеть TCPSender, моделирующую передачу сегментов в коммуникационную сеть, и подсеть TCPReceiver, которая моделирует обработку пришедших сегментов. Передача данных от пользовательского процесса удаленной стороне моделируется с помощью подсети DataSend. Подсеть SendACK используется для моделирования передачи подтверждений удаленной стороне соединения. Моделирование различных механизмов ретрансляции (по тайм-ауту и быстрой ретрансляции) производится с помощью подсети Retransmits. Подсеть Transmit была добавлена при моделировании протокола ARTCP и служит для передачи сегментов в сеть с заданной скоростью. Прием сегментов моделируется с помощью следующих подсетей. Подсеть SYNProcessing моделирует обработку SYN-сегментов, которые используются для синхронизации транспортного соединения. Обработка сегментов для синхронизированых соединений производится с помощью двух подсетей — Preprocessing и Processing. Модуль, представленный подсетью Preprocessing, моделирует начальную обработку сегмента, в частности проверки, выполняемые при приеме сегмента. Для моделирования обработки сегментов в порядке их очередности используется подсеть Processing. Остальные подсети используются для моделирования служебных нужд протокола. Подсеть ResetConnection моделирует обработку сегментов, которые сбрасывают соединение, а подсеть DiscardSegment моделирует обработку сегментов, которые поступили локальным соединениям, находящимся в состоянии CLOSED.
Представленная модель моделирует аспекты работы транспортного протокола TCP согласно последним официальным стандартам, основные из которых перечислены в таблице 2.1. Технология построения каждой из показанных подсетей одинакова и будет рассмотрена далее.
Здесь мы рассмотрим принципы, по которым строились подсети, моделирующие отдельные аспекты работы протокола.
Первый шаг в построении подмодели функциональной части состоит в том, чтобы определить те служебные структуры протокола, которые необходимы для работы этой функциональной части протокола. Решение принимается на основе анализа стандартной спецификации протокола. Кроме этого необходимо определить, какие стандартные очереди необходимы — очередь пришедших пользовательских вызовов, очередь ответных реакций протокола, очереди пришедших и отправленных сегментов. На основе этих данных в подмодель включаются позиции, которые моделируют необходимые структуры. Как показывает практика, в большинстве случаев, никаких других позиций не требуется.
После этого создаются переходы, которые моделируют действия, необходимые для работы рассматриваемого функционального аспекта протокола. В большинстве случаев создается один переход, который собственно и осуществляет моделирование. Однако в ряде случаев требуется два перехода. Это имеет смысл делать тогда, когда моделируемый аспект имеет несколько вариантов работы. Например, в случае моделирования повторной передачи сегментов, один переход моделирует повторную передачу по таймеру, а второй — механизм быстрой повторной передачи. При создании переходов также необходимо учитывать что действие, моделируемое переходом, должно быть атомарным с точки зрения протокола.
Следующим шагом позиции и переходы соединяются с помощью дуг. Если некоторая структура протокола должна быть создана в процессе работы моделируемого аспекта, то создается исходящая дуга. В том случае, если служебная структура протокола удаляется, то входящая. Если происходит обновление значения служебной структуры, то создается пара дуг — входящая, с помощью которой изымается маркер со старым значением структуры и исходящая, с помощью которой в позицию помещается маркер с новым значением структуры. Итак, мы имеет подсеть, которая показывает структуру того аспекта работы протокола, который мы хотим промоделировать. Теперь необходимо задать охраны переходов подсети, которые будут определять, когда действие может быть выполнено, и выражения на дугах, которые показывают, как будет изменяться разметка сети, а, соответственно, и служебные структуры протокола. В общем случае для каждого из переходов подсети нам необходимо реализовать следующие функции:
