Моделирование и анализ сетевых транспортных протоколов с помощью раскрашенных сетей Петри тема автореферата и диссертации по математике, 01.01.09 ВАК РФ

На правах рукописи

Чалый Дмитрий Юрьевич

МОДЕЛИРОВАНИЕ И АНАЛИЗ СЕТЕВЫХ ТРАНСПОРТНЫХ ПРОТОКОЛОВ С ПОМОЩЬЮ РАСКРАШЕННЫХ СЕТЕЙ ПЕТРИ

01.01.09 — дискретная математика и математическая кибернетика

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

Ярославль — 2006

Работа выполнена в Ярославском государственном университете им. П.Г. Демидова на кафедре теоретической информатики.

Научный руководитель - кандидат физико-математических наук,

профессор

Соколов Валерий Анатольевич

Официальные оппоненты: доктор физико-математических наук,

профессор

Ломазова Ирина Александровна

кандидат физико-математических наук, Непомнящий Валерий Александрович

Ведущая организация - Институт системного программирования

РАН

Защита состоится "¿О " 2006 в ч. <^?мин. на за-

седании диссертационного совета Д 212.002.03 при Ярославском государственном университете им. П.Г. Демидова по адресу: 150008, г. Ярославль, ул. Союзная 144.

С диссертацией можно ознакомиться в библиотеке ЯрГУ им. П.Г. Демидова.

Автореферат разослан "

Учёный секретарь диссертационного советаЯблокова С.И

ОБЩАЯ ХАРАКТЕРИСТИКА РАБОТЫ Объект исследования и актуальность темы. Одним из важнейших достижений научно-технического прогресса в настоящее время являются коммуникационные системы, представляющие собой сети передачи информации. Успешное внедрение Интернет и интранет технологий приводит к тому, что человечество становится все более зависимым от надежности функционирования вычислительных устройств.

Транспортные протоколы являются важным элементом коммуникационной архитектуры сети Интернет (согласно исследованиям К. Томпсона, Дж. Миллера и Р. Уайлдера, около 95% всех переданных байтов и 85-95% всех переданных пакетов). Основной задачей протокола транспортного уровня является предоставление сервиса программным процессам для надежного и эффективного обмена информацией через ненадежную среду передачи — коммуникационную сеть. С точки зрения транспортного протокола сеть представляется в виде «черного ящика», где информация может теряться, переупорядочиваться, искажаться и, возможно, дублироваться. Под эффективностью работы транспортного протокола понимается прежде всего эффективное использование сетевых ресурсов — таких как, например, пропускная способность каналов передачи и буферов маршрутизаторов.

Предметом нашего исследования является транспортный протокол TCP (Transmission Control Protocol), который является основным транспортным протоколом коммуникационной архитектуры сети Интернет. Так как этот протокол постоянно изменяется и дополняется, то можно говорить о семействе протоколов TCP.

Исследование свойств транспортных протоколов, в частности различных версий протокола TCP, является важной и актуальной задачей, которая рассматривалась в ряде работ. Основным объектом исследований являлись алгоритмы управления потоком транспортных протоколов, а основным методом исследований, который использовался в этих работах — имитационное моделирование. Яркими представителями таких работ являются работы К. Фолла и С. Флойд по исследованию различных версий алгоритма управления потоком протокола TCP; в работах С. Шао, М. Санадиди и М. Герла, которые представляют новый протокол TCP Westwood, и обосновывают его эффективность; работы И. В. Алек-

сеева и В. А. Соколова, которые представляют новый протокол ARTCP (Adaptive Rate TCP) и на ряде модельных экспериментов обосновывают его преимущество перед стандартным TCP. Другим популярным методом исследования является построение аналитических моделей. Например, в работах У. Виллингера и М. Tarry рассматриваются модели алгоритма управления потоком и вопросы порождения протоколом TCP самоподобного трафика. Методы имитационного моделирования могут быть весьма экономичными для выявления многих ошибок, однако проверить все возможные взаимодействия и пути выполнения протокола вряд ли представляется возможным.

Одним из подходов к решению задачи корректности транспортных протоколов может быть построение формальных моделей и их последующий анализ с помощью формальных методов (например, методов model checking). Вопросы корректности коммуникационных протоколов рассматривались, например, в работах Дж. Хольцмана, который предлагает строить модели протоколов с помощью конечных автоматов и использовать эти модели для последующей верификации; в работах В. А. Непомнящего, Т. Г. Чуриной и Е. В. Окунишниковой предлагаются методы по моделированию спецификаций, представленных на языках Estelle и SDL с помощью сетей Петри высокого уровня. Однако применение этих подходов к моделированию и верификации семейства протоколов TCP затруднено тем, что стандартные документы, задающие их спецификацию, изложены на неформальном языке. Были опубликованы работы по построению моделей протокола TCP в терминах раскрашенных сетей Петри. В работе X. Фигейредо и JI. Кристенсена представляются результаты моделирования процесса обмена данными ряда версий протокола TCP, а в работе Б. Хана и Дж. Биллингтона рассматривается модель процессов установки и завершения соединений. Эти работы рассматривают некоторые фрагменты оригинального протокола; перед нами же стояла задача промоделировать стандарт протокола целиком. Другой особенностью этих работ является то, что основной акцент они делают именно на построении моделей, а не на разработке методов их исследования. В нашей работе кроме задачи построения моделей, рассматриваются вопросы анализа различных свойств протоколов, таких как производительность и корректность.

