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

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

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

МОДЕЛИРОВАНИЕ РАСПРЕДЕЛЕННЫХ СИСТЕМ И АНАЛИЗ ИХ СЕМАНТИЧЕСКИХ СБОЙСТБ

Специальность 01.01.09 - Дискретная математика и математическая кибернетика

АВТОРЕФЕРАТ

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

Ярославль - 2006

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

Официальные оппоненты:

доктор физико-математических наук, профессор Ломазова Ирина Александровна;

доктор технических наук, профессор Вагин Вадим Николаевич;

доктор технических наук, профессор Малышкин Виктор Эммануилович.

Ведущая организация - Московский государственный университет

имени М. В. Ломоносова, факультет вычислительной математики и кибернетики.

Защита диссертации состоится 28 апреля 2006 года в ¿¿часовМ минут на заседании диссертационного совета Д 212.002.03 в Ярославском государственном университете имени П. Г. Демидова по адресу: г. Ярославль, ул. Союзная, 141.

С диссертацией можно ознакомиться в библиотеке Ярославского государственного университета имени П.Г. Демидова по адресу: г. Ярославль, ул. Полушкина роща, 1.

Автореферат разослан " ХУ» г.

Ученый секретарь

диссертационного совета . . к. ф.-м. н., доцент

Д 212.002.03 Яблокова С. И.

ОБЩАЯ ХАРАКТЕРИСТИКА РАБОТЫ

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

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

При исследовании сложных систем зачастую приходится строить формальные модели, которые представляют собой системы переходов с бесконечным числом состояний. В этом случае многие средства анализа и верификации, производящие полный перебор пространства состояний, становятся неприменимыми. Тем не менее, для некоторых ограниченных классов систем с бесконечным числом состояний разными авторами были разработаны достаточно эффективные методы верификации (как, • например, в работах P. Abdulla, К. terans1, A. Finkel, В. Jonssori, F. Moller2, Ph. Schnoebelen3). В частности, оказалось, что метод проверки модели (Model Checking), широко используемый при автоматической верификации систем с конечным числом состояний, может быть применим для некоторых классов систем с бесконечным числом состояний и

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

2 Moller F. Infinite results // Proc. CONCUR'96, LNCS 1119. - 1996. - 1M 95-216.

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

подмножеств темпоральных логик. Примерами формальных моделей, являющихся системами переходов с бесконечным числом состояний и позволяющих описывать параллельные и распределённые системы, являются магазинные автоматы"1, сети Петри5, ВРР (Basic Parallel Processes)*, LCS (Lossy Channel Systems — системы с каналами, теряющими сообщения)7, Real-Time Automata (автоматы реального времени)8 и др.

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

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

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

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

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

6 Christcnsen S., Hirshfeld Y., Moller F. Bisimulation equivalence is decidable for basic parallel processes II Proc. CONCUR'93, LNCS 715. - 1993. - P. 143-157.

7 Abdulla P., Jonsson B. Verifying Programs with Unreliable Channels // Proc. Logic in

