Моделирование распределенных систем и анализ их семантических свойств тема диссертации и автореферата по ВАК РФ 01.01.09, доктор физико-математических наук Соколов, Валерий Анатольевич

• Соколов, Валерий Анатольевич
• доктор физико-математических наук
• 2006

Оглавление диссертации доктор физико-математических наук Соколов, Валерий Анатольевич

Введение

1 Структурированные системы переходов

1.1. Предварительные сведения.

1.2. Системы помеченных переходов.

1.3. Примеры вполне структурированных систем переходов

2 Счетчиковые машины

2.1. Счетчиковые машины Минского.

2.2. Счетчиковые машины с потерями.

2.3. Счетчиковые машины с обнулениями и ошибками проверки на нуль.

2.4. Недетерминированные счетчиковые машины.

3 Темпоральные свойства систем переходов

3.1. Метод проверки модели.

3.2. Темпоральные свойства систем переходов.

4 Модели Dataflow - программ

4.1 Модели и свойства класса структурированных программ в языках потоков данных.

4.2 О проблеме достижимости в графах потоков данных с очередями и стеками.

5 Язык рекурсивно-параллельного программирования: семантика и приложение к алгебраическим вычислениям

5.1 Модель семантнки рекурспвнопараллельных программ

5.2 Язык рекурсивно-параллельного программирования и его применение к алгебраическим вычислениям.

6 Моделирование и анализ протоколов

6.1 Протокол TCP с адаптацией скорости

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

Введение диссертации (часть автореферата) на тему «Моделирование распределенных систем и анализ их семантических свойств»

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

За последнее время отмечается резкое возрастание интереса исследователей к проблемам, связанным с разработкой методов моделирования и проверки корректности параллельных и распределенных систем, накоплено большое количество теоретических результатов и практического опыта в этой области. Среди отечественных исследований по спецификации, моделированию и анализу сложных (в т.ч., параллельных и распределенных) систем отметим работы Н.А. Анисимова, О.Л. Банд-ман, И.Б. Вирбицкайте, В.В. Воеводина, Н.В. Евтушенко, В.А. Захарова, Ю.Г. Карпова, В.Е. Котова, И.А. Ломазовой, В.А. Непомнящего, А.К. Петренко, Р.Л. Смелянского, Л.А. Черкасовой, Н.В. Шилова.