Цели и задачи работы. Создание новых модификаций протокола TCP, которые являются более эффективными и/или корректными, является несомненно важной задачей. При этом корректность исполнения протокола имеет приоритет перед производительностью. Поэтому создание формальных моделей протоколов и разработка способов анализа этих моделей является одним из методов, которые позволяют верифицировать корректность и убедиться в эффективности работы протокола.

Таким образом, главными целями проведенной работы являются:

1. разработка формальной технологии моделирования спецификаций семейства транспортных протоколов TCP;

2. описание и применение формальных методов анализа свойств полученных моделей;

3. создание эффективных алгоритмов работы транспортных протоколов.

Для достижения этих целей были поставлены следующие задачи:

1. разработать формальную модель последней версии стандартной спецификации протокола TCP;

2. описать методы модификации модели для представления новых версий этого протокола;

3. с помощью формального математического аппарата провести верификацию свойств построенной модели;

4. разработать алгоритмы более эффективного восстановления от множественных потерь для транспортного протокола ARTCP;

5. провести оценку эффективности приведенных алгоритмов для протокола ARTCP по сравнению со протоколами семейста TCP.

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

модификации для представления новых версий протоколов. Верификация построенной модели проводилась с помощью метода model checking с использованием темпоральной логики и методов анализа множеств достижимых состояний, разработанных для формализма раскрашенных сетей Петри. Для исследования производительности рассматриваемых транспортных протоколов использовался метод имитационного моделирования.

Научная новизна. Научной новизной обладают следующие решения, выносимые на защиту:

1. построенная модель последней стандартной спецификации протокола TCP и разработанная технология модификации этой модели для представления новых версий протокола;

2. с помощью представленной технологии была разработана формальная модель протокола ARTCP;

3. с использованием методов model checking был проверен ряд режимов работы протокола и было показано, что модель соответствует стандартной спецификации протокола;

4. в связи с обновлением спецификации протокола TCP, усовершенствована спецификация протокола ARTCP и описаны эффективные алгоритмы для восстановления множественных потерь сегментов;

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

Практическое значение работы. Разработанная технология моделирования была реализована в системе моделирования Design/CPN и может быть применена для автоматизированного анализа новых транспортных протоколов семейства TCP.

Апробация работы. Результаты работы докладывались на международной конференции Parallel Computer Technologies (Нижний Новгород, 2003 год), Всероссийской научной конференции «Методы и средства обработки информации* (Москва, 2003 год), международной конференции по вычислительной математике (Новосибирск, 2004 год), междисциплинарной конференции НБАТТ-21 (Петрозаводск, 2004 год), XVI

Международной научно-технической конференции <Математические методы и информационные технологии в экономике, социологии и образовании> (Пенза, 2005 год). Кроме того, полученные результаты обсуждались на семинаре «Моделирование и анализ информационных систем» ЯрГУ. Материалы диссертации вошли в отчет по гранту РФФИ №03-01-00804.

Публикации. За время работы над диссертацией было опубликовано 7 публикаций.

Структура и объем работы. Диссертация состоит из введения, трех глав и заключения. Работа изложена на 148 страницах, иллюстрирована 46 рисунками и содержит 10 таблиц. Список литературы содержит 102 наименования.

КРАТКОЕ СОДЕРЖАНИЕ РАБОТЫ

Введение

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

Глава 1. Коммуникационные транспортные протоколы

Первая глава посвящена описанию транспортных протоколов коммуникационной архитектуры TCP/IP. Здесь также подробно рассмотрен объект исследования — коммуникационный транспортный протокол TCP и его модификации.

В разделах 1.1-1.3 приводится современный взгляд на сети передачи данных. Упомянуты основные составляющие коммуникационной сети (раздел 1.1), приведена стандартная модель взаимодействия открытых систем (раздел 1.2) и обзорно рассмотрено назначение различных протоколов стека TCP/IP (раздел 1.3).

Протокол TCP (Transmission Control Protocol — протокол управления передачей) является основным протоколом транспортного уровня, используемым в Internet. С момента своего появления в 1981 году, опубликованный в RFC793 (RFC —Request for Comments), он постоянно совершенствовался и на данный момент существует множество документов, регламентирующих различные аспекты его работы. Раздел 1.4 посвящен описанию этого транспортного протокола и его модификаций. Пользователями сервиса, предоставляемого протоколом TCP, являются

пользовательские программные процессы. Один из вариантов интерфейса между пользовательскими процессами и TCP рассмотрен в документе RFC793. Существуют альтернативные подобные интерфейсы, например, интерфейс Berkeley Sockets. Мы будем рассматривать только интерфейс, изначально описанный в спецификации протокола RFC793, и приведенный в п. 1.4.1 работы.

Взаимодействие протокола TCP с протоколом нижележащего уровня описано в п. 1.4.2. Протокол TCP использует сервис, предоставляемый протоколом IP, для обеспечения коммуникации с удаленной стороной соединения. Протокол TCP разбивает полученные от пользователя данные на части и «упаковывает» их в специальную структуру, называемую сегментом. С помощью сегментов протокол отправляет не только данные, но и различные служебные сообщения. Протокол TCP использует протокол IP для отправления сегментов в сеть и получения их из сети.

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

В п. 1.4.4 рассматриваются алгоритмы работы протокола, которые обеспечивают надежную передачу данных через ненадежную среду связи. TCP-соединения являются полнодуплексными, т.е. информация может передаваться одновременно в обоих направлениях. Каждому передаваемому байту присваивается уникальный номер возрастающей последовательности передачи. Принятые получателем сегменты помещаются в буфер, из которого уже передаются программному процессу. Кроме этого получатель обязан сообщать отправителю с помощью подтверждений о тех байтах, которые уже получены. Подтверждения имеют кумулятивный характер, т.е. если отправитель получил подтверждение с номером п, то это значит что все байты по (п—1)-й включительно успешно получены. В

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