Сотр. Science (LICS'93). - 1993. - P. 160-170.

Abdulla P., Jonsson B. Undecidable vérification problems for programs with unreliable channels // Information and Computation. - 1996. - 130(1 ). - P. 71 -90. Î^Alur R., Courcoubetis C., Dill D. Model-checking for real-time systems II Proc. 5lh IEEE Int. Symp. on Logic in Computer Science, Philadelphia. - 1990. - P. 414-425. ® Кларк Э.М. мл., Грамберг О., Пелед Д. Верификация моделей программ: Model Checking. Пер. с англ. / Под ред. Р. Смелянского. - М.: Изд-во МЦНМО, 2002. - 416 с.

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

Хопкрофт Д., Мотвани P., Ульман Д. Введение в теорию автоматов, языков и вычислений. 2-е изд.: Пер. с англ. - М,: Вильяме, 2002. - 528 с. Карпов Ю. Г. Теория автоматов. - СПб.: Питер, 2003. - 208 с.

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

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

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

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

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

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

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

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

Ранее в ряде публикаций таких авторов, как A. Bouajjani и R. Мауг1г, О. Burkart13, J. Esparza11, Л. Kiehn'5, исследовались вопросы

13 Bouajjani A., Mayr R. Model Checking Lossy Vcctor Addition Systems // Proc. 16th Intern. Symp. on Theoretical Aspects inComputer Science (STACS'99), LNCS 1563. - 1999.

13 Burkart O., lisparza J. More infinite results // Electronic Notes in Theoretical Computer Scicnce. - 1996. — 6.

разрешимости задачи проверки модели для некоторых конкретных представителей класса вполне структурированных систем переходов, а именно магазинных автоматов, сетей Петри, ВРР, LVAS (Lossy Vector Addition Systems) и различных темпоральных логик линейного времени и ветвящегося времени. Мы в нашей работе исходим из позиции обобщения и акцентируем внимание на проблеме разрешимости темпоральных свойств для различных классов вполне структурированных систем помеченных переходов, в частности для класса вполне структурированных систем переходов автоматного типа, которые из-за своей специфической структуры можно также отнести и к классу систем переходов, независимых отданных16.

Внимание исследователей практически обходит системы переходов, независимые от данных (за исключением систем переходов с конечным числом состояний). Тем не менее, системы, принадлежащие к этому классу, могут быть достаточно выразительными и нетривиальными. Для демонстрации этого факта в диссертации представлен специальный фрагмент алгебры процессов, построенный на основе таких хорошо известных алгебр процессов, как CCS (Calculus of Communicating Systems — исчисление взаимодействующих систем) Милнера17 н SCP (Communicating Sequential Processes — взаимодействующие последовательные процессы) Хоара18, позволяющий строить формальные модели (параллельных и распределённых систем), которые могут быть рассмотрены как независимые от данных помеченные системы переходов, а точнее, как вполне структурированные системы переходов автоматного типа. В качестве примера конкретной реализации этого фрагмента представлен формализм, который называется «взаимодействующие раскрашивающие процессы» (ССР — Communicating Colouring Processes)16, позволяющий строить модели распределённых систем, где поведение каждого компонента описывается последовательным процессом и между ними организовано взаимодействие, направленное на обмен и передачу пакетов информации. Формализм ССР принимает во внимание факт передачи данных, а также позволяет отслеживать перемещение данных различного типа между компонентами системы. Но переход из одного состояния в другое не зависит от оперируемых данных, а

14 Esparza J. Decidability of model-checking for infinite-state concurrent systems // Acta Informatica. 1997. - 34. — P. 857.

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

16 Кузьмин E.B., Соколов 13.A. Вполне структурированные системы помеченных переходов. - М.: ФИЗМАТЛИТ, 2005. - 176 с.

17 Milner R. Communication and Concurrency. - Prentice Hall, 1989.

18 Iloarc C. A. R. Communicating sequential processes. - Prentice-IIall, 1985.

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

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

Разработка языков потоков данных была начата более двадцати лет назад в работах Д. Денниса29, а в 1995 г. на рынке программного обеспечения появился первый широко доступный язык потоков данных: язык Prograph фирмы Piclorius Incorporated21.

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

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

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

Dennis J.B. Machines and Models for Parallel Computing // International Journal of Parallel Programming. - 1994. - Vol. 22, № 1. - P. 47-77.

21 Cote Raymond. PrographCPX: Purely Visual//Byte.- 1995. — Ks l.-P. 179-182.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

27 Postel J. Transmission Control Protocol. - RFC793 (STD7), 1980.

28 Jacobson V., Braden R., Borman D. TCP Extensions for High Performance. - Rl'C 1323, 1992.

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

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

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

Одно из главных преимуществ алгоритма управления потоком ARTCP состоит в том, что он не использует потерю сегмента как индикатор перегрузки сети. В работах И.В. Алексеева и В.Л. Соколова34 была показана эффективность работы алгоритма управления потоком ARTCP по сравнению со стандартным алгоритмом управления потоком.

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

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

Mathis M., Mahdavi J., Floyd S., Romanow A. TCP Selective Acknowledgement Option. -RFC2018, 1996.

29 Alckseev I.V., Sokolov V.A. ARTCP: Efficient Algorithm for Transport Protocol for Packet Switched Networks // LNCS 2127. - Springer-Verlag, 2001. - P. 159-174.

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

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: El sevier, 2002. - P. 813-827.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Основные научные результаты, выносимые на защиту:

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

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

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

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

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

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

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

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

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

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

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

- ИНТАС-РФФИ (грант 95-0378);

- РФФИ (гранты 94-01-01431; 97-01-00144; 99-01-00309; 03-01-00804);

- Министерства образования РФ по фундаментальным проблемам математики (1996-1997 и 1998-1999);

- Министерства образования РФ по фундаментальным проблемам технической кибернетики (1996-1997 и 1998-1999);

- ФЦП «Интеграция», "Ярославский объединенный учебно-научный центр информатики, электроники и телекоммуникации", проект № А0068 (1998-2001);

- издательский грант РФФИ 05-07-95008.

Кроме того, результаты, полученные в диссертации, используются в учебном процессе на факультете информатики и вычислительной техники Ярославского государственного университета им. П.Г. Демидова при преподавании дисциплин: «Верификация программ», «Модели

распределенных систем», «Теория вычислительных процессов и структур». Они также положены в основу трех монографий [1-3] и двух учебных пособий для студентов вузов с грифом УМО по классическому университетскому образованию РФ (2006 г.).

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

• 1-ая (Москва, 2003 г.) и II-ая (Москва, 2005 г.) всероссийские научные конференции «Методы и средства обработки информации» (МСО);

• XI Международный симпозиум "Temporal Representation and Reasoning" (TIME-2004). - France, 2004 г.;

• IV-ая (Ярославль, 1997 г.), VI-ая (Новосибирск, 2001 г.), VII-ая (Нижний Новгород, 2003 г.) и VIII-ая (Красноярск, 2005 г.) международные конференции "Параллельные компьютерные технологии" (РаСТ);

• Рабочее совещание "Распределенные информационно-вычислительные ресурсы и математическое моделирование" Международной конференции по вычислительной математике (МКВМ-2004). -11овосибирск, 2004 г.;

• Международный семинар "Program Understanding-2003", Salcllite Workshop of Fifth International Conference «Perspectives of System Informatics» (PS1-2003). - Новосибирск, 2003 г.;

• IV Международная конференция «Perspectives of System Informatics» (PSI-2001).- Новосибирск, 2001 г.;

• Международный семинар "First IEEE Popov Workshop ort Internet Technologies and Services". -Москва, 2000 г.;

• III Международный конгресс по прикладной и индустриальной математике (ИНПРИМ-98). — Новосибирск, 1998 г.;

• XI Международная конференция "Проблемы теоретической кибернетики".—Ульяновск, 1996 г.;

• IV Международная конференция по прикладной логике. — Иркутск, 1995 г.;

• X Международная конференция по проблемам теоретической кибернетики. - Саратов, 1993 г.;

• III Международная конференция по алгебре памяти М.И. Каргаполова. — Красноярск, 1993 г.;

• Всероссийский симпозиум "Математическое моделирование и компьютерные технологии". - Кисловодск, 1997 г.;

• II Всесоюзная конференция по прикладной логике. - Новосибирск, 1988 г.;

• VIH Всесоюзный семинар "Параллельное программирование и высокопроизводительные структуры". — Киев, 1988 г.;

• XIV Всесоюзная алгебраическая конференция. — Новосибирск,1977;

• III Всесоюзная конференция по теоретической кибернетике. -Новосибирск, 1974 г.

Полученные в диссертации результаты обсуждались также на научном семинаре "Моделирование и анализ информационных систем" факультета информатики и вычислительной техники Ярославского государственного университета им. П.Г. Демидова.

СТРУКТУРА И СОДЕРЖАНИЕ ДИССЕРТАЦИИ

Диссертационная работа состоит из введения, шести глав, заключения и приложения. Общий объем диссертации 318 с., основной текст — 262 е., приложение — 56 е., библиографический список — 207 наименований. Работа содержит 85 рисунков и 1 таблицу.

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

В начале первой главы приводятся предварительные сведения, которые используются в дальнейшем. Они, в основном, соответствуют материалу из литературных источников31. Здесь в разделе 1.1 определяются понятия мультимножества, правильных квазипорядков, верхних и нижних конусов и описываются их свойства. Затем в разделе 1.2 приводятся основные понятия теории вполне структурированных систем помеченных переходов, и рассматриваются различные классы вполне структурированных систем переходов как обобщенная модель для широкого класса распределенных систем; для них описываются методы анализа разрешимых семантических свойств.

Система помеченных переходов есть четвёрка LTS = (S, 7",—j0), где S есть множество состояний с элементами sq, s¡, S2, ..., Т — некоторый алфавит пометок (множество имён действий), —> с (SxTxS) — отношение перехода между состояниями, Ja е S— начальное состояние системы.

Последовательное исполнение для LTS есть конечная или бесконечная цепочка переходов so —'-^s/—'■>—>í2—!»—>..., где Sq — начальное состояние, системы.

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

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

Вполне структурированной системой переходов с совместимостью по возрастанию (соответственно, по убыванию) ПТБ называется система переходов 172> = (5, Т, ->, 50), дополненная отношением квазипорядка < с: Л"1 х 5, удовлетворяющим следующим условиям: I) отношение < является правильным квазипорядком; 2) квазипорядок < совместим (по возрастанию) с отношением переходов —», а именно, для любых состояний я, < д, и перехода существует переход с/;—'—х/?, такой что

«г < 42-

(соответственно, квазипорядок < совместим по убыванию с отношением переходов —а именно, для любых состояний Л; < и перехода^/—существует переход я/—такой что ^ < д2).

В этом же разделе определяется новый класс вполне структурированных систем переходов — класс вполне структурированных систем переходов автоматного типа. Для данного класса и класса вполне структурированных систем переходов в целом, исследуется разрешимость темпоральных свойств. В качестве базовых темпоральных логик, с помощью которых выражаются темпоральные свойства систем переходов, используются автоматная логика АЬ, логики СТЬА и 1ЛЬЛ. Элементарные высказывания интерпретируются верхними и нижними конусами.

Вполне структурированная система переходов автоматного типа \УБА - это помеченная система переходов ЬТБ = (5, Г, —$0), дополненная отношением правильного квазипорядка <с5х5, где 5 = £, <2 ~ конечное множество управляющих состояний, £) - конечное или бесконечное множество значений некоторых характеристик, 50 е 5 -начальное состояние,

-> с (5x7x5) такое, что Э ->. £ Ш*Тх()): для любых состояний {д, с!), (</', с1') и некоторой метки перехода Г переход (<?, с1)—с!') существует тогда и только тогда, когда существует переход г/—отношение < определяется так, что (д, с/) <(<?', */') <=> д =д'ч <Л<<1'.

Теорема 1.2.8. Класс вполне структурированных систем переходов с совместимостью по возрастанию и убыванию совпадает с классом вполне структурированных систем переходов автоматного типа.