При исследовании сложных систем зачастую приходится строить формальные модели, которые представляют собой системы переходов с бесконечным числом состояний. В этом случае многие средства анализа и верификации, производящие полный перебор пространства состояний, становятся неприменимыми. Тем не менее, для некоторых ограниченных классов систем с бесконечным числом состояний разными авторами были разработаны достаточно эффективные методы верификации (как, например, в работах P. Abdulla, К. Cerans, A. Finkel, В. Jonsson, F. Moller,

Ph. Schnoebelen [57, 112, 159]. В частности, оказалось, что метод проверки модели (Model Checking), широко используемый при автоматической верификации систем с конечным числом состояний, может быть применим для некоторых классов систем с бесконечным числом состояний и подмножеств темпоральных логик. Примерами формальных моделей, являющихся системами переходов с бесконечным числом состояний и позволяющих описывать параллельные и распределенные системы, являются магазинные автоматы [17, 56], сети Петри [21], ВРР (Basic Parallel Processes) [94], LCS (Lossy Channel Systems - системы с каналами, теряющими сообщения) [61, 62], Real-Time Automata(aBTOMaTbi реального времени) [71] и др.

Метод Model Checking - один из наиболее перспективных подходов к решению проблемы верификации [95]. В качестве языков спецификации для выражения свойств систем при этом подходе используются темпоральные логики. Задача проверки модели состоит в определении выполнимости для системы, заданной формальным образом (в виде формальной модели), сво3-писанною формулой темпоральной логики.

Исследования систем переходов с бесконечным числом состояний были мотивированы теорией формальных языков и грамматик [132, 56, 17]. Во-первых, в этой теории бесконечные языки описываются конечными грамматиками, а во-вторых, некоторые проблемы для языков, например, проблема эквивалентности регулярных языков, являются разрешимыми. Следовательно, не все проблемы систем переходов с бесконечным числом состояний неразрешимы. По аналогии с теорией формальных языков были введены новые формализмы для описания бесконечных систем переходов.

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

Указанные формализмы, как и многие другие, могут быть рассмотрены как вполне структурированные системы помеченных переходов [57, 112].

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

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

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

Ранее в ряде публикаций таких авторов, как A. Bouajjani, О. Burkart, J. Esparza, A. Kiehn, R. Мауг, из которых, например, можно выделить [88, 80, 107, 108], исследовались вопросы разрешимости задачи проверки модели для некоторых конкретных представителей класса вполне структурированных систем переходов, а именно магазинных автоматов, сетей Петри, ВРР, LVAS (Lossy Vector Addition Systems) и различных темпоральных логик линейного времени и ветвящегося времени. Мы в нашей работе исходим из позиции обобщения и акцентируем внимание на проблеме разрешимости темпоральных свойств для различных классов вполне структурированных систем помеченных переходов, в частности для класса вполне структурированных систем переходов автоматного типа, которые из-за своей специфической структуры можно также отнести и к классу систем переходов, независимых от данных.

Внимание исследователей практически обходит системы переходов, независимые от данных (за исключением систем переходов с конечным числом состояний). Тем не менее, системы, принадлежащие к этому классу, могут быть достаточно выразительными и нетривиальными. Для демонстрации этого факта в диссертации представлен специальный фрагмент алгебры процессов, построенный на основе таких хорошо известных алгебр процессов, как CCS (Calculus of Communicating Systems - исчисление взаимодействующих систем) Милнера [156] и SCP (Communicating Sequential Processes - взаимодействующие последовательные процессы) Хоара [128], позволяющий строить формальные модели (параллельных и распределенных систем), которые могут быть рассмотрены как независимые от данных помеченные системы переходов, а точнее, как вполне структурированные системы переходов автоматного типа.

В качестве примера конкретной реализации этого фрагмента представлен формализм, который называется взаимодействующие раскрашивающие процессы (ССР - Communicating Colouring Processes), позволяющий строить модели распределенных систем, где поведение каждого компонента описывается последовательным процессом и между ними организовано взаимодействие, направленное на обмен и передачу пакетов информации. Формализм ССР принимает во внимание факт передачи данных, а также позволяет отслеживать перемещение данных различного типа между компонентами системы. Но переход из одного состояния в другое не зависит от оперируемых данных, а определяется только управляющими состояниями. Отметим, что в книге И. А. Ломазовой [36] для моделирования и анализа распределенных систем с объектной структурой предлагается использовать вложенные сети Петри, которые также рассматриваются как вполне структурированные системы переходов и являются интересным примером систем переходов с сильной совместимостью по возрастанию отношения квазипорядка (на множестве состояний) с отношением переходов. В нашей работе вложенные сети Петри не рассматриваются; для ознакомления с этим формализмом, являющимся расширением обыкновенных сетей Петри, рекомендуется обратиться к упомянутой выше книге [36].

В настоящее время перспективным направлением является разработка изобразительных языков программирования, реализующих концепцию потоков данных. Такие языки противостоят широко известным визуальным системам Visual Basic, Visual С++, Delphi, которые являются в действительности текстуальными языками внутри визуальной среды.

Разработка языков потоков данных была начата около двадцати лет назад в работах Д. Денниса, но только сейчас на рынке программного обеспечения появился первый широко доступный язык потоков данных: язык Prograph фирмы Pictorius Incorporated [173].

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

Однако, проблемы семантической корректности программ в языках потоков данных столь же актуальны, как и в текстуальных языках. Кроме объективных причин семантических ошибок, связанных с неформальным, нечетким пониманием задачи, необычный изобразительный синтаксис языков потоков данных может быть причиной написания некорректных программ. Семантика программ потоков данных детально исследована в статье А.Рабиновича, В.А.Трахтенброта [172]. Однако, эта работа не дает конструктивного ответа на вопрос о том, как практически обеспечить семантическую корректность программ в языках потоков данных. Задача выработки и обоснования практических рекомендаций для обеспечения семантической корректности программ в языках потоков данных требует специального исследования.

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

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

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

Для последовательных вычислительных систем известен ряд подходов к разработке программного обеспечения, среди которых особое место принадлежит структурному программированию [1, 15, 35]. Значительно сложнее обстоит дело с разработкой программного обеспечения для параллельных вычислительных систем. В настоящей работе предлагаются методы и средства программирования, применимые при следующих ограничениях:

1. рекурсивно-параллельная форма представления программ;

2. динамический способ распараллеливания;

3. однородность структуры вычислительной системы.

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

Однако написание программы в рекурсивно-параллельном стиле не является достаточным условием ее эффективного выполнения. С точки зрения распараллеливания она должна быть написана таким обрат зом, чтобы накладные расходы на организацию рекурсивных вызовов процедур, порождение и синхронизацию параллельных процессов были значительно меньше, чем объемы полезных вычислений, связанных с параллельными процессами. В [13] приведено описание рекурсивно-параллельного языка С (сокращенно REPAC) и ряда эффективных приемов рекурсивно-параллельного программирования. В нашей работе рассматривается подход к построению формальной модели для языка REPAC Эта модель будет служить семантической областью, в которой язык программирования REPAC может быть интерпретирован. Необходимость этого обусловлена желанием иметь модель, на базе которой можно было бы разрабатывать новое поколение средств для анализа потока управления в рекурсивно-параллельных программах и для их диагностики.

Если принципы рекурсивного программирования для последовательных вычислительных систем детально исследовались [1,10], то при автоматизации рекурсивно-параллельного программирования возникает целый ряд проблем.

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

Во-вторых, модульное программирование для многопроцессорных вычислительных систем во многих случаях дает возможность получать лишь последовательно-параллельные программы [12], которые далеко не всегда оказываются самыми эффективными.

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

В диссертации дается описание предназначенных для решения указанных проблем новых методов рекурсивно-параллельного программирования и поддерживающего эти методы языка GSTC (Generalized STencil С).

Еще один класс систем, который является объектом нашего исследования, - коммуникационные протоколы. В последнее десятилетие наблюдается быстрое и постоянно нарастающее развитие сети Интернет.

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

Протоколы транспортного уровня используются для обеспечения коммуникации между конечными системами. Транспортные протоколы создают большую долю трафика в сети Интернет, поэтому эффективность механизма управления потоком определяет то, насколько эффективно будут использоваться ресурсы сети. Наиболее важным протоколом транспортного уровня является протокол управления передачей TCP (Transmission Control Protocol), который предназначен для обеспечения надежной передачи информации между конечными системами. Начальная спецификация протокола дана в [170]. С момента выхода этой спецификации было сделано множество дополнений, направленных как на исправление ошибок в протоколе, так и на создание новых алгоритмов работы протокола (например, [82, 68, 69, 65]). Большинство изменений затрагивают как раз механизм управления потоком TCP.

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

Протокол ARTCP (Adaptive Rate TCP) [65] использует адаптивную схему управления потоком. Цель алгоритма ARTCP состоит в том, чтобы определить свободную пропускную способность сети, а потом использовать эту оценку для расчета скорости отправления сегментов в сеть. Для оценки пропускной способности получатель данных измеряет скорость поступающих к нему сегментов и пересылает это значение отправителю в сегментах, подтверждающих прием данных. На основе этого значения и значения времени возврата (время пути сегмента от отправителя к получателю плюс время пути подтверждения обратно) алгоритм ARTCP вычисляет скорость передачи отправителем новых сегментов в сеть.

Одно из главных преимуществ алгоритма управления потоком ARTCP состоит в том, что он не использует потерю сегмента как индикатор перегрузки сети. В работах [65, 66] была показана эффективность работы алгоритма управления потоком ARTCP по сравнению со стандартным алгоритмом управления потоком.

Следующий шаг в модификации TCP состоит в том, чтобы использовать все возможности ARTCP, но заменить трудно вычисляемые временные замеры на значения длин очередей. Для этого нужно скорость заменить на произведение интенсивности поступления сегментов заданного типа на их число в очереди. Такая модификация не требует (в отличие от ARTCP) внесения новых полей в протокол и, кроме того, позволяет исключить некоторые замеры времени и упростить алгоритм управления потоком. В [185] показано, что при этом в среднем можно получить такое же качество работы, как и у ARTCP.

Цель работы заключается в разработке методов построения формальных моделей и анализа поведенческих свойств некоторых классов распределенных систем: систем переходов с бесконечным множеством состояний, Dataflow-nporpaMM, рекурсивно-параллельных программ, коммуникационных протоколов.

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

• Определен и исследован новый класс вполне структурированных систем переходов автоматного типа.

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

• Предложена реализация класса взаимодействующих процессов, независимых отданных - взаимодействующие раскрашивающие процессы.

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

• Предложен новый метод построения структурированных Dataflow-nporpaMM на основе модели языка Денниса и доказана алгоритмическая полнота этого класса программ.

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

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

Методы исследования основаны на использовании аппарата математической логики, теории квазипорядков, сетей Петри, конечных автоматов, теории алгоритмов, формальных языков, теоретического программирования и теории массового обслуживания. Исследование проблемы корректности распределенных систем опирается на применение темпоральных логик и метода проверки модели (Model Checking), а при построении моделей Dataflow-nporpaMM используется язык Денниса.

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

Теоретическая и практическая значимость. Работа носит теоретический характер, однако ее результаты могут быть использованы для решения некоторых прикладных задач при разработке моделей распределенных систем: параллельных программ, коммуникационных протоколов, взаимодействующих автоматов, программ потоков данных и других, для их семантического анализа и верификации. Кроме того, научные результаты, полученные при выполнении данной работы, легли в основу трех монографий и двух учебных пособий для студентов вузов, одно из которых с грифом Министерства общего и профессионального образования РФ (1998 г.), а другое - с грифом УМО по классическому университетскому образованию РФ (2006 г.).

Структура работы. Диссертация состоит из введения, шести глав, заключения, списка литературы и приложения.

Заключение диссертации по теме «Дискретная математика и математическая кибернетика», Соколов, Валерий Анатольевич

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

Укажем основные научные результаты, полученные в диссертации:

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

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

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

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

5. Разработан новый метод построения структурированных программ потоков данных на основе специально разработанной модели языка Денниса и доказана универсальность этого метода.

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

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

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

Заключение

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

Список литературы диссертационного исследования доктор физико-математических наук Соколов, Валерий Анатольевич, 2006 год

1. Алагич С., Арбиб М. Проектирование корректных структурированных программ. М.: Радио и связь, 1984 - 264 с.

2. Алексеев И.В., Соколов В.А. Протокол TCP с адаптацией скорости // Моделирование и анализ информационных систем. 1999, т. 6, № 1. С. 4-11.3J Алексеев И.В. Интегрированные услуги нового поколения Internet. // Сети, № 10, 1999. С. 102-108.

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

4. Ахо А., Ульман Дж. Теория синтаксического анализа, перевода и компиляции. Том 1. Синтаксический анализ. М.: Мир, 1978.6J Ачасова С.М., Бандман O.JL Корректность параллельных вычислительных процессов. Новосибирск: Наука. 1990. - 253 с.

5. Бадин Н.М., Бродский Г.М. Об одном подходе к рекурсивно-параллельному программированию // Разработка, моделирование и оптимизация сложных информационных систем. Ярославль: Яросл. гос. ун-т., 1993. С. 14-19.

6. Бадин Н.М., Бродский Г.М., Соколов В.А. О последовательных шаблонах в технологии рекурсивно-параллельного программирования // Сб. трудов XI-ой Международной конференции «Проблемы теоретической кибернетики». Ульяновск: 1996. С. 14-15.

7. Бадин Н.М., Бродский Г.М., Соколов В.А. Языковые средства рекурсивно-параллельного программирования // Сб. научных трудов «Актуальные проблемы современной математики», т.З. Новосибирск: НИИ МИОО, 1997. С. 19-28.

8. Бердж В. Методы рекурсивного программирования. М.: Машиностроение, 1983 - 248 с.

9. Борщев А.В., Карпов Ю.Г., Рудаков В.В. О корректности параллельных алгоритмов // Программирование, N 4, 1996. С. 5-17.

10. Валях Е. Последовательно-параллельные вычисления. М.: Мир, 1985. - 456 с.

11. Васильчиков В.В., Емелин В.П. Рекурсивно-параллельное программирование для вычислительных систем с динамическим распараллеливанием. Ярославль: Яросл. гос. ун-т., 1992. - 32 с.

12. Грис Д. Наука программирования. М.: Мир, 1984. - 416 с.

13. Дал У., Дейкстра Э., Хоор К. Структурное программирование. М.: Мир, 1975.- 247 с.

14. Дейкстра Э. Дисциплина программирования. М.: Мир, 1978.

15. Карпов Ю.Г. Теория автоматов. СПб.: Питер, 2003. - 208 с.

16. Карпов Ю. Г. Формальное описание и верификация протоколов на основе CSS // Автоматика и вычислительная техника. Рига, 1986. - № 6. - С.21-30.

17. Китаев М.Ю., Рыков В.В. Система обслуживания с ветвящимися потоками вторичных требований // Автоматика и телемеханика. -1980, № 9. С. 52-61.

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

19. Котов В.Е. Сети Петри. М.: Наука, 1984.

20. Кузьмин Е.В., Соколов В.А. Взаимодействующие раскрашивающие процессы // Моделирование и анализ информационных систем, т. 11 (2), 2004. С. 8-17.

21. Кузьмин Е.В. О разрешимости задачи проверки модели для автоматной логики и вполне структурированных систем переходов автоматного типа // Моделирование и анализ информационных систем, т. 11 (1), 2004. С. 8-17.

22. Кузьмин Е.В., Соколов В.А. Проверка свойств вполне структурированных моделей // Мат. Всероссийской научной конференции, посвященной 200-летию Ярославского государственного университета им. П.Г. Демидова. Ярославль: ЯрГУ, 2003. С. 50-54.

23. Кузьмин Е.В. Недетерминированные счетчиковые машины // Моделирование и анализ информационных систем, т. 10 (2), 2003. С. 41-49.

24. Кузьмин Е.В. О разрешимости задачи проверки модели для модального /i-исчисления и некоторых классов вполне структурированных систем переходов // Моделирование и анализ информационных систем, т. 10 (1), 2003. С. 50-55.

25. Кузьмин Е.В. Верификация графов потоков данных с использованием символьной проверки модели для CTL // Моделирование и анализ информационных систем, т. 8 (1), 2001. С. 38-43.

26. Кузьмин Е.В., Соколов В.А. Вполне структурированные системы помеченных переходов. Монография. М.: ФИЗМАТЛИТ, 2005,176 с.

27. Кузьмин Е.В., Соколов В.А. Структурированные системы переходов. Монография. М.: ФИЗМАТЛИТ, 2006, 178 с.

28. Куратовский К., Мостовский А. Теория множеств. М.: Мир, 1970.

29. Кушнаренко О.В., Соколов В.А. Рекурсивно-параллельное программирование и сети Петри: моделирование, анализ и верификация программ // Сб. научных трудов «Моделирование и анализ информационных систем», т. 2. Ярославль: ЯрГУ, 1994. С. 91-97.

30. Кушнаренко О.Б., Соколов В.А. Анализ семантических свойств одного класса рекурсивно-параллельных программ // Сб. тезисов докладов IV-й Международной конференции по прикладной логике. -Иркутск: ИГУ, 1995. С. 72-73.

31. Лингер Р., Миллс X., Уитт Б. Теория и практика структурного программирования. М.: Мир, 1982. - 406 с.

32. Ломазова И.А. Вложенные сети Петри: моделирование и анализ распределенных систем с объектной структурой. М.: Научный мир, 2004, 208 с.

33. Майерс Г. Архитектура современных ЭВМ. М.: Мир, 1985. - 312с.

34. Мальцев А.И. Алгоритмы и рекурсивные функции. М.: Наука, 1965.

35. Матиясевич Ю.В. Диофантовость перечислимых множеств. ДАН, 1970, 191, №2. С. 279-282.

36. Минский М. Вычисления и автоматы. М.: Мир, 1971.

37. Непомнящий В.А. Практические методы верификации программ // Кибернетика, №2, 1984. С. 21-28, 43.

38. Питерсон Дж. Теория сетей Петри и моделирование систем. М.: Мир, 1984. - 263 с.

39. Рубцова Э. Е., Сидорова Н. С. Символьный анализ достижимости в программах потоков данных со структурами данных. // Моделирование и анализ информационных систем, Вып. 5, Ярославль, 1998. С.27-40.

40. Рубцова Э.Е., Соколов В.А. Модели и свойства класса структурированных программ в языках потоков данных // Сб. научных трудов «Моделирование и анализ информационных систем», т. 3. Ярославль: ЯрГУ, 1996. С. 127-157.

41. Соколов В.А. Об одной задаче в классе вычислимых функций с операцией суперпозиции // «Вестник Ярославского университета», № 9. Ярославль: ЯрГУ, 1975. С. 111-114.

42. Соколов В.А. Вычисление частично рекурсивных функций сетями Петри // Сб. научных трудов «Модели и алгоритмы математического обеспечения вычислительных систем». Ярославль: ЯрГУ, 1986. С. 100-105.

43. Соколов В.А. О проблеме достижимости в графах потоков данных с очередями и стеками // Вестник Костромского гос. ун-та им. Н.А. Некрасова. 2003. Спец. выпуск № 2. С. 4-12.

44. Соколов В.А., Тимофеев Е.А., Чалый Д.Ю. Моделирование, оптимизация и верификация транспортных протоколов // Труды 1-ой Всероссийской научной конференции «Методы и средства обработки информации» МСО-2003. Москва: МГУ, 2003. С. 254-259.

45. Соколов В.А., Солопов А.Г. Разработка инструментальных средств моделирования систем на основе одного класса сетей Петри высокого уровня // Вестник компьютерных и информационных технологий. М.: Машиностроение, 2005. № 6. С. 48-53.

46. Соколов В.А. Обоснование выбора и анализ моделей управления передачей информации в сетях // Вестник компьютерных и информационных технологий. М.: Машиностроение, 2005. № 7. С. 30-36.

47. Соколов В.А. Модификация транспортного протокола TCP с использованием метода динамических приоритетов // Вестник компьютерных и информационных технологий, № 4. М.: Машиностроение, 2006.

48. Тимофеев Е.А. Вероятностно-разделительная дисциплина обслуживания и многогранник средних времен ожидания в системе GI/Gn/1 // Автоматика и телемеханика. 1991, № 10. С. 121-125.

49. Тимофеев Е.А. Оптимизация средних длин очередей в системе обслуживания с ветвящимися потоками вторичных требований // Автоматика и телемеханика. 1995, № 3. С. 60-67.

50. Хоар Ч. Взаимодействующие последовательные процессы: Пер. с англ. М.: Мир, 1989. - 264 с.

51. Хопкрофт Д., Мотвани Р., Ульман Д. Введение в теорию автоматов, языков и вычислений. 2-е изд.: Пер. с англ. М.: «Вильяме», 2002, 528 с.

52. Abdulla P.A., Cerans К., Jonsson В., Yih-Kuen Т. General decidability theorems for infinite-state systems // Proc. 11th IEEE Symp. Logic in Computer Science (LICS'96), 1996. P. 313-321.

53. Abdulla P.A., Cerans K., Jonsson В., Yih-Kuen T. Algorithmic analysis of programs with well quasi-ordered domains // Information and Computation, 1997.

54. Abdulla P., Bouajjani A., Jonsson B. On-the-fly Analysis of Systems with Unbounded, Lossy Fifo Channels // Proc. 10th Intern. Conf. on Computer Aided Verification (CAV'98). LNCS 1427, 1998.

55. Agnelli S., Dewhurst V. LAN Interconnection via ATM Satellite Links for CAD Applications: The UNOM Experiment //Proceedings of IEEE ICC, June 1996

56. Abdulla P., Jonsson B. Verifying Programs with Unreliable Channels // Proc. Logic in Сотр. Science (LICS'93), 1993. P. 160-170.

57. Abdulla P., Jonsson B. Undecidable verification problems for programs with unreliable channels // Information and Computation, 130(1), 1996. P. 71-90.

58. Alekseev I.V., Sokolov V.A. Compensation Mechanism for Adaptive Rate TCP // Proceedings of the First IEEE / Popov workshop on Internet Technologies and Services, v. 2. Moscow, 1999. P. 68-75.

59. Alekseev I.V. Model and Analysis of Transmission Protocol ARTCP // Investigation in Russia. 2000, № 27. C. 395-404. (http://zhurnal.ape.relarn.ru/articles/2000/027.pdf).

60. Alekseev, I.V., Sokolov, V.A. ARTCP: Efficient Algorithm of Transport Protocol for Packet Switched Networks // LNCS № 2127, Berlin: Springer-Verlag, 2001. P. 159 174.

61. Alekseev, I.V., Sokolov, V.A. Modeling and Traffic Analysis of the Adaptive Rate Transport Protocol // Future Generation Computer Systems, Vol.18, № 6, North-Holland: Elsevier, 2002. P. 813-827.

62. Allman M., Hayes С., Kruse H., Ostermann S. TCP Performance Over Satellite Links //Proceedings of the 5th International Conference on Telecommunication Systems, March 1997

63. Allman M., Paxson V., Stevens W. TCP Congestion Control. RFC2581, 1999.

64. Allman M., Balakrishnan H., Floyd S. Enhancing TCP's Loss Recovery Using Limited Transmit. RFC3042, 2001.

65. Alur R., Kannan S., Yannakakis M. Communicating hierarchical automata // ICALP'99, Springer LNCS 1644, 1999. P. 169-178.

66. Alur R., Courcoubetis C., Dill D. Model-checking for real-time systems // Proc. 5t/l IEEE Int. Symp. on Logic in Computer Science, Philadelphia, 1990. P. 414-425.

67. Araki Т., Kasami T. Some decision problems related to the reachability problem for Petri nets // Theoretical Computer Science, 3(1), 1977. P. 85-104.

68. Bajaj S., Breslau L., Estrin D., Fall K., Floyd S. Improving Simulation for Network Research // Technical Report 99-702. University of Southern California, 1999.

69. Bakre A., Badrinath R., I-TCP: Indirect TCP for Mobile Hosts //Proceedings of the 15th International Conference on Distributed Computing Systems (ICDCS), May 1995

70. Balakrishnan H., Padmanabhan V.,Seshan S., Katz R. A comparison of Mechanisims for Improving TCP Performance over Wireless Links //ACM SIGCOMM, August 1996

71. Balakrishnan H., Padmanabhan V., Katz R. The Effects of Asymmetry on TCP Performance //ACM MobiCom, September 1997, v.9.

72. Bouajjani A., Esparza J., Mayer O. Reachability Analysis of Pushdown Automata: Application to Model-Checking. // Concur 97, LNCS 1243, 97.

73. Bouajjani A., Habermehl P. Symbolic reachability analysis of FIFO-channel systems with nonregular sets of configurations // Proc. of ICALP'97, LNCS 1256, 1997.

74. Bouajjani A., Mayr R. Model Checking Lossy Vector Addition Systems // Proc. 16th Intern. Symp. on Theoretical Aspects in Computer Science (STACS'99), LNCS 1563, Trier (Germany), March 1999.

75. Braden R. T. Requirements for Internet Hosts Communication Layers //RFC1122 (STD 3), 01 October, 1989

76. Braden R., Jacobson V., Borman D. TCP Extension for High-Performance //RFC1323, May 1992

77. Brakmo L., O'Malley S., Peterson L. TCP Vegas: New Techniques for Congestion Detection and Avoidance //ACM SIGCOMM, August 1994, v.8. P.24-35.

78. Brakmo L., Peterson L. TCP Vegas: End to End Congestion Avoidance on a Global Internet // IEEE Journal on Selected Areas in Communications, 13(8), 1995.

79. Brakmo L., Peterson L. Performance Problems in BSD4.4 TCP // ACM Computer Communications Review, 25(5), 1995. P. 69-86.

80. Biichi J.R. On a decision method in restricted second order arithmetic // Proc. Int. Congr. Logic, Method and Philos. Sci. 1960, Stanford, 1962. P. 1-12.

81. Burkart 0., Caucal D., Moller F., Steffen B. Verification over Infinite States. Chapter in the Handbook of Process Algebra, J. Bergstra, A. Ponse and S.A. Smolka (editors), Elsevier Publishers, 2001. P. 545-623.

82. Burkart O., Esparza J. More infinite results // Electronic Notes in Theoretical Computer Science, 6, 1996.

83. Bartlett K., Scantlebury R., Wilkinson P. A note on reliable full-duplex transmissions over half duplex lines. // Communications of the ACM, 2 (5), 1983. P. 323-342.

84. Cardelli L., Donahue J., Glassman L., Jordan M., Kalsow В., and Nelson G. // Modula-3 report. Technical report, Dec Systems Research Center, 1989.

85. Сёсё G., Finkel A., Purushothaman Iyer S. Unreliable channel are easier to verify than perfect channels. // Information and Computation, 124 (1), 1995. P. 20-31.

86. Chaly D.Yu., Sokolov V.A. An Extensible Coloured Petri Net Model of a Transport Protocol for Packet Switched Networks // Lecture Notes in Computer Science, № 2763. Berlin: Springer-Verlag, 2003. P. 66-75.

87. Chiu D., Jain R. Analysis of the Increase and Decrease Algorithms for Congestion Avoidance in Computer Networks // Computer Networks and ISDN Systems, v. 17, 1989. P. 1-14.

88. Christensen S., Hirshfeld Y., Moller F. Bisimulation equivalence is decidable for basic parallel processes // Proc. CONCUR'93, LNCS 715, P. 143-157.

89. Clarke E., Grumberg 0., Peled D. Model Checking. The MIT Press, 2001.

90. Clarke E.M., Emerson E.A. Design and synthesis of synchronization skeletons using branching time temporal logic // LNCS 131, 1981. P. 52-71.

91. Comer E. D., Stevens L. D. Internetworking with TCP/IP. Volume II. Prentice Hall. 1994

92. Dam M. Fixpoints of Biichi automata // International Conference on the Foundations of Software Technology and Theoretical Computer Science (FST&TCS), LNCS, vol. 652, 1992. P. 39-50.

93. Daniele M., Giunchiglia F., Vardi M.Y. Improved automata generation for linear temporal logic // Computer-Aided Verification, Proc. 11th Int. Conference, v. 1633, 1999. P. 249-260.

94. Dennis J.B. and van Horn E.C. Programming semantics for multiprogramming computations // Communications of the ACM, 9(3), March 1966. P. 143-155.

95. Dennis J.B. Machines and Models for parallel Computing //International Jourmal of Parallel Programming. 1994. Vol. 22. N 1. P. 47-77

96. Dickson L. E. Finiteness of the odd perfect and primitive abundant numbers with r distinct prime factors I j Amer. Journal Math, 35, 1913. P. 413-422.

97. Dufourd С., Jancar P., Schnoebelen Ph. Boundedness of Reset P/T nets // Proc. ICALP'99, LNCS 1644, Springer, 1999. P. 301-310.

98. Dufourd C., Finkel A., Schnoebelen Ph. Reset nets between decidability and undecidability // Proc. ICALP'98, LNCS 1443, Springer, 1998. P. 103-115.

99. Emerson E.A. Temporal and modal logic j j Handbook of Theoretical Computer Science, v. B, 1990. P. 995-1072.

100. Esparza J. On the decidabilty of model checking for several ^-calculi and Petri nets // Proc. CAAP'94, LNCS 787, 1994. P. 115-129.

101. Esparza J. Decidability of model-checking for infinite-state concurrent systems // Acta Informatica, 34, 1997. P. 85-107.

102. Esparza J., Kiehn A. On the model checking problem for branching time logics and basic parallel processes // Proc. of CAV'95, LNCS 939, Springer-Verlag, 1995. P. 353-366.

103. Fall K. Network Emulation in the Vint/NS Simulator // Proc. of ISCC'99, 1999.

104. Filman Robert E. and Friedman Daniel P. Coordinated Computing. // Tools and Techniques for Distributed Software. McGraw-Hill, 1984.

105. Finkel A. Reduction and covering of infinite reachability trees // Information and Computation, 89(2), 1990. P. 144-179.

106. Finkel A., Schnoebelen Ph. Well-structured transition systems everywhere! // Theoretical Computer Science, 256(1-2), 2001. P. 63-92.

107. Finkel A., Schnoebelen Ph. Fundamental structures in well-structured infinite transition systems // Proc. 3rd Latin American Theoretical Informatics Symposium (LATIN'98), Campinas, Brazil, Apr. 1998, LNCS 1380, Springer, 1998. P. 102-118.

108. Floyd S. Connections with Multiple Congested Gateways in Packet Switched Networks, Part 1: One-Way Traffic // ACM Computer Communications Review, 21 (5), 1991. P. 30-47.

109. Floyd S., Jacobson V. Random Early Detection Gateways for Congestion Avoidance //IEEE/ACM Transactions on Networking, August 1993

110. Floyd S. TCP and Explicit Congestion Notification //ACM Computer Communication Review. V. 24. N. 5. 1994. P. 10-23.

111. Floyd S., Jacobson V. Link-sharing and Resource Man-agement Models for Packet Networks // IEEE/ACM Trans-actions on Networking, Vol. 3 No. 4, 1995. P. 365-386.

112. Gerth R., Peled D., Vardi M.Y., Wolper P. Simple on-the-fly automatic verification of linear temporal logic // Proc. of the 15th Workshop on Protocol Specification, Testing, and Verification, 1995.

113. GinsburgD. ATM: Solutions for Enterprise Internetwork-ing. Addison-Wesley Longman Limited, UK, 1996.

114. Hack M. Decision problems for Petri nets and vector addition systems. Project MAC Memo 59. Cambridge, 1975.

115. Hack M. The equality problem for vector addition systems is un-decidable // Theoretical Computer Science, 2, №1, 1976. P.77-96.

116. Henderson Т., Sahouria E., McCanne S., Katz R. On Improving the Fairness of TCP Congestion Avoidance // Proc. IEEE Globecom '98, 1998.

117. Hennessy M. Algebraic Theory of Processes. MIT Press, 1988.

118. Hennessy M., Milner R. On observing nondeterminism and concurrency. // Lecture Notes in Computer Science, 85 (1980). P. 295-309.

119. Hennessy M., Milner R. Algebraic laws for nondeterminism and concurrency // Journal of Association of Computer Machinery, 32, 1985. P. 137-162.

120. Higman G. Ordering by divisibility in Abstract Algebra // Proc. London Math. Soc., 3(2), 1952. P. 326-336.

121. Hoare C.A.R. Communicating sequential processes. // Communications of the ACM, 21 (8), August 1978. P. 666-677.

122. Hoare C.A.R. Communicating sequential processes. Prentice-Hall, 1985.

123. Holzmann G.J. A Theory for Protocol Validation // IEEE Transactions on Computers. Vol. C-31, JN'«8, 1982. P. 730-738.

124. Holzmann G.J. Tracing Protocols // AT&T Technical Journal. Vol. 64, 1985. P. 2413-2434.

125. Holzmann G.J.Design and Validation of Computer Protocols. Prentice Hall, New Jersey, 1991.

126. Hopcroft J.E., Ullman J.D. Introduction to Automata Theory, Languages and Computation. Addison Wesley, 1979.

127. ISO. Data communications HDLC procedures - elements of procedures. Technical Report ISO 4335, International Standards Organization, Geneva, Switzerland, 1979.

128. Jacobson V. Congestion Avoidance and Control //ACM SIGCOMM-88, August 1988

129. Jensen K. Coloured Petri Nets // Vol.1. Eatcs Monographs on TCS, Springer-Verlag, 1994.

130. Karn P., Partridge C. Round Trip Time Estimation //ACM SIGCOMM-87, August 1987

131. Karp R.M. and Miller R.E. Parallel program schemata. Journal of Computer and System Sciences, 3 (2), 1969. P.147-195.

132. Keshav S., Sharma R. Issues and Trends in Router Design // Department of computer science, Cornell University, 1998.

133. Keller R.M. Parallel program schemata and maximal parallelism. Journal of the ACM, 20 (3/4), 1973. P.514-537 and 696-710.

134. Kotov V. Program Scheme Theory. Nauka, Moscow, 1991.

135. Kouzmin E.V., Shilov N.V., Sokolov V.A. Model Checking ^-Calculus in Well-Structured Transition Systems // Proc. 11th Int. Symposium on Temporal Representation and Reasoning TIME-2004, Tatihou, France, IEEE Press, 2004. P. 152-155.

136. Kouzmin E.V., Shilov N.V., Sokolov V.A. Model Checking ^-Calculus in Well-Structured Transition Systems // Joint Bulletin of NCC & IIS, Сотр. Science, Novosibirsk, JY« 20, 2004. P. 49-59.

137. Кузьмин Е.В., Соколов В.А. Исследование свойств класса вполне структурированных систем переходов // Труды П-ой Всероссийской научной конференции «Методы и средства обработки информации» МСО-2005. Москва: МГУ, 2005. С. 399-393.

138. Kouchnarenko О., Schnoebelen Ph. A model for recursive-parallel programs // Proc. 1st Int. Workshop on Verification of Infinite State Systems (INFINITY'96), Pisa, Italy, Aug. 1996, vol. 5 of Electronic Notes in Theor. Сотр. Sci. Elsevier, 1997.

139. Kozen D. Results on the propositional /^-calculus // Theoret. Comput. Sci. 27 (1983). P. 242-272.

140. Larsen K. Proof systems for satisfiability in Hennesy-Milner logic with recursion // Theoret. Comput. Sci. 72 (1990). P. 265-288.

141. Lee Ben, Hurson A.R. Issues in Dataflow Computing //Advaces in computers. 1993. Vol.37. P. 285-333.

142. Mamatov Y., Vasilchikov V., Volchenkov S., and Kurchidis V. Multiprocessor computer system with dynamic parallelism. // Technical Report 7160, VINITI, Moscow, Russia, September 1988.

143. May D.OCCAM. SIGPLAN Notices, 13(4), April 1983.

144. Mayr R. Lossy counter machines. Tech. Report TUM-I9827, Institut fur Informatik, TUM, Munich, Germany, October 1998.

145. Mayr R. Decidability and complexity of model checking problems for infinite-state systems. Technischen Universitat Munchen, dissertation, 1998.

146. Milner R. A Calculus of Communicating Systems // LNCS 92, Springer-Verlag, 1980.

147. Milner R. Communication and Concurrency. Prentice Hall Int., 1989.

148. Minsky M. Computation: Finite and Infinite Machines. Prentice-Hall, 1967.

149. Mogul J. DEC-PKT-4 //http://town.hall.org/Archives/pub/ITA/ html/contrib/DEC-PKT.html

150. Moller F. Infinite results // Proc. CONCUR'96, LNCS 1119, 1996. P. 195-216.

151. Moller F., Birtwistle. Logic for Concurrency // LNCS 1043, 1996.

152. Morris R. TCP Behavior with Many Flows //Proc. of the 5-th IEEE International Conference on network protocols, October 1997

153. Mosses. P.D. Denotational semantics. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, vol. B, chapter 11, Elsevier Science Publishers, 1990. P.575-631.

154. Nicoll C. Overview: Multiservice Networking // Packet. Cisco Systems Inc, 1999.

155. Padhye J., Firoiu V., Towsley Т., Kurose J. Modeling TCP Throughput: A Simple Model and its Empirical Validation //ACM SIGCOMM'98, August 1998

156. Panov S. Programming Particularities for Recursive Computer System. IPVT RAN, Yaroslavl, Russia, 1989.

157. Peterson J.L. Petri Net Theory and the Modeling of Systems. Prentice-Hall Int., 1981.

158. Plotkin G.D. A structural approach to operational semantics. Lect. Notes, Aarhus University, Aarhus, DK, 1981.

159. Podlovchenko R. Recursive programs and hierarchy of their models. Programming, (6), 1991. P.44-52.

160. Pnueli A. The temporal logic of programs // FOCS'77, IEEE, 1977.

161. Postel J. Transmission Control Protocol //RFC793 (STD7), 1981

162. Pratt V. A decidable y.-calculus // Proceedings of 22nd FOCS (1981). P. 421-427.

163. Rabinovich A., Trakhtenbrot B.A. Nets of processes and data flow //Lecture Notes in Computer Science., 1988, Vol.354. P. 574-602.

164. Raymond Cote. Prograph CPX: Purely Visual //Byte. N1.1995. P.179-182.

165. Riedi R., Willinger W. Towards an Improved Understanding of Network Traffic Dynamics // Preprint chapter from the book «Self-similar Network Traffic and Performance Evaluation», 1999.

166. Ritchie D.M. and Thompson K. The unix timesharing system. // Communications of the ACM, 17(7), July 1974. P.365-375.

167. Roubtsova Е. Е., Sokolov V. A. A Model for Reachability Analysis of Data-Flow Graph with Queues and Stacks. // Моделирование и анализ информационных систем, т.6 (1), Ярославль, 1999. С. 50-57.

168. Schildt Н. С: the Complete Reference // McGraw-Hill, Berkeley CA. Second Edition, 1987.

169. Shepard T. TCP Packet Trace Analysis // Masters of Science Thesis. Massachusetts institute of Technology, MIT/LCS/TR-494, 1991.

170. Shilov N.V., Yi K. Puzzles for Learning Model Checking, Model Checking for Programming Puzzles, Puzzles for Testing Model Checkers // Electr. Notes Theor. Comput. Sci. 43, 2001.

171. Shilov N.V., Yi K. On Expressive and Model Checking Power of Propositional Program Logics // Ershov Memorial Conference, 2001. P. 39-46.

172. Shilov N.V., Yi К. How to find a coin: prepositional program logics made easy // Bulletin of the European Association for Theoretical Computer Science, v.75, 2001. P. 127-151.

173. Shilov N.V. Program Schemata vs. Automata for Decidability of Program Logics // Theor. Comput. Sci. 175(1), 1997. P. 15-27.

174. Sokolov V.A., Roubtsova E.E., Roubtsov S.A. On a Technology of Design and Analysis of Dataflow Programs // Lecture Notes in Computer Sciences, № 1277. Berlin: Springer-Verlag, 1997. P. 115-120.

175. Sokolov V.A., Timofeev E.A. Dynamical Priorities without Time Measurements and Modification of the TCP // LNCS, № 2244, Berlin: Springer-Verlag, 2001. P. 240-245.

176. Sokolov V.A., Timofeev E.A. An Approach to the Implementation of the Dynamical Priorities Method // Lecture Notes in Computer Sciences, № 3606. Berlin: Springer-Verlag, 2005. P. 74-78.

177. Somenzi F., Bloem R. Efficient Biichi automata from LTL formulae // Computer-Aided Verification, Proc. 12th Intern. Conference, v. 1633, 2000. P. 247-263.

178. Steffen B. Characteristic formulae // Proc. ICALP (1989).

179. Stevens W.R. TCP/IP Illustrated. Volume 1: The Protocols. Addison-Wesley. 1994

180. Stirling C. P. Temporal logics for CCS. Proc. of REX Workshop, 1988.

181. Stirling C. P. Modal and temporal logics // Handbook of Logic in Computer Science, v. 2, Oxford University Press, 1992. P. 477-563.

182. Stirling C. P. Modal and temporal logics for processes // LNCS 1043, 1996, P. 149-237.

183. Stirling C., Walker D. Local model checking in the modal /i-calculus // Theoretical Computer Science, 89 (1991), P. 161-177.

184. Stoy J.E. Denotational Semantics: The Scott-Stratchey Approach to Programming Language. MIT Press, 1977.

185. Stroustrup B. The С++ Programming Language. Addison-Wesley, Third Edition, 1997.

186. Taqqu M., Teverovsky V., Willinger W. Is network traffic self-similar or multifractal? // Fractals, n. 5, 1997. P. 63-73.

187. Tanenbaum A. Computer networks. Prentice Hall. 1996

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

189. Vardi M.Y, An automata-theoretic approach to linear temporal logic // Logics for Concurrency, LNCS 1043, 1996. P. 238-266.

190. Vardi M.Y., Wolper P. Reasoning about infinite computations // Information and Computation, 115(1), 1994. P. 1-37.

191. Vardi M.Y., Wolper P. An automata-theoretic approach to automatic program verification // Proc. of the First Symposium on Logic in Computer Science, 1986. P. 322-331.

192. Vasilchikov V., Emielyn V., Kurchidis V., and Mamatov Y. Recursive-parallel programming and work in RPMSHELL. IPVT RSN, Yaroslavl, Russia, 1994.

193. Volchenkov S., Krichmara A., Tcikunov A. Programming particularities for recursive computer system on some problem examples. //In Computer Systems and their models, Yaroslavl, Russia, 1990.

194. Wakeman I., Ghosh A., Crowcroft J., Jacobson V., Floyd S. Implementing Real Time Packet Forwarding Policies using Streams // Usenix 1995 Technical Conference, 1995.

195. Wirth N. Moduala-2. // Technical Report 36, Institut for Informarik ETN, December 1978.

196. Wolper P. Temporal logic can be more expressive // Information and Control, 56, 1983.

197. Wolper P., Vardi M.Y., Sistla A.P. Reasoning about infinite computation paths // Proc. 24th IEEE Symposium on Foundations of Computer Science, 1983. P. 185-194.