Для управления передачей сегментов протокол использует два вида алгоритмов. Во-первых, протоколом используется алгоритм «скользящего окна» (sliding window algorithm), для того чтобы предотвратить перегрузку буфера получателя. В процессе освобождения буфера получатель обязан сообщать об этом удаленной стороне. Во-вторых, для того чтобы реагировать на загруженность коммуникационной сети, используются алгоритмы управления потоком, стандарт которых представлен в RFC2581, RFC3390 и RFC3782.

Далее в работе описываются различные расширения протокола TCP, которые направлены на улучшение эффективности и надежности его работы. Рассматриваются мехнизмы выборочных подтверждений (selective acknowledgements), масштабирования окна (window scaling), алгоритмы, использующие временную метку (timestamp), алгоритм Limited Transmit.

После этого рассматривается алгоритм ARTCP (Adaptive Rate TCP), который характеризуется рядом существенных отличий от стандартного алгоритма управления потоком TCP. Так, скорость отправки сегментов в сеть определяется не размером окна передачи (как в TCP), а индивидуальной задержкой каждого сегмента. Изменение скорости передачи потока выражается в изменении его скважности (межсегментного временного интервала). Индикатором текущего состояния сети служит изменение скважности потока, измеряемое получателем, а не потеря сегмента как в стандартном TCP. В протоколе ARTCP устранена логическая зависимость алгоритмов коррекции ошибок передачи и управления потоком.

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

Глава 2. Моделирование транспортных протоколов с помощью раскрашенных сетей Петри.

В главе представляется построенная модель семейства транспортных протоколов TCP и рассматриваются принципы модификации модели для моделирования последующих версий протокола TCP.

В разделе 2.1 рассматривается определение структуры раскрашенных сетей Петри (CP-сети), их динамическое поведение, расширения этого класса сетей Петри, а также методы анализа свойств моделей и автоматические средства, поддерживающие этот формализм. Раскрашенная сеть Петри представляет собой ориентированный граф с двумя видами вершин — позициями и переходами, а также имеет блок определений. Блок определений раскрашенной сети Петри содержит определения типов, операций и функций, которые могут быть использованы для задания выражений, использующихся в CP-сети. На практике для этих целей используется язык CPN ML.

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

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

бы один переход.

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

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