Далее, в разделе 1.3, приводятся примеры формальных моделей параллельных • и распределённых систем, порождающих вполне структурированные системы переходов рассматриваемых классов: обыкновенные сети Петри и сети Петри с обнуляющими дугами, системы с. ненадёжными каналами, в частности РН'О-канальпые системы с потерями, системы переходов, независимых от данных. Эти формализмы позволяют продемонстрировать ряд абстрактных свойств на конкретных примерах.

В конце главы в качестве конкретной реализации модели систем взаимодействующих процессов, независимых от данных, представлен

новый формализм, названный нами «взаимодействующие раскрашивающие процессы» (ССР — Communicating Colouring Processes), и показана разрешимость для ССР проблем покрытия, субпокрытия, достижимости, неизбежности (и как следствие - проблемы останова). В рамках формализма ССР возможно построение моделей распределённых систем, где поведение каждого компонента описывается последовательным процессом и между ними . организовано взаимодействие, направленное на обмен и передачу пакетов информации. В данной модели мы игнорируем значения передаваемых данных и принимаем в расчёт лишь тип (цвет) данных, определяемый, возможно, типом источника данных и уровнем секретности. Фокусируется внимание на возможности отслеживать перемещение данных различного типа между компонентами системы. В этом аспекте могут рассматриваться вопросы о доставке пакетов данных до адресата и о недопущении передачи конфиденциальных данных в открытую небезопасную среду.

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

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

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

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

С другой стороны, существует много формализмов, таких как машины Тьюринга и счётчиконые машины, сети Петри, системы с ненадёжными каналами (Lossy Channel Systems), которые имеют семантическое расширение и производят манипуляции с данными. Модель в рамках этих формализмов состоит из системы переходов с копечным числом управляющих состояний (управляющая часть), работающая с потенциально бесконечным множеством D значений данных. Состояние такой системы может быть представлено в виде пары (q, d), где q -управляющее состояние, a d е D. Переход в управляющей части имеет метку и операцию над множеством D. Переход возможен лишь в том случае, если будет истинен соответствующий этому переходу некоторый предикат над D (т.е. переход зависит как от управляющих состояний, так и от данных, с которыми производятся манипуляции).

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

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

Предполагаем наличие следующих множеств: Рг - {X, Y, X,,...} -конечное множество имён процессов; Var = fx, у, х/,...} ~ конечное множество переменных; Ghl — fv, V/, .../ - конечное множество капалон; Exp = fe, cj, C2, ■■■} — конечное множество выражений над множеством переменных Var; Actyar = fx ! е, ..„ дг ? у,...} -множество простых действий процессов; Actcм ~ f(v!e, v ? х), (v,! е. V/ ? х),...} - множество взаимодействии между процессами (передача данных через каналы v, V/,...); D = fd, dj, di, ■■■} - бесконечное множество допустимых значений переменных.

Опишем абстрактный синтаксис выражений (для) процессов. Выражения процессов Е, Е',... задаются следующей грамматикой: Е,Е':~0 | XePr | v?x.E | v.'e.E \ Е + Е'\ Е\\Е' Дадим интуитивное представление смысла приведённых выше конструкций. Процесс 0 представляет собой процесс, который не является активным, т.е. никакое действие не может быть выполнено. Процессы v?x.E н v!e.E совершают действия v?x и vie соответственно, а затем продолжаются как процесс Е. Действие v?x означает копирование (присвоение) в переменную Jt значения из v, где в данном случае v может быть как обычной переменной, так и синхронизирующим каналом передачи данных,

т.е. v е Var kj Chi. Действие v/e представляет собой копирование в V е Var U Chi значения выражения е. Вместо е будем также писать е(х i,...jc„). Дня двух процессов Е и Я'оператор суммы даёт процесс Е + Е\ который ведёт себя либо как Е, либо как Я'. Для двух данных процессов Е и Е' параллельная композиция даёг процесс Е || Е', способный выполнять действия Е и Е' параллельно, т.е. либо произвольно чередуя их, либо синхронизируя работу (в случае передачи данных по каналу):

Прогрессом является выражение процесса, переменные которого определены конечным набором рекурсивных уравнений (процессов).

Декларацией npaijccca называется совокупность А рекурсивных уравнений процессов А = {Xt | I <1< п], где и е N„ переменные Л",

все различны, и где выражения Ei используют только те переменные, которые принадлежат множеству Pr(A)=äef {Xt, Более того, если

выражение Et строится с помощью оператора параллельной композиции ||, запретим использование в этом выражении переменной Xt.

Каждая декларация процессов А задаёт систему помеченных переходов: управляющими состояниями в ней являются выражения процессов (в данной семантике их конечное число), построенные на множестве Рг(Д), множество меток задаётся как Act = ActVar и Act сип и отношение переходов определяется с помощью следующих правил вывода.

_ „ _ v*r в . .

a.b. ——> £;-А = Л б Д; —--5-j е /:

X——:«е/}—^Е'

Е—^Е' , Е-2-*Е' F "и >F'

-а е Act и '

Л'|| F—г—»A"|| F """ Е || /■' '""■"1х) >£" || /■"

Последнее правило означает одновременное взаимодействие между процессами, связанное с передачей значения выражения е в переменную х через канал v, т.е. после срабатывания перехода с пометкой а = (v!e, у?л) переменная х становится равной значению выражения е. Если есть процесс вида vle.E (или, соответственно, v?x.E), где v е Chi, е е Ехр, он может перейти в процесс Е тогда и только тогда, когда в параллельной композиции будет процесс vlx.F (соответственно, vle.F), который при одновременном срабатывании перейдёт в F.

Для того, чтобы система переходов, порождаемая декларацией процессов А, была вполне структурированной системой переходов автоматного типа WTA — (S, Т, ->, х0), где Т = Act, необходимо на А наложить ' дополнительные ограничения. Положим, что на множестве D задан правильный квазипорядок <. Далее, нами будут рассматриваться только те

выражения е(х/.....х„) е Ехр, которые представляют собой монотонную

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

< , т.е. для любых двух векторов значений переменных (ddn) < (dl',..., d„') должно выполняться условие e{dd„) £ e(d,',..., d„').

Тогда, состояние s системы IFTA будет представлять собой пару (q, d), где q е Q - это выражение процессов, а d = (с//,...,с/*) -- вектор значений всех переменных (при условии, что переменные некоторым образом упорядочены), к = \Var\. Начальное состояние s<> есть (qo, d0), где qo соответствует выражению процесса X), а do — вектор начальных значений переменных. Из определения декларации процессов А следует, что множество Q конечно. Но множество S системы )УТЛ бесконечное, т.к. векторов значений переменных может быть бесконечно много. Более того, на множестве S можно задать правильный квазипорядок <птл так, что л = (<7,d)<IIT^j'=(g',d') <=> ? = tf'nd<d'.

Далее в этом разделе рассматривается конкретная реализация взаимодействующих процессов, независимых от данных — взаимодействующие раскрашивающие процессы (ССР).

Для этого определяется новое множество 2 типов (или цветов) данных. Описывается тип переменных из Var как мультимножество над 2-Без нарушения условия монотонности задаются допустимые для данного формализма выражения £■(*/,...Гг„).

Итак, выражение e(xi,...rx„) в рамках ССР может быть одного из следующих видов:

е+(х1ух2) = х, + х2; e,j(xlrx:) - х, u х2;

е(.,(д:,) = х, (-) от; en(x,)=xi п т,

е(х,) ~х/\ О, efai) = х/ / С,

где С с а т принадлежит множеству всех возможных мультимножеств над X.

Выражения вида e+(y,z) = у+ z или e,Jy,z) - у vjz моделируют формирование (построение) нового пакета данных из данных других пакетов, находящихся в переменных у и г, который, например, с помощью действия х\е помещается в переменную х

Выражения с,(х) = х \ С, е/(х) — х/ С или е(.)(х) = х (-) т в сочетании с действием х\е(х) могут интерпретироваться как извлечение данных из пакета переменной х.

Выражения v!e(x/,*j) и v?jr означают отправку и приём пакета данных через канал v соответственно.

Оператор о может быть использован для формирования пакета данных определённого формата. Например, последовательность действий г\(х гл от), дг!(--е (-) т), v!z означает передачу пакета данных формата т через канал v; оператор п ограничивает размер передаваемых за' один раз данных.

Таким образом, состояние ССР - это набор (q, тт„), где q — локальное состояние (определяемое декларацией процессов А, пред-

ставляющее собой выражение процессов, a mi,...,mn — мультимножества, являющиеся содержимым соответствующих переменных.

Раскраска (colouring) ССР - это отображение M множества переменных Var на множество всех возможных мультимножеств над

Определим на множестве переменных Var некоторый порядок, т.е. Var = (*/,..,,хД тогда раскраска M - это вектор из мультимножеств Ai = (mi,...,/»„), где V/ (1 < ; < п) пи - М(х,), п = \Var\.

Тогда состояние ССР может быть представлено как (q, Ai).

Исполнение ССР - это последовательность состояний, начинающаяся в начальном состоянии (qo,Mo), где qa представляет собой начальное выражение процесса X/, которая строится в соответствии с правилами переходов.

Каждое срабатывание перехода q—'—*q'переводит ССР из состояния {q, M) в некоторое последующее состояние (q',M% где М' вычисляется в соответствии с выражением, ассоциированным с меткой действия перехода t.

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

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

Счетчиковые машины с потерями были введены R. Mayer в качестве общего средства для демонстрации алгоритмической неразрешимости ряда проблем для систем с потерями, которые используются для моделирования передачи данных через ненадёжные каналы связи, например, проблемы верификации систем с ненадежными очередями (lossy FIFO-channel systems), задачи проверки модели для сетей Петри с потерями, некоторых проблем для сетей Петри с обнуляющими дугами и параметрических проблем таких, как справедливость для протоколов-передачи данных.

Счетчиковые машины с потерями (lossy counter machines), т.е. машины со счётчиками, значения которых могут уменьшаться самопроизвольно в любое время, слабее по выразительной мощности чем машины Тьюринга и могут быть заданы (моделироваться) многими системами.

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

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

Недетерминированная счетчиковая маитна псМ — это набор из

четырёх элементов (£?, {х,.....хт], —>■, Г), где х,- счетчик, Q = {170,..., (¡„} —

конечное множество состояний, qn — начальное состояние, д„ — финальное состояние, Т — конечное множество меток действий, соответствующих выражению над счетчиками, -^c:(Q\qn) хТу. Q- отношение переходов. Переход из одной конфигурации в другую может быть одного из следующих видов (при -£->?'):

.....с(+1,...,ет), если / соответствует

выражению := х> + 1;

(?, с,.....с......с',,...,ст), гдес'( = 0 при с, = 0 и = с, - 1

при с( > 0, если метка ? соответствует выражению х1 := х, (-) 1;

(<7> С/.....с,,..., ст)—ц\с/,..., 0,...,с,„), если Г соответствует

выражению .V/ := 0;

(<7. —'—*( д", с,,...,с'(,...,ст), где с- = с,+ 1 при с, £ 1 и

с'¡-С! при о = 0, если метка перехода / соответствует выражению х, := X/ + тт(ху,1).

Недетерминированная /н-счетчиковая машина псМ рассматривается как помеченная система переходов. Естественным образом задается отношение < правильного квазипорядка на множестве конфигураций машины псМ (т.е., на множестве состояний системы переходов).

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

Теорема 2.4.1. Система переходов (псМ,<) является эффективной но пересечению вполне структурированной системой переходов с

совместимостью по возрастанию и убыванию (автоматного тина), имеющей эффективный предбазис.

Здесь же доказано, что проблемы ограниченности и тотальной ограниченности для недетерминированной четырехсчстчиковой машины неразрешимы (Следствие 2.4.1 и Теорема 2.4.3)

Для недетерминированных счетчиковых машин доказывается неразрешимость проблем включения и эквивалентности (теоремы 2.4.4 и 2.4.5), а также неразрешимость проблемы достижимости для недетерминированной пятисчетчиковой машины и вектора значений счётчиков (с/, с2, сз, с4, а) > (0, 0, 0,0, 0) (Теорема 2.4.7).

В то же время, для недетерминированных счетчиковых машин задача достижимости некоторой нулевой конфигурации (q, 0,...,0) разрешима (Теорема 2.4.6).

В разделе 2.2 аналогичные вопросы рассматриваются для счетчиковых машин с потерями, а в 2.3 - для счетчиковых машин с обнулениями и ошибками проверки на нуль (такие машины моделируются, например, сетями Петри).

В третьей главе исследуется алгоритмическая разрешимость темпоральных свойств систем переходов. Здесь описывается метод проверки модели (Model Cheeking) и приводится ряд темпоральных логик линейного времени (слабая логика линейного времени, LTL) и ветвящегося времени (логика Хсннеси-Милнера, CTL, модальное ц-нсчисление). Вводятся расширения широко известных логик CTL (computation tree logic) и LTL (linear-time logic), которые обозначаются CTLA и LTLA соответственно, позволяющие строить темпоральные формулы с учётом пометок действий систем переходов. Описывается автоматная логика AL, представляющая собой обобщение и расширение логик CTLA и LTLA32.

В качестве базовой темпоральной логики рассматривается автоматная логика AL. Проводится сравнение (по выразительной силе) этой логики с другими приведёнными темпоральными логиками. Затем для рассматриваемых классов вполне структурированных систем переходов устанавливаются разрешимые и неразрешимые темпоральные свойства, т. е. устанавливаются подмножества логик, в частности, подмножества автоматной логики, для которых метод проверки модели (Model Checking) может быть применим, а также неразрешимые подмножества, для которых п общем случае этот метод может оказаться бесполезным.

" Кузьмин Е.В., Соколов В.Л. Г!полни структурированные системы помеченных переходов. - М.: ФИЗМЛТЛИТ, 2005. - 176 с.

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

В данной главе производится сравнение логик по выразительной силе. При этом рассматриваются две задачи:

- локальная проверка модели: для заданной модели (системы переходов) LTS определить истинность формулы темпоральной логики (р в состоянии s, т.е. проверить, выполняется ли s |= <рг,

- глобальная проверка модели: построить множество всех состояний модели LTS, в которых формула <р темпоральной логики является истинной.

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

Далее в этом разделе рассматриваются результаты относительно разрешимости и неразрешимости темпоральных свойств всего класса WS вполне структурированных систем переходов.

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

Четвертая глава посвящена выработке и обоснованию рекомендаций для обеспечения семантической корректности программ в языках потоков данных (Datallow-iiporpaMM)'13.

В ней описан структурный подход к проектированию программ для машин потоков данных.

В рамках этого подхода построен новый класс программ в синтаксисе языков потоков данных — класс структурированных Dataflow-программ, для которого доказана алгоритмическая полнота, а также разработаны семантические модели и критерии корректности программ этого класса.

M Sckolov V.A., Roubtsova li.li., Roubtsov S.A. On a Technology of Design and Analysis of Dataflow Programs // Lecture Notes in Computer Sciences. — Uerlin: Springer-Verlag, 1997. - № 1277.-C. 115-120.

Как н любая другая программа, программа и языке потоков данных может рассматриваться как некоторый оператор, преобразующий входную информацию в выходную. Этот оператор, и свою очередь, может включать в себя совокупность элементарных (базисных) операторов. В качестве таких операторов может быть выбрано семейство операторов языка Денниса34: а) размножителей (сору), Ь) блоков выполнения операций (operator) и блоков принятия решения (predicate), с) вентилей (switch) и d) смесителей (merge). Понятие оператора потоков данных, или DF-оператора, включает п себя структурную модель и модель поведения DF-оператора.

-'/1 V-j и Ц (/

а) Ь) <:) <|)

Рис. 4.1. Базисные операторы языка потоков данных

Структурной моделью О /У'-оператора является помеченный ориентированный граф с вершинами двух типов: операторными вершинами н вершинами данных.

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

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

Вершина данных может иметь не более одной входящей дуги и не более одной выходящей дуги.

Различают информационные и управляющие вершины данных.

Вершина данных, которая не имеет ни одной входящей дуги, называется входом ¿^-оператора. Вершина данных, которая не имеег ни одной выходящей дуги, называется выходом /Э/•'-оператора.

Таким образом, среди вершин данных выделяют п входов и т выходов. Поэтому /^-оператор можно рассматривать как (п,т)-потоышк.

Вершины данных, которые не являются входами и выходами, называются связями.

34 Dennis J.I!. Machines and Models lor Parallel Computing // International Journal оГ Parallel Programming. - 1994. - Vol. 22, № 1. - P. 47-77.

Каждой вершине данных р ¿'/'-оператора сопоставляется переменная, имеющая имя вершины данных и принимающая значения из некоторого множества У¡, Это множество содержи т в частности элемент неопределеио.

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

Vp = {истина, ложь, неопределеио}.

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

Состояние sp вершины данных р определяется значением её переменной р.

Состояние Sjf DF-onepamopa — это набор состояний всех его вершин данных: Sdr~ {spi, sp2,...}.

Входной (выходной) вектор DF-onepamopa — это вектор переменных, соответствующих входам (выходам) /^-оператора.

Событие - это переход .DF-оператора из одного состояния в другое.

Любое событие DF-оператора принадлежит одному из трех множеств:

-множеству IN внешних воздействий на неготовый вход DF-онератора,

-множеству OUT внешних воздействий на готовый выход DF-оиератора,

-множеству F срабатываний одного из базисных операторов, входящих в состав DF-onepaTopa.

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

Внешнее воздействие• на готовый выход у/ - это такое событие, в результате которого DF-oneparop из состояния s с определенным выходом Hi переходит в другое состояние л-// отличающееся от s только тем, что выход yf - неопределен.

Для каждого базисного оператора выделяется множество состояний Ма в которых базисный оператор готов к срабатыванию.

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

Для размножителя, блоков выполнения операций и принятия решений, а также для вентилей множество Ма состоит из всех состояний, в которых все входы определены и все выходы не определены.

Процесс в DF-onepamope — это последовательность переходов DF-оператора из одного состояния в другое, получающаяся в результате событий et, .......ек.

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

Модель поведения ОЕ-опсрачюра - это система ВЕН-{С,Б,Е}, где

(7 - структурная модель ^•"-оператора, содержащего заданный набор базисных операторов;

5 - множество состояний ОЛ-оператора;

Е - множество событий, Е ~ Ш I) ОПТ и /•'.

Под режимом работы ОР-оператора будем понимать совокупность поведений при ограничении на множество допустимых событий и множество исходных состояний.

Модель поведения ОГ-опсрапюра в заданном режиме - это система Л= {О, Б, Ег, Б„}, где Е, - множество событий, допустимых при данном режиме, &Б„- множество исходных состояний.

Введем следующие режимы: автономный режим, режим входных воздействий и срабатываний, конвейерный режим.

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

Перечислим операции, применяемые к базисным операторам для построения структурированных программ:

1) Операция объединения О^'-опсраторон;