Темпоральные логики, такие как СТЬ, являются мощным инструментом для исследования свойств параллельных и распределенных систем. Задачу проверки модели с помощью темпоральных, логик можно сформулировать следующим образом. Пусть задана формальная модель, некоторое состояние модели и формула темпоральной логики <р. Необходимо выяснить, удовлетворяет ли это состояние модели формуле темпоральной логики (р? Для раскрашенных сетей Петри была разработана логика АБК-СТЬ, которая может задавать свойства не только на множестве позиций, но и на множестве переходов.

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

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

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

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

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

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

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

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

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

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

• функцию, определяющую, какие сегменты должны быть отправлены удаленной стороне соединения в ответ на данное действие;

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

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

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

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

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

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

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

С момента публикации начальной спецификации протокола в 1981 году протокол TCP постоянно изменялся. Эти изменения были направлены как на исправление ошибок в протоколе, так и на введение новых механизмов, которые позволяют протоколу работать более эффективно. В разделе 2.8 рассмотрены методы, которые позволяют модифицировать модель для того, чтобы она могла представлять новые версии протокола TCP. Любое изменение протокола TCP затрагивает обычно изменение алгоритма работы протокола. Как следствие, иногда для этого необходимо вводить новые параметры для работы этих изменений (например, в контрольный блок соедиенения). Таким образом, для модификации модели необходимо предоставить достаточно удобные средства, которые позволяют модифицировать как структуры данных оригинального протокола, так и алгоритм работы протокола.

В работе рассматриваются два основных направления модификации алгоритма протокола: введение различных расширений и изменение алгоритма управления потоком. Кроме этого приводятся общие рекомендации по модификации модели. Под расширениями протокола понимаются прежде всего алгоритмы, предложенные в RFC1323, RFC2018, RFC2883. Эти алгоритмы расширяют функциональность протокола, являются стандартизированными, однако нигде не указано, что реализация, которая соответствует стандарту протокола, обязана их включать. Решение о том, необходимо ли учитывать алгоритм работы расширения при работе локального соединения, принимается на этапе синхронизации соединения. В работе рассматривается метод модификации модели для хранения параметров работы таких расширений, а также метод модификации блока определений модели, который позволяет реализовать алгоритм работы этих расширений. В отличие от расширений, которые могут быть включены или нет в реализацию протокола, алгоритм управления потоком обязан присутствовать в транспортном протоколе. Здесь мы также рас-

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

В общем случае метод модификации модели для представления новой версии протокола можно представить в следующем виде:

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

2. определение того, какие функциональные модули протокола затрагивает модификация;

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

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

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

Глава 3. Анализ свойств коммуникационных транспортных протоколов.

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

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

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

Раздел 3.2 посвящен рассмотрению набора темпоральных формул логики ASK-CTL, которые позволяют верифицировать нашу модель предоставляемого протоколом сервиса. В этом разделе явно выписаны темпоральные формулы, которые проверяют корректность обработки пользовательских вызовов согласно стандарту RFC793 с учетом исправлений из RFC1J22. Количество формул в наборе составляет 30 формул.

Любая формула из этого набора, имеет вид а Л, где а — это формула переходов, которая задает условие обработки некоторого пользовательского вызова, а А это темпоральная формула, которая проверяет обработку этого пользовательского вызова. Заметим, что а — это формула элементарных высказываний, которая в качестве условия включает как пользовательский вызов, так и условия (в частности, состояние локального соединения-адресата), при которых выражается его обработка. Можно сказать, что рассмотренная импликация задает частичную спецификацию обработки пользовательского вызова. Имея ввиду это, можно сформулировать следующую теорему:

Теорема 1 Пусть {ai Ai,..., ап => А„} — это набор свойств из раздела 3.2, тогда формула переходов логики ASK-CTL Ф s Лй=1(а!- => Ai) выражает полную спецификацию сервиса, предоставляемого протоколом TCP.

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

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

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

1. потери синхронизирующих сегментов коммуникационной сетью;

2. вызовы программного процесса, которые могут мешать протоколу

установить соединение;

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

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

В экспериментах были представлены две стороны транспортного соединения, которые пытаются синхронизироваться. При этом одна из сто-

рон выступает в активной роли инициатора установки соединения, а вторая — в пассивной роли стороны, которая принимает запрос на установку соединения. Каждой из сторон соединения пользовательский процесс отправляет вызовы, обработка которых зависит от состояния соединения. Причем, отправляются только такие вызовы, которые существенно изменяют состояние протокола, что влечет за собой, например, передачу сегментов удаленной стороне, сброс соединения и т.п. Множество таких вызовов было построено на основе анализа спецификации протокола RFC793 и RFC1122. Это множество является конечным для каждого из состояний, которое минует протокол в процессе установки соединения. Рассмотрим теперь, как изменяются состояния протокола в процессе выполнения такой модели:

1. пусть протокол находится в некотором состоянии state и для него построено множество вызовов щ ... и^, которые при обработке существенно изменяют состояние state',

2. недетерминированно выбирается некоторый вызов щ 6 щ...ип и обрабатывается, переводя протокол в состояние state'',

3. если состояние протокла state' не моделирует закрытое или синхронизированное соединение, переходим к шагу 1.

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

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

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

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

Построенное множество достижимых состояний не имеет циклов. Следовательно протокол открывает соединение за конечное число шагов. Было также проверено соответствие модели оригинальной спецификации протокола согласно подходу, описанному в разделе 3.2.

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

Раздел 3.5 посвящен анализу работы алгоритма протокола АИТСР при множественных потерях сегментов коммуникационной сетью и представлению более эффективных алгоритмов работы. В работах И. В. Алексеева и В. А. Соколова утверждается, что при потерях сегментов протокол АИТСР полагается на работу алгоритмов быстрой ретрансляции и повторной передачи по тайм-ауту. В случае потери одного сегмента

существует вероятность того, что эта потеря будет эффективно восстановлена с помощью алгоритма быстрой ретрансляции. Однако когда теряется более одного сегмента, только первый сегмент может быть восстановлен с помощью механизма быстрой ретрансляции, а остальные восстанавливаются с помощью ретрансляции по тайм-ауту, что является неэффективным (см., напр. работы К. Фолла и С. Флойд). Поэтому для более эффективного восстановления от множественных потерь сегментов для протокола TCP вводятся алгоритмы NewReno как стандартный алгоритм (когда невозможно использовать выборочные подтверждения), и алгоритм SACK, который не является официальным стандартом (когда возможно использовать выборочные подтверждения).

Вскоре после представления протокола ARTCP был выпущен стандарт протокола RFC2988, который определяет процедуру установки и управления таймером повторной передачи. Этот документ рекомендует устанавливать таймер для первого сегмента в очереди повторной передачи и ретранслировать по срабатыванию таймера только его. Это обновляет алгоритм протокола ARTCP, так как в работах И. В. Алексеева и В. А. Соколова утверждается, что для протокола ARTCP от протокола TCP сохраняются алгоритмы определения значения тайм-аута и установки таймера повторной передачи.

В работе представлены два алгоритма восстановления от множественных потерь сегментов для протокола ARTCP — NewReno ARTCP, который используется в том случае, когда невозможно использовать выборочные подтверждения, и SACK ARTCP, когда возможно использовать выборочные подтверждения. Основная идея алгоритмов состоит в том, чтобы до тайм-аута попытаться определить, какие сегменты были потеряны и передать их в сеть. Несмотря на то, что для протокола TCP были разработаны алгоритмы для более эффективного восстановления от множественных потерь сегментов, отличающаяся специфика протоколов ARTCP и TCP не позволяет применять эти алгоритмы непосредственно для протокола ARTCP.

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

анализа свойств производительности. В экспериментах рассматривается модель простой сетевой инфраструктуры, которая дополнительно загружается синтетическим трафиком, обладающим свойством самоподобия. Это позволяет моделировать нагрузку па выбранную сетевую архитектуру. При различной загрузке была показана более эффективная работа протоколов SACK ARTCP и NewReno ARTCP, чем протоколов SACK TCP и NewReno TCP. Кроме того, были рассмотрены случаи снижения производительности алгоритма управления потоком ARTCP. Основные выводы и результаты.

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

• в работе представлена разработанная технология построения модели последней спецификации протокола TCP и методы ее модификации для моделирования будущих версий этого протокола;

• в работе были предложены подходы к верификации протокола TCP. В качестве примеров описана формальная верификация процессов открытия и закрытия транспортного соединения;

• разработаны алгоритмы для восстановления после множественных потерь сегментов для протокола ARTCP, которые учитывают несколько вариантов работы: с использованием механизма выборочных подтверждений (SACK ARTCP) или без них (NewReno ARTCP);

• предложены подходы к решению задачи анализа производительности коммуникационных транспортных протоколов. В ходе экспериментов была показана более эффективная работа протоколов SACK ARTCP и NewReno ARTCP, чем у протоколов SACK TCP и NewReno TCP. Кроме этого, были рассмотрены случаи снижения производительности алгоритма управления потоком ARTCP.

ПУБЛИКАЦИИ ПО ТЕМЕ ДИССЕРТАЦИИ

1. Dmitry Ju. Chaly, Valéry A. Sokolov. An Extensible Coloured Petri Net Model of a Transport Protocol for Packet Switched Networks 11 Proceedings of PaCT'2003, Springer-Verlag.- 2003 - №2673.- p. 66-75 C. 58-69.

2. Соколов В. А., Тимофеев E. А., Чалый Д. Ю. Моделирование, оптимизация и верификация транспортных протоколов // Труды Пер-

вой Всероссийской научной конференции МСО-2003, Москва.— 2003.— стр. 254-259.

3. Чалый Д. Ю. Моделирование протоколов TCP и ARTCP с помощью раскрашенных сетей Петри // Моделирование и анализ информационных систем, Ярославль.— 2003.— №2— стр. 11-17,

4. Соколов В. А., Чалый Д. Ю. Методы исследования поведения транспортных протоколов в условия интенсивного сетевого трафика // Труды Международной конференции по вычислительной математике, Новосибирск,— 2004,— стр. 126-131.

5. Чалый Д. Ю. Моделирование транспортных протоколов коммуникационной сети Интернет // Труды 3-й междисциплинарной конференции НБАТТ-21, Петрозаводск.— 2004.— стр. 76-77.

6. Алексеев И. В., Соколов В. А., Чалый Д. Ю. Моделирование и анализ транспортных протоколов в информационных сетях // ЯрГУ им. П.Г. Демидова, Ярославль,— 2004.— 262 с.

7. Чалый Д. Ю. Анализ и верификация моделей транспортных протоколов коммуникационной сети Интернет // Труды XVI Международной научно-технической конференции «Математические методы и информационные технологии в экономике, социологии и образовании:», Пенза,- 2005,- стр. 199-201.

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

Подписано к печати 18.09.2006. Формат А5. Бумага офисная. Отпечатано на ризографе. Усл.-печ. л. —1,3. Заказ № 2078. Тираж 100 экз.

Редакционно-издательский центр МУБиНТ 150003 г. Ярославль, ул. Советская, 80 Лицензия ЛР № 071542 от 24.11.97

Введение

Предмет исследования.

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

Практическая ценность результатов.

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

Содержание работы.

1 Коммуникационные транспортные протоколы

1.1 Современные коммуникационные сети

1.2 Модель взаимодействия открытых систем

1.3 Семейство протоколов TCP/IP.

1.4 Transmission Control Protocol (TCP).

1.5 Протокол ARTCP

1.6 Модели коммуникационных протоколов и сетевого трафика.

2 Моделирование транспортных протоколов с помощью раскрашенных сетей Петри

2.1 Раскрашенные сети Петри

2.2 Моделирование служебных структур протокола.

2.3 Иерархическая структура модели

2.4 Построение модели функциональной части протокола.

2.5 Моделирование обработки пользовательских вызовов.

2.6 Моделирование передачи сегментов в сеть.

2.7 Моделирование обработки пришедших сегментов.

2.8 Модификация модели.

2.9 Общая схема модельных экспериментов.

Предмет исследования

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

Транспортные протоколы являются важным элементом коммуникационной архитектуры сети Интернет (согласно исследованиям [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. Работа завершается выводами.

Заключение

В диссертации рассмотрены вопросы моделирования и анализа коммуникационных транспортных протоколов семейства TCP с помощью раскрашенных сетей Петри. В работе изложена разработанная технология построения модели последней спецификации протокола TCP и методы ее модификации для моделирования будущих версий этого протокола. Для создания и исследования модели использован пакет Design/CPN [98]. Одним из дальнейших направлений работы будет перенос этой модели в более современный пакет CPN Tools [99].

В работе были предложены подходы к верификации протокола TCP. В качестве примеров описана формальная верификация процессов открытия и закрытия транспортного соединения.

Другими результатами диссертации являются изложенные алгоритмы для восстановления после множественных потерь сегментов для протокола ARTCP, которые учитывают несколько вариантов работы: с использованием механизма выборочных подтверждений или без них. Одним из дальнейших направлений исследований можно назвать поиск других параметров (кроме оценки свободной пропускной способности сети и RTT) для управления потоком, а также возможное упрощение алгоритма протокола.

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

1. Алексеев И.В. Адаптивная схема управления потоком для транспортного протокола в сетях с коммутацией пакетов. // Дисс. на соискание степени к.ф.-м.н. Ярославль. 2000.

2. Алексеев И.В., Соколов В.А., Чалый Д.Ю. Моделирование и анализ транспортных протоколов в информационных сетях. // Ярославский государственный университет. Ярославль, 2004.

3. Соколов В.А., Тимофеев Е.А., Чалый Д.Ю. Моделирование, оптимизация и верификация транспортных протоколов.// Труды первой Всероссийской конференции МСО-2003. Под. ред. J1.H. Королева. Москва, 2003.

4. Чалый Д.Ю. Моделирование протоколов TCP и ARTCP с помощью раскрашенных сетей Петри.// Моделирование и анализ информационных систем. № 2 за 2003 год. Ярославль, 2003. стр. 11-17.

5. Соколов В.А., Чалый Д.Ю. Методы исследования поведения транспортных протоколов в условиях интенсивного сетевого трафика. // Труды Международной конференции по вычислительной математике. Под. ред. Ю.И. Шокина и др. Новосибирск, 2004. стр. 126— 131.

6. Чалый Д.Ю. Моделирование коммуникационных протоколов коммуникационной сети Интернет. // Материалы 3-й междисциплинарной конференции НБАТТ-21. Под. ред. С. Е. Ка-рашурова. Петрозаводск, 2004. стр. 76-77.

7. Соколов В.А., Чалый Д.Ю. Построение и анализ формальных моделей семейства транспортных протоколов TCP. // Труды III Международной конференции «Параллельные вычисления и задачи управления», (принято к публикации)

8. Кларк Э., Грамберг О., Пелед Д. Верификация моделей программ: Model-Checking. МЦ-НМО, Москва, 2002.

9. Ломазова И.А. Сети Петри и анализ поведенческих свойст распредленных систем. Ярославль, 2002. 164 с.

10. Непомнящий В.А., Алексеев А.Г., Быстрое А.В., Куртов С.А., Мыльников С.П., Оку-нишникова Е.В., Чубарев П.А., Чурина Т.Г. Верификация Estelle-спецификаций распределенных систем посредством раскрашенных сетей Петри. Новосибирск, 1998.

11. Chaly D. Ju., Sokolov V. A. An Extensible Coloured Petri Net Model of a Transport Protocol for Packet Switched Networks. // In Proceedings of Parallel Computer Technologies'2003, LNCS Vol. 2551, Springer-Verlag, 2003. p. 66-75.

12. Alekseev I.V., Sokolov V.A. ARTCP: Efficient Algorithm for Transport Protocol for Packet Switched Networks. // In Proceedings of Parallel Computer Technologies'2001. Lecture Notes in Computer Science, Vol. 2127. Springer-Verlag, 2001. стр. 159-174.

13. Alekseev I.V., Sokolov V.A. Modelling and Traffic Analysis of the Adaptive Rate Transport Protocol. // Future Generation Computer Systems. Number 6, Vol. 18. NH Elsevier, 2002. стр. 813-827.

14. Holzmann G. Design and Validation of Computer Protocols. Prentice-Hall, 1991.

15. Transmission Control Protocol. DARPA Internet Program. Protocol Specification. RFC793, September, 1981. Web site: www.rfc-editor.org

16. Clark D. D. Window and Acknowledgement Strategy in TCP. RFC813, July, 1982. Web site: www.rfc-editor.org

17. Postel J. The TCP Maximum Segment Size and Related Topics. RFC879, November, 1983. Web site: www.rfc-editor.org

18. Nagle J. Congestion Control in IP/TCP Internetworks. RFC896, January, 1984. Web site: www.rfc-editor.org

19. Reynolds J., Postel J. Assigned Numbers. RFC1010, May, 1987. Web site: www.rfc-editor.org

20. Jacobson V., Braden R. TCP Extensions for Long-Delay Paths. RFC1072, October, 1988. Web site: www.rfc-editor.org

21. Braden R. (Ed.) Requirements for Internet Hosts — Communication Layers. RFC1122, October, 1989. Web site: www.rfc-editor.org

22. Socolofsky Т., Kale С. A TCP/IP Tutorial. RFC1180, January 1991. Web site: www.rfc-editor.org

23. Jacobson V., Braden R., Zhang L. TCP Extension for High-Speed Paths. RFC1185, October, 1990. Web site: www.rfc-editor.org

24. O'Malley S., Peterson L. TCP Extensions Considered Harmful. RFC1263, October, 1991. Web site: www.rfc-editor.org

25. Jacobson V., Braden R., Borman D. TCP Extensions for High Performance. RFC1323, May, 1992. Web site: www.rfc-editor.org

26. Braden R. TIME-WAIT Assasination Hazards in TCP. RFC1337, May, 1992. Web site: www.rfc-editor.org

27. Connoly Т., Amer P., Conrad P. An Extension to TCP: Partial Order Service. RFC1693, November, 1994. Web site: www.rfc-editor.org

28. Stevens W. TCP Slow Start, Congestion Avoidance, Fast Retransmit and Fast Recovery Algorithms. RFC2001, January, 1997. Web site: www.rfc-editor.org

29. Mathis M., Mahdavi J., Floyd S., Romanow A. TCP Selective Acknowledgement Options. RFC2018, October, 1996. Web site: www.rfc-editor.org

30. Bradner S. Key Words for Use in RFCs to Indicate Requirement Levels. RFC2119, March,1997. Web site: www.rfc-editor.org

31. Touch J. TCP Control Block Interdependence. RFC2140, April, 1997. Web site: www.rfc-editor.org

32. Borman D. TCP and UDP over IPv6 Jumbograms. RFC2147, May, 1997. Web site: www.rfc-editor.org

33. Parker S., Schmechel C. Some Testing Tools for TCP Implementors. RFC2398, August,1998. Web site: www.rfc-editor.org

34. Allman M., Floyd S., Partridge C. Increasing TCP's Initial Window. RFC2414, September, 1998. Web site: www.rfc-editor.org

35. Poduri К., Nichols К. Simulation Studies of Increased Initial TCP Window Size. RFC2415, September, 1998. Web site: www.rfc-editor.org

36. Shepard Т., Partridge C. When TCP Starts Up With Four Packets Into Only Three Buffers. RFC2416, September, 1998. Web site: www.rfc-editor.org

37. Ramakrishnan K., Floyd S. A Proposal to Add Explicit Congestion Notification (ECN) to IP. RFC2481, January, 1999. Web site: www.rfc-editor.org

38. Allman M., Glover D., Sanchez L. Enhancing TCP Over Sattelite Channels Using Standard Mechanisms. RFC2488, January, 1999. Web site: www.rfc-editor.org

39. Paxson V., Allman M., Dawson S., Fenner W., Griner J., Heavens /., Lahey K., Semke J., Volz B. Known TCP Implementation Problems. RFC2525, March, 1999. Web site: www.rfc-editor.org

40. Allman M., Paxson V., Stevens W. TCP Congestion Control. RFC2581, April, 1999. Web site: www.rfc-editor.org

41. Floyd S., Henderson T. The NewReno Modification to TCP's Fast Recovery Algorithm. RFC2582, April, 1999. Web site: www.rfc-editor.org

42. Allman M., Dawkins S., Glover D., Griner J., Tran D., Henderson Т., Heideman J., Touch J., Kruse H., Ostermann S., Scott K., Semke J. Ongoing TCP Research Related to Satellites. RFC2760, February, 2000. Web site: www.rfc-editor.org

43. Handley M., Padhye J., Floyd S. TCP Congestion Window Validation. RFC2861, June, 2000. Web site: www.rfc-editor.org

44. Xiao X., Hannan A., Paxson V., Crabbe E. TCP Processing of the IPv4 Precedence Field. RFC2873, June, 2000. Web site: www.rfc-editor.org

45. Floyd S., Mahdavi J., Mathis M., Podolsky M. An Extension to the Selective Acknowledgement (SACK) Option for TCP. RFC2883, July, 2000. Web site: www.rfc-editor.org

46. Hadi Salim J., Ahmed U. Performance Evaluation of Explicit Congestion Notification (ECN) in IP Networks. RFC2884, July, 2000. Web site: www.rfc-editor.org

47. Lahey K. TCP Problems with Path MTU Discovery. RFC2923, September, 2000. Web site: www.rfc-editor.org

48. Paxson V., Allman M. Computing TCP's Retransmission Timer. RFC2988, November, 2000. Web site: www.rfc-editor.org

49. Allman M., Balakrishnan H., Floyd S. Enhancing TCP's Loss Recovery Using Limited Transmit. RFC3042, January, 2001. Web site: www.rfc-editor.org

50. Ramakrishnan K., Floyd S., Black D. The Addition of Explicit Congestion Notification (ECN) to IP. RFC3168, Septempber, 2001. Web site: www.rfc-editor.org

51. Floyd S. Inappropriate TCP Resets Considered Harmful. RFC3360, August, 2002. Web site: www.rfc-editor.org

52. Allman M., Floyd S., Partridge C. Increasing TCP's Initial Window. RFC3390, October, 2002. Web site: www.rfc-editor.org

53. Handley M., Floyd S., Padhye /., Widmer J. TCP Friendly Rate Control (TFRC): Protocol Specification. RFC3448, January, 2003. Web site: www.rfc-editor.org

54. Balakrishnan H., Padmanabhan V. N., Fairhurst G., Sooriyabandara M. TCP Performance Implications of Network Path Assymetry. RFC3449, December, 2002. Web site: www.rfc-editor.org

55. Allman M. TCP Congestion Control with Appropriate Byte Counting (ABC). RFC3465, February, 2003. Web site: www.rfc-editor.org

56. Ludwig R., Meyer M. The Eifel Detection Algorithm for TCP. RFC3522, April, 2003. Web site: www.rfc-editor.org

57. Spring N., Wetheral D., Ely D. Robust Explicit Congestion Notification (ECN) Signaling with Nonces. RFC3540, June, 2003. Web site: www.rfc-editor.org

58. Floyd S. Highspeed TCP for Large Congestion Windows. RFC3649, December, 2003. Web site: www.rfc-editor.org

59. Floyd S. Limited Slow-Start for TCP with Large Congestion Windows. RFC3742, March, 2004. Web site: www.rfc-editor.org

60. Floyd S., Henderson Т., Gurtov A. The NewReno Modification to TCP's Fast Recovery Algorithm. RFC3782, April, 2004. Web site: www.rfc-editor.org

61. Ludwig R., Gurtov A. The Eifel Response Algorithm for TCP. RFC4015, February, 2005. Web site: www.rfc-editor.org

62. Raghunarayan R (Ed.). Management Information Base for the Transmission Control Protocol (TCP). RFC4022, March, 2005. Web site: www.rfc-editor.org

63. Karn P., Partridge C. Improving Round-Trip Time Estimates in Reliable Transport Protocols. // In Proceedings of ACM SIGCOMM'87. 1987.

64. Fall K., Floyd S. Simulation-based Comparisons of Tahoe, Reno, and SACK TCP. // Computer Communications Review, 26(3). 1996. стр. 5-21.

65. Shao S., Sanadidi M. Y., Gerla M. A Simulation Study of the Interoperability of TCPW with RED and ECN. // In Proceedings of SPECTS 2003, Montreal, Canada, July 2003.

66. Figueiredo D.R., Liu В., Feldmann A., Misra V., Towsley D., Willinger W. On TCP and self-similar traffic. // Performance Evaluation, №61. Elsevier, 2005. p. 129-141.

67. Paxson V. Measurements and Analysis of End-to-End Internet Dynamics. // PhD thesis, University of California, Berkeley. 1997.

68. Leland W., Willinger W., Taqqu M., Wilson D. On the Self-Similar Nature of Ethernet Traffic (Extended Version). // IEEE/ACM Transactions on Networking. 2(1). 1994. p. 1-15.

69. Taqqu M., Willinger W., Sherman R. Proof of Fundamental Result in Self-Similar Traffic Modelling. // Computer Communications Review. № 27. 1997. p. 5-23.

70. Thompson K., Miller G.3., Wilder R. Wide-Area Internet Traffic Patterns and Characteristics. // In IEEE Networks, November, 1997.

71. Youngmi loo, Ribeiro V., Feldmann A., Gilbert A., Willinger W. TCP/IP traffic dynamics and network performance: A lesson in workload modeling, flow control, and trace-driven simulations. // ACM Computer Communication Review, April, 2001.

72. Network Simulator Ns-2. Web site: http://www.isi.edu/nsnam/ns/

73. Comer D. Internetworking with TCP/IP, Volume 2: Design Implementation and Internals. // Prentice Hall, NJ, 1994.

74. Han В., Billington J. Experience with Modelling TCP's Connection Management Procedures. // Proceedings of 5th Workshop and Tutorial on Practical Use of Coloured Petri Nets and the CPN Tools. Aarhus, Denmark. 2004. p. 57.-77.

75. Kumar A. Comparative Performance Analysis of Versions of TCP in a Local Network with a Lossy Link. // IEEE/ACM Transactions on Networking, №6. 1998. p. 485-498.

76. Ost A., Haverkroft B.R. Analysis of Windowing Mechanisms with Infinite-State Stochastic Petri Nets. // Performance Evaluation Review, №26(2). 1998. p. 38-46.

77. Gordon S. Verification of the WAP Transaction Layer Using Coloured Petri Nets. // PhD Thesis, University of South Australia, 2001.

78. Clarke E. M., Emerson E. A., Sistla A. P. Automatic Verification of Finite State Concurrent System Using Temporal Logic. // ACM Transactions on Programming Languages and Systems, №8(2), 1986. стр. 244-263.

79. Jensen K. Coloured Petri Nets. Basic Concepts, Analysis Methods and Practical Use. Vol. 1, Basic Concepts. // Monographs in Theoretical Computer Science. Springer-Verlag, 1997. 2nd corrected printing.

80. Jensen K. Coloured Petri Nets. Basic Concepts, Analysis Methods and Practical Use. Vol. 2, Analysis Methods. // Monographs in Theoretical Computer Science. Springer-Verlag, 1997. 2nd corrected printing.

81. Jensen K. Coloured Petri Nets. Basic Concepts, Analysis Methods and Practical Use. Vol. 2, Practical Use. // Monographs in Theoretical Computer Science. Springer-Verlag, 1997.

82. Jensen K. Coloured Petri Nets with Time Stamps. // Computer Science Department, Aarhus University, Denmark, 1991.

83. Jensen K. An Introduction to the Theoretical Aspects of Coloured Petri Nets. // In (eds.): de Bakker J. W., de Roever W.-P., Rozenberg G. A Decade of Concurrency, LNCS Vol. 803, Springer-Verlag, 1994. стр. 230-272.

84. Shin /., Levis A.H. Performance Prediction Model Generator Powered by Occurrence Graph Analyzer of Design/CPN. // Proceedings of 2nd Workshop on Practical Use of Coloured Petri Nets and Design/CPN. Aarhus, Denmark. 1999. p. 191-210.

85. Christensen S., Haagh Т. B. Overview of CPN ML Syntax. // University of Aarhus, 1996.

86. Design/CPN Reference Manual for X-Windows, Version 2.0. // Meta Software Corporation, 1993.

87. Jensen K., Christensen S., Kristensen L. M. Design/CPN Occurence Graph Tool Manual, Version 3.0.// Department of Computer Science, Aarhus University, Aarhus, Denmark, 1996.

88. J0rgensen J. В., Kristensen L. M. Design/CPN OE/OS Graph Manual, Version 1.0. 11 Department of Computer Science, Aarhus Unversity, Denmark, 1996.

89. Lindstr0m В., Wells L. Design/CPN Performance Tool Manual, Version 1.0. // Department of Computer Science, Aaurhus University, Aarhus, Denmark, 1999.

90. Christensen S., Mortensen К. H. Design/CPN ASK-CTL Manual, Version 0.9. // Department of Computer Science, Aaurhus University, Aarhus, Denmark, 1996.

91. Christensen S., Kristensen L. M., Mailund T. Design/CPN Sweep Line Method Library. // Department of Computer Science, Aarhus University, Denmark, 2001.

92. University of Aarhus. Design/CPN Online. Web site: http://www.daimi.au.dk/designCPN/

93. University of Aarhus. CPNTools Online. Web site: http://www.daimi.au.dk/"cpntools/

94. Ullman J. D. Elements of ML Programming. // Prentice Hall, Englewood Cliffs, NJ, 1994.

95. Milner R., Tofte M., Harper R., MacQueen D. The Definition of Standard ML (Revised). // MIT Press, 1997.

96. Standard ML of New Jersey. Web site: http://cm.bell-labs.com/cm/cs/what/smlnj.