2) Операция отождествления к пар вершин данных двух П17-операторов;

3) Операция замыкания выхода Д/г-опсратора на вход;

4) Операция размыкания связи £/7-оператора;

5) Операция построения цикла по стандартной схеме.

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

1) Каждый из базисных ОЕ-операторов языка потоков данных является структурированной программой.

2) Пусть даны два ЛР-опсратора, являющиеся структурированными программами потоков данных Ли В.

а) £Р-оператор, получающийся в результате применения операции объединения операторов А и В, является структурированной программой.

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

с) ¿□/«'-оператор, построенный по стандартной схеме, цикла из операторов А ч В, является структурированной программой.

3) Других структурированных программ нет.

л-] ->:2

А

В

< < £ VI у2 ш

(I

и

в

.'л тг

а) Объодшкяшо

! А В '

б) Отождествление ■Г2 а'2 о 0:,'3

А

£

в

У1

У

тп

Уз

<•} Замыкание " 1/2 Рис. 4.2: Операции обра кжанни ОК-опори горои

Для согласования работы операторов, составляющих структурированную программу, вводятся понятия синхронизации ОГ-оператора и синхроб.юка.

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

Теорема 4.1.

Любая структурированная программа - это либо один синхроблок типа 1 или 2, либо результат объединения или отождествления некоторой структурированной программы и синхроблока типа 1 или типа 2.

Теорема 4.2.

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

Теорема 3.

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

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

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

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

Рис.4.7,а. Переход Рис.4.7,Ь. Порт.

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

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

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

• агрегирование ( || ), т. е. неформальное объединение двух программ в одну без установления связей между ними;

• последовательная композиция (*), т. е. связывание выходов одной программы с входами другой;

• замыкание (•), которое для одного оператора не определено.

Граф потоков данных ОС ~ <Ор, Р, -/*', +1\ Ф> определяется пятью компонентами:

• Ор — конечное множество операторов op¡ конечного множества типов операторов Тир, Ор — { ор,}, ор^'Гир, \Ор\ = п, i = 1... и;

• Р — {Pj} — конечное множество портов, j = 1... к;

• -F = { -F¡ } — множество входных отношений инцидентности, где

-F¡ = < opi, Pj >, ор,е Ор, Pj е-Р,, -P¡ е Р,

-Pi — множество входных портов оператора op¡, |-F,-| > 1;

• +F=f+FJ - множество выходных отношений инцидентности, где

+F^< op,,p¡>, ор.еОр, pje+Pi, +Р,еР,

+P¡ — множество выходных портов оператора op-,, |+F,| > 1;

• Ф — функция разметки, которая назначает уникальное имя каждому оператору и уникальное имя каждому порту.

Граф потоков данных с очередями и стеками (DGQ) — это граф потоков данных DGQ = < Ор\ Р\ -F, +F, Ф > такой, что

a) множество портов Р' дополнено множеством очередей Q и стеков S: Р'= Р yj Q и S, причем множества Р, Q, S попарно не пересекаются. Для каждой очереди q и стека s определена наибольшая граница Ь для того, чтобы различать конечное число состояний любой очереди (стека).

-Р, -Q, -S — множества входных портов, очередей, стеков DGQ. +Р, +Q, +S — множества выходных портов, очередей, стеков DGQ.

b) множество типов операторов дополнено типами Qin (поместить в очередь), Qout (взять из очереди), Sin (поместить в стек), Sout (взять из стека),4 Тор' = Тор и {Qin, Qout, Sin, Sout}.

Любой DGQ. строится из конечного множества операторов с использованием конечного числа операций агрегирования, последовательной композиции и замыкания:

• Если для операторов op¡ и op¡ (-Pj'n+P/ = 0) и (+P¡ п -Pj' = 0), то можно осуществить агрегирование op¡ || opj.

• Если для операторов op¡ и op¡ [(+P¡'r>P/^0или (+Q¡'r>Qj'*0) или (+S¡'n-S/y0)] и (-P¡'n \ Pj'-0)y то возможна последовательная композиция операторов op*opj. Связывание портов различных типов не допускается,

PnQ=0 PnS=0, Sn Q=0.

• Замыкание для одного отдельно взятого оператора не определено. Если для операторов op¡ и op¡ [(+Pt'r>Pj'*0) или (+Q,'r>Qj'*0) или (+S¡'r>-S;*0)] и {(-Р/п+Р/=0> или

(-Qi'n+Qj'*0) или (-S'n+Sj'*0)\, то возможны в совокупности

две операции: последовательная композиция и замыкание

'(ор, * ор,).

?

щ

| Ом! |

о-

ь

Р

Ф

«ОО'

"Г

о /

Рис. 4.9. Пример ОСС>.

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

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

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

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

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

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

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

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

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

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

Как в последовательном, так и в параллельном случае рекурсивный

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

Шестая глава посвящена моделированию, анализу и оптимизации транспортных коммуникационных протоколов. Описана модификация протокола TCP - "TCP с адаптацией скорости" (ARTCP), которая

35 Badin N.M., Brodsky G.M., Sokolov, V.A. A Recursive Parallel Programming Language and its Application to Algebraic Computations // Joint Bulletin of the Novosibirsk Computing Center and A.P. Ershov Institute of Informatics Systems. Series: Computer Science. -Novosibirsk: NCC Publisher, 1999. 11. - C. 1-14.

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

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

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

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

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

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

• Разделение механизмов восстановления после ошибок и управления загрузкой.

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

3(S Alekseev I.V., Sokolov, V.A. ARTCP: F,(Ticicnt Algorithm for Transport Protocol for Packct Switched Networks // I.ectnre Notes in Computer Scicnce. - Berlin: Springer-Verlag, 2001.-№ 2127.-C. 159-174.

Рас. 6.1: Функциональные компоненты механизма управления потоком протокола АПТСР

Данная схема функционирования протокола ARTCP предусматривает пересмотр функционирования механизма управления потоком.

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

Задачей механизма диспетчеризации является отправка сегментов в сеть с определенной скоростью Rs (t), а не в виде всплеска. Значение Rs (t) задается функцией адаптации.

Механизм адаптации управляет двумя параметрами работы соединения: значением скорости Rs (t) и скоростью изменения скорости -тангенсом угла наклона ¡рафика Rs(t). Скоростью прирост скорости управляет механизм компенсации перегрузок.

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

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

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

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

- существует возможность возврата заявки для повторного обслуживания;

- вероятность возврата зависит как от внешних (вообще говоря, неизвестных) причин, так и от дисциплины обслуживания;

- длительность обслуживания заявки зависит от времени;

- имеется большое число заявок с резко различающимися длительностями обслуживания.

Нетрудно заметить, что перечисленные свойства справедливы для

TCP.

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

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

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

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

37 Balakrishnan H., Padmanabhan V., Katz R. The Effects of Assymetry on TCP Performance // ACM MobiCom. - 1997. - v. 9.

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

38 Sokolov V.A., Timofeev U.A. Dynamical Priorities without Time Measurements and Modification of the TCP // LNCS. - Berlin: Springer-Verlag, 2001. -№ 1649. - C. 240-245.

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

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

Эта имитационная модель использовалась для проведения эксперимента в рамках 9 сценариев, результаты которого показали существенное превосходство адаптивного алгоритма управления скоростью потока протокола ARTCP по сравнению с TCP.

Публикации. По теме диссертации опубликовано более 60 работ, в том числе 3 монографии [1-3], две из которых [1,2] — в центральном издательстве ФИЗМАТ ЛИТ (одна [1] - при поддержке издательского гранта РФФИ 05-07-95008), 13 статей в центральных отечественных и ведущих зарубежных журналах, 16 докладов на международных конференциях, 9 - на отечественных конференциях, 19 статей в местных изданиях, 3 учебных пособия (одно из них [10] - с грифом Министерства общего и профессионального образования РФ).

Основные положения диссертационного исследования представлены в следующих публикациях автора:

Монографии и статьи в ведущих рецензируемых научных журналах, перечень которых утвержден ВАКом

1. Соколов, В.А. Структурированные системы переходов: монография / М.: ФИЗМАТЛИТ, 2006. - 178 е.: ил. - С грифом "Допущено учебно-

методическим советом по прикладной математике и информатике УМО по классическому университетскому образованию в качестве учебного пособия для студентов высших учебных заведений, обучающихся по специальности 010200 «Прикладная математика и информатика» и но направлению 510200 «Прикладная математика и информатика»". — Издание поддержано фантом РФФИ № 05-07-95008. (В соавторстве с Е.В. Кузьминым. Авторское участие - 50%).

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

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

4. Соколов, В.А. Об изоморфизмах максимальных подалгебр алгебры Р. Робинсона // Алгебра и логика. - 1967. - № 6 (3). - С. 91-99.

5. Соколов, В.А. О максимальных подалгебрах алгебры всех частично рекурсивных функций Н Кибернетика. - 1972. - № 1. - С. 70-73.

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

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

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

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

Учебные пособия

10. Соколов, В.А. Формальные языки и грамматики: учебное пособие / Ярославль: Изд-во Яросл. гос. ун-та им. П.Г. Демидова, 1998. - 152 е.: ил. -С грифом "Рекомендовано Министерством общего и профессионального образования РФ в качестве учебного пособия для студентов университетов но специальности 010200 «Прикладная математика и информатика» и по направлешпо 510200 «Прикладная математика и информатика»".

11. Соколов, В.А. Формальные языки и грамматики. Курс лекций: учебное пособие / Ярославль: Изд-uo Яросл. гос. ун-та им. П.Г. Демидова, 2003,-152 е.: ил.

12. Соколов, В.А. Формальные языки и грамматики. Задачи и упражнения: учебное пособие / Ярославль: Изд-во Яросл. гос. ун-та им. П.Г. Демидова, 1993. — 56 е.: ил. (В соавторстве с О.Б. Кушнаренко и U.M. Бадиным. Авторское участие - 50%).

Научные статьи

13. Соколов, В.А. Замечания о классе частичных функций счетнозначнон логики // Дискретный анализ. — 1971. —№ 19. — С. 56-62.

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

15. Соколов, В.А. Об одной модели параллельных вычислений // Вычислительные системы и процессы: сб. науч. тр. / отв. ред. Ю.А. Маматов. -Ярославль: ЯрГУ, 1985. - С. 62-76.

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

17. Соколов, В.А. Замечание о классе функций, вычислимых сетями Петри // Моделирование и анализ вычислительных систем: сб. науч. тр. / отв. ред. Ю.А. Маматов.-Ярославль: ЯрГУ, 1987.- С. 119-123.

18. Соколов, В.А. Об одном подходе к реализации циклов и процедур на ЭВМ, управляемых потоком данных // Моделирование и оптимизация вычислительных систем. и процессов: сб. науч. тр. / отв. ред. Ю.А. Маматов. — Ярославль: ЯрГУ, 1988. — С. 41-44. (В соавторстве с Г.М. Бродским. Авторское участие — 50%).

19. Соколов, В.А. Статический подход к распределению памяти в системе программирования для ЭВМ, управляемых потоком данных // Вычислительные системы: моделирование, проектирование и программирование: сб. науч. тр. / отв. ред. Ю.А. Маматов. — Ярославль: ЯрГУ, 1990. — С. 14-20. (В соавторстве с Г.М. Бродским. Авторское участие - 50%).

20. К проблеме построения компиляторов для параллельных систем распределенного типа / О.Б. Кушнаренко, О.Л. Подземский, В.А. Соколов, Б.В. Тамаров // Многопроцессорные вычислительные системы и параллельные алгоритмы: сб. науч. тр. / отв. ред. Ю.А. Маматов. — Ярославль: ЯрГУ, 1991. - С. 8-14. (В соавторстве с О.Б. Кушнаренко, О.Л. Подземским и Б.В. Тамаровым. Авторское участие - 25%).

21. Соколов, В.А. Визуализация сетевых моделей процессов управления в параллельных программах // Архитектура и программное

обеспечение вычислительных систем: сб. науч. тр. / отв. ред. Ю.А. Маматов. — Ярославль: ЯрГУ, 1992. - С. 32-34. (В соавторстве с Б.В. Тамаровым. Авторское участие - 50%).

22. Соколов, В.Л. Применение сетей Петри для анализа профамм, написанных на языке параллельного программирования // Моделирование и анализ информационных систем / Под ред. В.А. Соколова. - Ярославль: Изд-во Яросл. гос. ун-та им. II.Г. Демидова, 1993. - Т.1. - С. 27-44. (В соавторстве с А.И. Легаловым. Ангорское участие - 50%).

23. Соколов, В.А. Анализ внешнего поведения одного класса программ для машин потоков данных // Моделирование и анализ информационных систем / Под ред. В.А. Соколова. - Ярославль: Изд-во Яросл. гос. ун-та им. П.Г. Демидова, 1993. - Т.1. - С. 106-120. (В соавторстве с H.A. Абрамовой и Э.Е. Рубцовой. Авторское участие - 30%).

24. Соколов, В.А. Рекурсивно-параллельное программирование и сети Петри: моделирование, анализ и верификация программ // Моделирование и анализ информационных систем / Под ред. В.А. Соколова. — Ярославль: Изд-во Яросл. гос. ун-та им. П.Г. Демидова, 1994. - Т.2. - С. 91-97. (В соавторстве с О.Б. Кушнаренко. Авторское участие - 50%).

25. Соколов, В.А. Модели внешнего поведения ациклических программ для машин потоков данных // Моделирование и анализ информационных систем / Под ред. В.А. Соколова. — Ярославль: Изд-во Яросл. гос. ун-та им. П.Г. Демидова, 1994. -Т.2. - С. 3-12. (В соавторстве с H.A. Абрамовой и Э.Е. Рубцовой. Авторское участие — 30%).

26. Соколов, В.А. Модели и свойства класса структурированных программ в языках потоков данных // Моделирование и анализ информационных систем / Под ред. В.А. Соколова. - Ярославль: Изд-во Яросл. гос. ун-та им. П.Г. Демидова, 1996. - Т.З. - С. 127-157. (В соавторстве с Э.Е. Рубцовой. Авторское участие — 50%).

27. Sokolov, V.A. On a Technology of Design and Analysis of Dataflow Programs // Lecture Notes, in Computer Sciences. - Berlin: Springer-Verlag, 1997. - № 1277. - С. 115-120. (В соавторстве с Э.Е. Рубцовой и С.А. Рубцовым. Авторское участие - 30%).

28. Соколов, В.А. Языковые средства рекурсивно-параллельного программирования // Актуальные проблемы современной математики: сб. науч. тр. / отв. ред. В.Г1. Чуваков. - Новосибирск: НИИ МИОО, 1997. -Т.З. - С. 19-28. (В соавторстве с Н.М. Бадиным и Г.М. Бродским. Авторское участие - 30%).

29. Соколов, В.А. Протокол TCP с адаптацией скорости // Моделирование и анализ информационных систем. — 1999. - Т.6, № 1. - С. 4-12. (В соавторстве с И-В. Алексеевым. Авторское участие — 50%).

30. Sokolov, V.A. A Model for Reachability Analysis of Data-Flow Graphs with Queues and Stacks // Моделирование и анализ информационных

систем. - 1999. - Т. б, № 1. - С. 50-57. (В соавторстве с Э.Е. Рубцовой. Авторское участие - 50%).

31. Sokolov, V.A. A Recursive Parallel Programming Language and its Application to Algebraic Computations // Joint Bulletin of the Novosibirsk Computing Center and A.P. Ershov Institute of Informatics Systems. Series: Computer Science. - Novosibirsk: NCC Publisher, 1999. -№ 11. - C. 1-14. (B соавторстве с H.M. Бадиным и Г.М. Бродским. Авторское участие — 30%).

32. Sokolov, V.A. Dynamical Priorities without Time Measurement and Modification of the TCP // Lecture Notes in Computer Science. — Berlin: Springer-Verlag, 2001. - № 2244. - C. 240-245. (В соавторстве с E.A. Тимофеевым. Авторское участие — 50%).

33. Sokolov, V.A. ARTCP: Efficient Algorithm for Transport Protocol for Packet Switched Networks // Lecture Notes in Computer Science. - Berlin: Springer-Verlag, 2001. - № 2127. - C. 159-174. (В соавторстве с И.В. Алексеевым. Авторское участие — 50%).

34. Sokolov, V.A. Modeling and Traffic Analysts of the Adaptive Rate Transport Protocol // Future Generation Computer Systems. — North-Holland: ELSVIER, 2002. - V.18, № 6. - C. 813-827. (В соавторстве с И.В. Алексеевым. Авторское участие — 50%).

35. Sokolov, V.A. An Extensible Coloured Petri Net Model of a Transport Protocol for Packet Switched Networks // Lecture Notes in Computer Science. — Berlin: Springer-Verlag, 2003. - № 2763. - C. 66-75. (В соавторстве с Д.Ю. Чалым. Авторское участие - 50%).

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

37. Sokolov, V.A. ■Model Checking ц-Calculus in Well-Structured Transition Systems // Joint Bulletin of the Novosibirsk Computing Center and A.P. Ershov Institute of Informatics Systems. Series: Computer Science. — Novosibirsk: NCC Publisher, 2004. - № 20. - C. 49-59. (В соавторстве с Е.В. Кузьминым и Н.В. Шиловым. Авторское участие - 30%).

38. Sokolov, V.A. An Approach to the Implementation of the Dynamical Priorities Method // Lecture Notes in Computer Sciences. — Berlin: SpringerVerlag, 2005. - № 3606. - C. 74-78. (В соавторстве с E.A. Тимофеевым. Авторское участие - 50%).

Труды конференций

39. Соколов, В.А. О мощности множества "эффективных" предельных Логик // III Всесоюзная конференция по теоретической кибернетике: сб. тезисов докладов. Новосибирск, 1974. - Новосибирск: Институт математики СО АН СССР, 1974. - С. 120-121.

40. Соколов, В.А. Об одной задаче в теории сетей Петри // Математические методы в исследовании операций: сб. тезисов докладов

Международной научной конференции. София (Болгария), 1987. - София: Институт математики АН Болгарии, 1987. - С. 48.

41. Соколов, В. А. К вопросу о формализации вычислений, управляемых потоком данных // II Всесоюзная конференция по прикладной логике: сб. тезисов докладов. — Новосибирск, 1988. — Новосибирск: Институт математики СО АН СССР, 1988. - С. 219-221.

42. Соколов, В.А. Некоторые проблемы анализа и редукции сетей Петри // Методы и системы технической диагностики: сб. тезисов докладов X Международной конференции по проблемам теоретической кибернетики. Саратов, 1993. - Саратов: СГУ, 1993.-Вып. 18.-С. 164-166. (В соавторстве с О.В. Ноевой и U.C. Сидоровой. Авторское участие — 30%).

43. Соколов, В.А. Метод формализации анализа программ для машин, управляемых потоком данных // Теоретические и прикладные проблемы моделирования предметных областей в системах баз данных и знаний: сб. тезисов докладов II Международного научно-технического семинара. Киев, 1993. - Киев: Институт кибернетики АН Украины, 1993. - Т.2. — С. 190-194. (В соавторстве с Э.Е. Рубцовой. Авторское участие - 50%),

44. Соколов, В.А. Система автоматизированного проектирования и моделирования // Теоретические и прикладные проблемы моделирования предметных областей в системах баз данных и знаний: сб. тезисов докладов II Международного научно-технического семинара. Киев, 1993. -Киев: Институт кибернетики All Украины, 1993. - Т.2. - С. 194-196. (В соавторстве с О.В. Ноевой. Авторское участие - 50%).

45. Соколов, В.А. Об операциях редукции сетей Петри // III Международная конференция по алгебре памяти М.И. Каргаполова: сб. тезисов докладов. Красноярск, 1993. - Красноярск: КрасГУ, 1993. - С. 305306. (В соавторстве с Н.С. Сидоровой. Авторское участие - 50%).

46. Соколов, В.А. Проблемы разработки формализованных семантических моделей программ для машин потоков данных // Юбилейная научная конференция "Актуальные проблемы естественных и гуманитарных наук" (Математика. Информатика): сб. докладов. Ярославль, 1995. — Ярославль: ЯрГУ, 1995. - С. 140-143. (В соавторстве с Э.Е. Рубцовой. Авторское участие - 50%).

47. Соколов, В.А. Об одном подходе к семантическому анализу и доказательству правильности рекурсивно-параллельных программ // Юбилейная научная конференция "Актуальные проблемы естественных и гуманитарных наук" (Математика. Информатика): сб. докладов. Ярославль, 1995. - Ярославль: ЯрГУ, 1995. — С. 134-137. (В соавторстве с О.Б. Кушнаренко. Авторское участие - 50%).

48. Соколов, В.А. Анализ семантических свойств одного класса рекурсивно-параллельных программ // IV Международная конференция по прикладной логике: сб. тезисов докладов. Иркутск, 1995. — Иркутск:

ИГУ, 1995. - С. 72-73. (В соавторстве с О-В. Кушнаренко. Авторское участие — 50%).

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

50. Соколов, В.А. Структурированные сети потоков данных // Математическое моделирование и компьютерные технологии: сб. тезисов докладов Всероссийского симпозиума. Кисловодск, 1997. — Кисловодск: КИЭиП, 1997. - Т.З "Информационные системы". - С. 93-94. (В соавторстве с Э.Е. Рубцовой и С.А. Рубцовым. Авторское участие - 30%).

51. Sokolov, V.A. Behavioral Equivalences on Communication Free Petri Nets // III Международный конгресс по индустриальной и прикладной математике "INPR1M-98": сб. трудов. Новосибирск, 1998. - Новосибирск: Институт математики СО РАИ, 1998. (В соавторстве с II.C. Сидоровой и Н.Ю. Юстиновой. Авторское участие - 30%).

52. Sokolov, V.A. Symbolic Reachability Analysis of Data Flow Programs with Data Structures // III Международный конгресс по индустриальной и прикладной математике "1NPR1M-98": сб. трудов. Новосибирск, 1998. -Новосибирск: Институт математики СО РАН, 1998. (В соавторстве с Э.Е. Рубцовой и Н.С. Сидоровой. Авторское участие - 30%).

53. Sokolov, V.A. Compensation Mechanism for Adaptive Rate TCP // First IEEE Popov Workshop on Internet Technologies and Services: сб. трудов Международного семинара. Москва, 2000. - М., 2000. - Т. 2. — С. 68-75. (В соавторстве с И.В. Алексеевым. Авторское участие — 50%).

54. Sokolov, V.A. Dynamical Priorities without Time Measurement and Modification of the TCP // Andrei Ershov Fourth International Conference «Perspectives of System Informatics»: сб. трудов IV Международной конференции PSI-2001. Новосибирск, 2001. — Новосибирск: Институт систем информатики им. А.П. Ершова СО РАН, 2001. - С. 141-146. (В соавторстве с Е.А. Тимофеевым. Авторское участие — 50%).

55. Соколов, В.А. Оптимизация обработки запросов к большим базам данных методами ТМО // Всероссийская научная конференция, посвященная 200-летию Ярославского государственного университета им. П.Г. Демидова: сб. докладов "Информатика". Ярославль, 2003. -Ярославль: ЯрГУ, 2003. - С. 13-16. (В соавторстве с П.П. Черменским. Авторское участие - 50%).

56. Соколов, В.А. Курс "Верификация программ" в подготовке магистров по прикладной математике и информатике // Функциональные пространства. Дифференциальные операторы. Проблемы математического образования: сб. трудов И Международной конференции, посвященной 80-летию чл.-корр. РАН Л.Д. Кудрявцева. Москва, 2003. - М.: ФИЗМАТЛИТ,

2003.-С. 338-340.

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

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

59. Sokolov, V.A. Communicating Colouring Automata // Международный семинар "Program Understanding -2003" (Satellite Workshop of Fifth International Conference «Perspectives of System Informatics PSI-2003»): сб. трудов. Новосибирск, 2003. - Новосибирск: Институт систем информатики им. А.П. Ершова СО РАН, 2003. - С. 40-46. (В соавторстве с Е.В. Кузьминым. Авторское участие - 50%).

60. Соколов, В.А. Методы исследования поведения транспортных протоколов в условиях интенсивного сетевого трафика / Международная конференция по вычислительной математике "МКВМ-2004": сб. трудов рабочего совещания "Распределенные информационно-вычислительные ресурсы и математическое моделирование". Новосибирск, 2004. — Новосибирск: Институт вычислительной математики и математической геофизики СО РАН, 2004. - С. 126-131. (В соавторстве с Д.Ю. Чалым. Авторское участие — 50%).

61. Sokolov, V.A. Model Checking (i-CalcuIus in Well-Structured Transition Systems // Temporal Representation and Reasoning: сб. докладов XI Международного симпозиума TIME-2004. Tatihou, France, 2004. - France: IEEE Press, 2004. - C. 152-155. (В соавторстве с Е.В. Кузьминым и Н.В. Шиловым. Авторское участие — 30%).

62. Sokolov, V.A. Model Checking for Well-Structured Transition Systems of Automaton Type // Международная конференция по вычислительной математике "МКВМ-2004": сб. трудов рабочего совещания "Распределенные информационно-вычислительные ресурсы и математическое моделирование". Новосибирск, 2004. - Новосибирск: Институт вычислительной математики и математической геофизики СО РАН, 2004. - С. 73-85. (В соавторстве с Е.В. Кузьминым. Авторское участие — 50%).

63. Соколов, В.А. Исследование свойств класса вполне структурированных систем переходов // Методы и средства обработки информации: сб. трудов II Всероссийской научной конференции МСО-2005. Москва, 2005. - М.: МГУ, 2005. - С. 388-393. (В соавторстве с Е.В. Кузьминым. Авторское участие — 50%).

Лицензия J1P № 071542 от 24.11.97 г. Редакщюнно-издательский центр Международного университета бизнеса и новых технологий /института/. Подписано п печать 20.03.2006. Заказ № (>7Х.

ФорматЛ5. Уч.-изд. л. - 2,00. Тираж 100 экз. Отпечатано в Центре малой полиграфии МУБиПТ. г. Ярославль, ул. Советская, 80.

Введение

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, а именно, предложено и обосновано использование оценки средних длин очередей вместо замеров времени возврата с целью оптимизации процесса передачи информации в сетях с коммутацией пакетов.

Заключение

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

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.