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

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

□□3456428

Быстрой Александр Васильевич

СПЕЦИФИКАЦИЯ И АНАЛИЗ РАСПРЕДЕЛЕННЫХ СИСТЕМ С ИСПОЛЬЗОВАНИЕМ ИНСТРУМЕНТАЛЬНЫХ СРЕДСТВ, ПОДДЕРЖИВАЮЩИХ МОДЕЛИ СЕТЕЙ ПЕТРИ

05.13.11 — математическое и программное обеспечение вычислительных машин, комплексов, систем и компьютерных сетей

АВТОРЕФЕРАТ диссертации на соискание ученой степени кандидата физико-математических наук

Новосибирск - 2008 0 5 ДЕК 2008

003456428

Работа выполнена в Институте систем информатики им. А.П. Ершова Сибирского отделения Российской академии наук

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

Непомнящий В.А.

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

Ломазова И. А. доктор технических наук, Глинский Б.М.

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

имени П.Г. Демидова

Защита состоится 12 декабря 2008 года в 14 час. 00 мин. на заседании диссертационного совета К 003.032.01 в Институте систем информатики имени А.П. Ершова СО РАН по адресу: 630090, Новосибирск, пр. Ак. Лаврентьева, 6

С диссертацией можно ознакомиться в читальном зале библиотеки Института систем информатики СО РАН

Автореферат разослан _[]_ ноября 2008 г.

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

специализированного совета К 003.^32.01 к.ф.-м.н.

Мурзин Ф.А.

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

Актуальность. Сети Петри — одна из наиболее популярных моделей параллельных систем, используемых как для теоретических исследований, так и практических применений в различных областях — распределенных баз данных и операционных систем, архитектур вычислительных машин, систем и сетей, систем программного обеспечения, протоколов коммуникаций, семантики параллельных языков, систем с элементами искусственного интеллекта и т.д. Модели сетей Петри играют такую же важную роль в изучении параллельных систем, что и конечные автоматы для последовательных. К достоинствам сетей Петри относятся наглядное графическое представление их структуры и эффективные методы анализа их поведения. В течение трех последних десятилетий теория сетей Петри породила большое разнообразие моделей, теорем, алгоритмов и инструментов, предназначенных для спецификации, разработки и верификации параллельных/распределенных систем. Складываются устойчивые системы базовых понятий и общепринятых методик, появляются специальные периодические издания, регулярно проводятся научные конференции, посвященные данной тематике. С помощью сетевых моделей установлен ряд фундаментальных фактов, которые позволили лучше понять природу параллельных вычислений. Так, выделены три базовых отношения между событиями параллельных систем: причинная зависимость, параллелизм и недетерминированный выбор (конфликт). С одной стороны, дальнейшее продвижение в данной области связано с изучением обоснованных с теоретической точки зрения подклассов сетевых моделей (например, элементарных сетевых систем (elementary net systems), систем с условиями/событиями (condition/event systems), сетей со свободным выбором (free choice nets), позволяющих рассматривать сети Петри как математические объекты и формально исследовать их свойства, правила конструирования и преобразования. С другой стороны, появились различные расширения сетей Петри: разнообразные модели временных и стохастических сетей, сети с предикатами (predicate/transition nets), сети Петри с раскрашенными фишками (coloured Petri nets) и т. д., призванные служить математическим инструментом для моделирования и анализа реальных параллельных систем со сложной структурной организацией. Кроме того, в настоящее время также разрабатывается целый ряд инструментальных систем, основанных на моделях сетей Петри.

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

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

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

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

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

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

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

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

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

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

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

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

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

RT-MEC (Real-Time Model and Equivalence Checker), XNES (eXtensible NEtworks Simulator), SPV(SDL Protocol Vérifier), которые поддерживают различные методы проектирования, анализа, верификации, валида-ции сложных распределенных систем и систем реального времени, представленных различными сетевыми моделями.

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

Представление работы. Основные идеи и конкретные результаты диссертационной работы обсуждались на следующих международных научных симпозиумах, конференциях и семинарах: 2-й Международный симпозиум по информатике в России (Екатеринбург, 2007). 13th Intern. Workshop "Concurrency: Spécification and Programming" (Berlin, 2004); 1-ая и 2-ая Всероссийская научная конференция "Методы и средства обработки информации" (Москва: МГУ, 2003, 2005); 4-ый Сибирский Конгресс "Прикладная и Индустриальная Математика" (Новосибирск, 2000); Международный семинар "Распределенная обработка информации" (Новосибирск, 1998); lst Intern. Workshop "Formai Description Technique, ESTELLE'98" (Evry, France, 1998); Intern. Workshop "Discrète Event Systems" (Cagliari, Italy, 1998); Intern. Conférence "Parallel Computing in Electrical Engineering"(Bialystok, Poland, 1998); 3rd and 5th Intern. Conférence "Parallel Computing Technologies" (St. Petersburg, Russia, 1995, 1999); 1-ая Всесоюзная конференция "Проблемы создания супер-ЭВМ, супер-систем и эффективность их применения (Минск, 1987))";

Кроме того, доклады по теме работы были сделаны на ряде семинаров Института информатики Университета г. Хильдесхайма (Германия), Института прикладной математики (г. Гренобль, Франция), Института кибернетики (г. Киев), Института программных систем РАН (г. Переславль-Залесский), Института математики СО РАН (г. Новосибирск), Института систем информатики СО РАН (г. Новосибирск), кафедр Новосибирского государственного университета и др.

Публикации. По теме диссертации опубликовано 30 научных работ, в том числе 3 — в изданиях, входящих в Перечень ВАК; 1 — монография; 9 — в трудах международных симпозиумов, конференций и семинаров; 5 — в трудах национальных симпозиумов, конференций и семинаров; 9 — в сборниках научных трудов. В конце автореферата

приведен список основных публикаций.

Участие в проектах и грантах. Результаты исследований, изложенные в диссертации, легли в основу ряда научно-исследовательских проектов, поддержанных в разные годы различными грантами Российского фонда фундаментальных исследований (гранты 93-01-00986, 96-01-01655,00-01-00898, 03-07-90331в, 07-07-00173а), Фондом Фольксваген (грант 1/70 564), Фондом ИНТАС (грант 1010-СТ93-0048), Фондом ИНТАС-РФФИ (грант 95-0378) и др.

Личный вклад. Диссертация содержит результаты работ, выполненных автором в Вычислительном центре СО РАН с 1974 по 1990 гг. и в Институте систем информатики СО РАН с 1990 по 2008 гг.

Во всех работах опубликованных в соавторстве автор участвовал в постановке задач, разработке методов решения и анализе результатов. Также в работах [1,14,19,20,24,25,28] диссертантом предложены синтаксис и семантика подъязыка управления языка Барс, алгоритмы управления вычислениями и программно реализованы соответствующие компоненты транслятора и симулятора. Результаты, изложенные в работах [6,7,10] получены автором самостоятельно, за исключением того, что разработка структуры и функций системы ПТ-МЕС была выполнена совместно с И.Б. Вирбицкайте. В работах [2,3,5,8,9,11,15-18,26,27] диссертант принимал участие в создании модели ИВТ-сетей, им сформулированы требования и разработана архитектура программных комплексов XNES/SPV, он также участвовал в их программной реализации и отладке. Работы [21-23] написаны в неделимом соавторстве.

Структура и объем работы. Диссертация состоит из введения, четырех глав, разбитых на разделы, заключения, списка литературы и приложения. Общий объем диссертации 136 е., основной текст - 126 е., приложение - 10 е., библиографический список - 121 наименование. Работа содержит 39 рисунков и 11 таблиц.

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

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

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

СП со свободным выбором, регулярные и иерархические СП, дискретно-временные и непрерывно-временные СП, раскрашенные СП, временные и иерархические раскрашенные СП, а также СП с приоритетами. В конце главы представляется краткий аналитический обзор инструментальных систем, базирующихся на сетевых моделях. При этом обосновываются достоинства ряда программных комплексов, среди которых отмечается система PEP (Programming Environment based on Petri nets).

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

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

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

В разделе 2.3 описывается язык параллельного программирования Барс, базирующийся на асинхронной модели вычислений. Этот язык разрабатывался в 1980-1985 гг. под руководством В.Е. Котова в рамках выполняемого в Вычислительном центре СО АН СССР научно-исследовательского проекта Марс (модульные асинхронные развиваемые системы). Основными чертами языка являются: наличие развитых средств описания разнообразных структур управления; непроцедурная форма записи применения операций к сложным структурам данных; модульность и развиваемость. Язык Барс представляет собой систему из ортогональных взаимодействующих подъязыков: С-язык содержит средства описания управления (см. ниже), Е-язык содержит средства описания выражений, М-язык содержит средства описания работы с памятью, кроме того, выделен специальный подъязык для конструирования и преобразования (абстрактных) структур данных (К-язык) и вспомогательные подъязыки для описания типов данных.

В разделе 2.4 рассматривается синтаксис и семантика подъязы-

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

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

Компонент транслятора языка Барс, осуществляющий перевод структур управления во внутреннюю форму (расширенное сетевое представление) реализован на языке Си.

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

арбитража.

Третья глава посвящена анализу временных сетевых моделей посредством системы КГ-МЕС. В качестве моделей распределенных систем реального времени рассматриваются модель дискретно-временной сети Петри (ДВСП) ШЯ = (Р, Т, Р, М0, £>) (с функцией Д сопоставляющей каждому переходу целочисленную временную длительность его срабатывания) и модель непрерывно-временной сети Петри (НВСП) С77/ = (Р, Т, Р, М0,0) (с функцией Д сопоставляющей каждому переходу временной интервал с целочисленными границами его срабатывания).

В разделе 3.1 разрабатываются методы структурного анализа НВСП. Считается, что НВСП имеет корректное тпаймирование, если £>(¿1) П £>(£2) ф 0 для всех П* г2 ф 0-

Теорема 3.1. Пусть N = (Р,Т, Р, Мо) — ограниченная (безопасная) СП. Тогда СТН = (./V, Ц) — ограниченная (безопасная) НВСП при любом корректном таймировании И.

Теорема 3.2. Пусть N = (Р,Т,Р,Мо) — живая СП, удовлетворяющая следующим условиям: \/р е Р о |р* | > 1 и Ур, <7 € Р о р* П д* ф 0 => р* С д* V / С р\ Тогда СТЛГ = (Р, Т, Р, М0, Р>) - живая НВСП при любом корректном таймировании.

Теорема 3.3. Пусть СТМ = (Р, Г, Р, М0, Б) — живал (дивергентная, ограниченная, безопасная) НВСП с корректным таймированием. Тогда N = (Р, Т, Р, Мо) — живая (дивергентная, ограниченная, безопасная) СП.

Далее приводятся алгоритмы структурного анализа некоторых поведенческих свойств непрерывно-временной СП со свободным выбором (НВССВ).

Алгоритм А1 осуществляет анализ живости ограниченных НВССВ.

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

Алгоритм А2.6 производит углубленный анализ ограниченности непрерывно-временных структурированных сетей — определяет максимальное количество фишек для каждого места.

Алгоритм АЗ предназначен для анализа свойства дивергентности НВССВ при заданном множестве внутренних переходов.

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

В разделе 3.2 строится семантика "истинного" параллелизма ДВСП и НВСП в терминах временных первичных структур событий и временных локальных структур событий соответственно.

Для ДВСП устанавливается изоморфизм между множеством RSS(TESt>taî) достижимых временных конфигураций временной первичной структуры TESvtM, упорядоченным отношением смены конфигураций (—»), и множеством STP{VTJ\f) временных бесконфликтных сетей-процессов, упорядоченным отношением вложения (С). Теорема 3.6. Для ДВСП VTM верно, что частично-упорядоченные множества (RSS(TESvt/s),->) и (STP(VTAf),ç) изоморфны.

Далее вводится понятие временных локальных структур событий и разрабатывается семантика "истинного параллелизма" для безопасных НВСП. Приводится построение, позволяющее по безопасной НВСП CTAÎ получить временную локальную структуру событий tptes(CTJ\f) такую, что множество seq(SFS(CTAf)) последовательностей шагов НВСП, упорядоченное отношением вложения (С), и множество ExecSet(tptes(CTAf)) выполнений временной локальной структуры событий, упорядоченное отношением вложения (С), изоморфны. Теорема 3.7. Для НВСП СТМ верно, что частично-упорядоченные множества (seq(SFS(CTM)),C) и (ExecSet(tptes(CTAf))),Ç) изоморфны.

В разделе 3.3 предлагается программный комплекс RT-MEC (RealTime Model and Equivalence Checker), поддерживающий спецификацию, валидацию и верификацию параллельных систем реального времени, представленных различными моделями временных сетей Петри, и функционирующий на базе системы РЕР. При рассмотрении структуры и функций комплекса особенное внимание уделяется модулям, поддерживающим анализ, симуляцию и верификацию временных расширений сетей Петри. В комплексе RT-MEC анализ осуществляется посредством исследования структуры моделируемой системы, валидация — путем имитационного моделирования (симуляции), а верификация — с помощью как "проверки модели", так и проверки на поведенческую эквивалентность. Отличительная черта комплекса RT-MEC состоит в том, что делается попытка объединить в единое целое различные методы анализа и верификации распределенных систем реального времени с возможностью последующего их сравнения. Также приводятся резуль-

таты экспериментов, проведенных средствами R.T-MEC.

Четвертая глава посвящена разработке и реализации программного комплекса XNES (eXtended Net Editor and Simulator), являющегося одним из основных компонент системы SPV (SDL Protocol Verifier), предназначенной для проектирования, анализа и верификации протоколов коммуникаций, представленных моделями ИВТ-сетей (модификациями иерархических временных раскрашенных сетей Петри Йенсе-на). XNES позволяет работать с сетевыми моделями, как полученными в результате трансляции с языков спецификаций (SDL, Estelle), так и построенными непосредственно в XNES, а также импортировать и экспортировать модели для использования совместно с другими системами. Комплекс XNES реализован с использованием языка программирования Python, открытой библиотеки Petri Net Kernel и открытого формата хранения PNML (Petri Net Markup Language).

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

В разделе 4.2 рассматриваются структура и функции программного комплекса XNES. Основные модули XNES: графический редактор для построения сетевых моделей; симулятор для имитационного моде-

лирования и отладки ИВТ-сетей; трассировщик для протоколирования сеанса симуляции; визуализатор для построения высоко-уровневой визу-ализационной модели протокола; подключаемые модули (плагины) для расширения возможностей системы XNES.

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

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

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

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

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

Далее рассматриваются результаты экспериментов, проводимых с использованием системы XNES с сетевыми моделями известных протоколов таких, как ATMR-протокол, InRes-протокол, i-протокол и кольцевой протокол RE.

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

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

Основные результаты, полученные в диссертации

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

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

3. Разработан и реализован программный комплекс XNES (extended Net Editor and Simulator), являющийся одним из основных компонент системы SPV (SDL Protocol Verifier), предназначенной для проектирования, анализа и верификации протоколов коммуникаций, представленных моделями ИВТ-сетей (модификациями иерархических временных раскрашенных сетей Петри). С помощью комплека проведены эксперименты с рядом протоколов коммуникаций с целью анализа их корректности, включая сетевые модели таких известных протоколов, как InRes-протокол, ATMR-протокол, i-протокол и кольцевой протокол RE.

Основные публикации по теме диссертации

Публикации в изданиях, входящих в Перечень ВАК:

1. Бульонков М.А., Быстров А.В., Дудоров Н.Н., Котов В.Е. Базовый язык параллельного программирования Барс // Программирование. -1986. - № 6. - С. 32-40.

2. Непомнящий В.А., Алексеев Г.И., Быстров А.В., Куртов С.А., Мыльников С.П., Окунишникова Е.В., П.А. Чубарев П.А., Чурина Т.Г. Использование сетей Петри для верификации распределенных систем, представленных на языке Estelle // Известия академии наук. Теория и системы управления. - 1999. - N. 5. - С. 105-116.

3. Непомнящий В.А., Алексеев Г.И., Быстров А.В., Мыльников С.П., Окунишникова Е.В., П.А. Чубарев П.А., Чурина Т.Г. Верификация коммуникационных протоколов, представленных на языке Estelle с помощью сетей Петри высокого уровня // Программирование. - 2001. - № 2.

- С. 18-30.

Публикации в трудах международных конференций:

4. Быстров А.В. Синхросети - средство описания взаимодействия асинхронных процессов // Proc. 4th International Conference of Young Computer Scientists. - Bratislava, 1984. - P. 52-56.

5. Nepomniaschy V.A., Alekseev G.I., Bystrov A.V., Churina T. G., Myl-nikov S. P., Okunishnikova E. V. Petri net modelling of Estelle-specified communication protocols // Proc. 3rd Intern. Conference PaCT-95, St.-Petersburg, Russia, 1995. Lecture Notes in Computer Science . - 1995. -Vol. 964. - P. 94-108.

6. Быстров A.B., Вирбицкайте И.Б. Автоматический анализ и верификация распределенных систем реального времени // Тр. 6-ого межд. семинара "Распределенная обработка информации" (РОИ'98 & DDP'98).

- Новосибирск: Изд-во СО РАН, 1998. - С. 236-240.

7. Bystrov А.V., Virbitskaite, I.B. RT-Mec: a Tool for Validation and Verification of Petri Nets with Time Parameters // Proc. Intern. Workshop on Discrete Event Systems. - Italy, Cagliari, 1998. The IEE Publisher, London, 1998. - P. 510-514.

8. Nepomniaschy V.A., Alekseev G.I., Bystrov A.V., Churina T.G., Myl-nikov S.P., Okunishnikova E.V. Towards Verification of Estelle-specified Communication Protocols: Coloured Petri Net Approach // Proc. Intern. Conf. on Parallel Computing in Electrical Engineering, - Poland, Bialystok, 1998. - P. 141-147.

9. Nepomniaschy V.A., Alekseev G.I., Bystrov A.V., Churina T.G., Myl-

nikov S.P., Okunishnikova E.V. EPV — Petri Net Based Estelle Protocol Verifier // Proc. 1st Intern. Workshop on the Formal Description Technique Estelle. - France, Evry, 1998. - P. 101-108.

10. Bystrov A.V., Virbitskaite I.B. Implementing Model Checking and Equivalence Checking for Time Petri Nets by the RT-MEC Tool // Proc. 5th Intern. Conf. PaCT-99, St-Petersburg, Russia, 1999. - Lecture Notes in Computer Science. Springer Berlin / Heidelberg, 1999. - Vol. 1662. -P. 194-200.

11. Nepomniaschy V.A., Argirov V.S., Beloglazov D.M., Bystrov A.V., Churina T.G., Mashukov M.Yu., Novikov R.M. Modeling and verification of SDL specified distributed systems using high-level Petri nets // Proc. 13th Intern. Workshop "Concurrency, Specification and Programming", Berlin, 2004. - Humboldt University, Berlin. - Informatik-Bericht 170. -P. 100-111.

12. Nepomniaschy V.A., Alekseev G.I., Argirov V.S., Beloglazov D.M., Bystrov A.V., Chetvertakov E.A., Churina T.G., Mylnikov S.P., Novikov R.M, Application of Modified Coloured Petri Nets to Modeling and Verification of SDL Specified Communication Protocols // Proc. 2-nd Intern. Symp. on Computer Science in Russia, Ekaterinburg, 2007. Lecture Notes in Computer Science. Springer Berlin / Heidelberg, 2007. - Vol. 4649. - P. 303314.

Публикации в трудах отечественных конференций:

13. Быстров А.В. 8 Сетевые средства синхронизации процессов // Тр. Всесоюзного научно-технического семинара "Программное обеспечение многопроцессорных систем". - Калинин, 1985. - С. 44-46.

14. Бульонков М.А., Быстров А.В., Дудоров Н.Н., Касперович Д.А., Чурина Т.Г. Опыт реализации языка параллельного программирования БАРС // Тр. 1-ой Всесоюзной конференции "Проблемы создания суперЭВМ, супер-систем и эффективность их применения". - Минск, 1987. -Ч. I. - С. 113-114.

15. Непомнящий В.А., Алексеев Г.И., Быстров А.В., Мыльников С.П., ОкунишниковаЕ.В., П.А. Чубарев П. А., Чурина Т.Г. Верификация коммуникационных протоколов, представленных на языках Estelle и SDL //Тр. 4-ого сибирского конгресса "Прикладная и индустриальная математика". - Новосибирск: Институт математики СО РАН, 2000. - С. 123.

16. Непомнящий В.А., Алексеев Г.И., Аргиров B.C., Быстров А.В., Мыльников С.П., Новиков P.M., Чурина Т.Г. Моделирование и верификация коммуникационных протоколов, представленных на языке SDL, с помо-

щью сетей Петри высокого уровня // Тр. 1-ой Всероссийской научной конференции "Методы и средства обработки информации". - Москва: МГУ, 2003. - С. 454-460.

17. Непомнящий В.А., Алексеев Г.И., Аргиров B.C., Белоглазов Д.М., Быстров A.B., Машуков М.Ю., Москвин С.О., Мыльников С.П., Новиков P.M., Семенов И.А., Четвертаков Е.А., Чурина Т.Г. Программный комплекс SPV для симуляции, анализа и верификации SDL спецификаций коммуникационных протоколов // Тр. 2-ой Всероссийской научной конференции "Методы и средства обработки информации". - Москва: МГУ, 2005. - С. 407-413.

Публикации в сборниках научных трудов и монографии:

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

19. Быстров A.B., Дудоров H.H., Котов В.Е. О базовом языке системы МАРС // Сб.: Языки и системы программирования. - Новосибирск: ВЦ СО АН СССР, 1979. - С. 85-106.

20. Быстров A.B., Городняя Л.В., Дудоров H.H. Основные черты базового языка // Высокопроизводительные вычислительные системы. - Т. 11. - Москва: ИПУ АН СССР, 1981. - С. 32-38.

21. Быстров A.B., Городняя Л.В., Котов В.Е. Сетевой подход к преобразованию программ и процессов // Сб.: Оптимизация и преобразование программ. - Ч. 1. - Новосибирск: ВЦ СО АН СССР, 1983. - С. 114-222.

22. Быстров A.B., Городняя Л.В. Обработка исключительных ситуаций в асинхронных программах // Сб.: Теоретические и прикладные вопросы параллельной обработки информации. - Новосибирск: ВЦ СО АН СССР, 1984. - С. 91-99.

23. Бульонков М.А., Быстров A.B., Дудоров H.H. Сети с синхронизацией - функционирование и корректность // Сб.: Теория программирования и средства описания параллельных дискретных систем. -Новосибирск: ВЦ СО АН СССР, 1985. - С. 115-127.

24. Бульонков М.А., Быстров A.B., Дудоров H.H., Касперович Д.А., Чурина Т.Г. Опыт реализации языка параллельного программирования БАРС на ЭВМ последовательной архитектуры // Сб.: Вычислительные системы и программное обеспечение. - Новосибирск: ВЦ СО АН СССР, 1986. - С. 78-88.

25. Бульонков М.А., Быстров A.B., Дудоров H.H., Касперович Д.А., Чу-

рина Т.Г. Система программирования на базе языка параллельного программирования Барс // Сб.: Архитектура и программное обеспечение многопроц. выч.комплексов. - Новосибирск: ВЦ СО АН СССР, 1988. -С. 98-104.

26. Алексеев Г.И., Быстров A.B., Мыльников С.П., Реализация системы проектирования сетевых моделей в MS-WINDOWS // Сб.: Проблемы теоретического и экспериментального программирования. - Новосибирск: ВЦ СО АН СССР, 1993. - С. 73-80.

27. Alekseev G.I., Bystrov A.V., Churina T.G., Mylnikov S.P. Petri-net based environment for the specification, analysis and simulation of concurrent systems // Specification, Verification and Net Models of Concurrent Systems. - Novosibirsk: IIS SB RAS, 1994. - P. 116-127.

Прочие:

28. Бульонков M.A., Быстров A.B., Дудоров H.H., Котов B.E. Базовый язык параллельного программирования для многопроцессорных систем БАРС. (Описание языка) // Алгоритмы и программы. - № 4(61). -Москва: ВМТМ Центр, 1984. - С. 23-25.

29. Бульонков М.А., Быстров A.B., Дудоров H.H., Котов В.Е. Предварительное описание языка Барс // Препринт ВЦ СО АН ССР. - № 556. - Новосибирск: ВЦ СО АН ССР, 1985. - 44 с.

30. Быстров A.B. Структурный анализ поведения непрерывно-временных сетей Петри // Препринт ИСИ СО РАН ССР. - № 137. - Новосибирск: ИСИ СО РАН. - 2006. - 30 с.

Подписано в печать Формат бумаги 60x84 1/16 Тираж 100 экз.

Центр оперативной печати "Оригинал 2" г.Бердск, ул. Островского, 55, оф. 02, тел. (383) 214 45 35

__.__.2008.

Усл. печ. л. 1 Заказ

Введение

1 Модели СП и инструментальные средства, поддерживающие СП

1.1 Основные определения теории СП.

1.2 Свободные СП.

1.3 Регулярные и иерархические СП.

1.3.1 Алгебра регулярных сетей

1.3.2 Иерархические сети

1.4 Временные СП.

1.4.1 Дискретно-временные СП.

1.4.2 Непрерывно-временные СП.

1.5 Раскрашенные СП.

1.5.1 Неиерархические раскрашенные сети Петри

1.5.2 Временные раскрашенные СП

1.5.3 Раскрашенные СП с приоритетами.

1.5.4 Иерархические раскрашенные СП.

1.6 Обсуждение возможностей инструментальных средств, поддерживающих сетевые модели

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

2.1 Структуры управления.

2.2 Типы управления.

2.2.1 Описание типов управления.

2.2.2 Программирование с типами управления.

2.3 Базовый язык асинхронного параллельного программирования Барс.

2.4 С-язык.

2.5 Программная симуляция иерархических сетей с ожиданием

3 Анализ временных сетевых моделей посредством системы RT-MEC

3.1 Структурный анализ ВСП

3.1.1 Теоретическое обоснование.

3.1.2 Анализ живости НВСП.

3.1.3 Анализ на основе ^-компонент.

3.1.4 Анализ на основе Т-компонент.

3.2 Семантический анализ ВСП.

3.2.1 Семантика ДВСП в терминах временных первичных структур событий.

3.2.2 Семантика НВСП в терминах временных локальных структур событий.

3.3 Концепции, организация и возможности системы RT-MEC

3.3.1 Структура и функции.

3.3.2 Реализация и эксперименты.

4 Проектирование, симуляция и валидация иерархических временных раскрашенных сетевых моделей посредством системы XNES

4.1 ИВТ-сети.

4.2 Особенности структурной и функциональной организации системы XNES.

4.2.1 Графический редактор.

4.2.2 Симулятор

4.2.3 Трассировщик

4.2.4 Визуализатор.

4.2.5 Подключаемые модули (плагины)

4.2.6 Эксперименты

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

Сети Петри — одна из наиболее популярных моделей параллельных систем, используемых как для теоретических исследований, так и практических применений в различных областях — распределенных баз данных и операционных систем, архитектур вычислительных машин, систем и сетей, систем программного обеспечения, протоколов коммуникаций, семантики параллельных языков, систем с элементами искусственного интеллекта и т.д. Модели сетей Петри играют такую же важную роль в изучении параллельных систем, что и конечные автоматы для последовательных. К достоинствам сетей Петри относятся наглядное графическое представление их структуры и эффективные методы анализа их поведения. В течение четырех последних десятилетий теория сетей Петри породила большое разнообразие моделей, теорем, алгоритмов и инструментов, предназначенных для спецификации, разработки и верификации параллельных/распределенных систем. Складываются устойчивые системы базовых понятий и общепринятых методик, появляются специальные периодические издания, регулярно проводятся научные конференции, посвященные данной тематике. С помощью сетевых моделей установлен ряд фундаментальных фактов, которые позволили лучше понять природу параллельных вычислений. Так, выделены три базовых отношения между событиями параллельных систем: причинная зависимость, параллелизм и недетерминированный выбор (конфликт). С одной стороны, дальнейшее продвижение в данной области связано с изучением обоснованных с теоретической точки зрения подклассов сетевых моделей (например, элементарных сетевых систем (elementary net systems), систем с условиями/событиями (condition/event systems), сетей со свободным выбором (free choice nets), позволяющих рассматривать сети Петри как математические объекты и формально исследовать их свойства, правила конструирования и преобразования. С другой стороны, появились различные расширения сетей Петри: разнообразные модели временных и стохастических сетей, сети с предикатами (predicate/transition nets), сети Петри с раскрашенными фишками (coloured Petri nets) и т. д., призванные служить математическим инструментом для моделирования и анализа реальных параллельных систем со сложной структурной организацией. Кроме того, в настоящее время также разрабатывается целый ряд инструментальных систем, основанных на моделях сетей Петри.

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

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

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

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

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

3. развитие и совершенствование методов исследования взаимосвязей различных поведенческих моделей и моделей реального времени в семантике "истинного параллелизма";

4. эффективный анализ, моделирование и валидация иерархических и временных расширений моделей СП.

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

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

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

• язык управления функционированием параллельных асинхронных программ,

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

• алгоритмы структурного и семантического анализа систем реального времени, представленные временными сетями Петри,

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

Практическая значимость. Результаты диссертации были успешно реализованы в рамках транслятора языка параллельного программирования Барс, а также экспериментальных систем XNES (extensible NEtworks Simulator) и RT-MEC (Real-Time Model and Equivalence Checker), которые поддерживают различные методы проектирования, анализа, валидации сложных распределенных систем и систем реального времени, представленных различными сетевыми моделями.

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

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

Представление работы. Основные идеи и конкретные результаты диссертационной работы обсуждались на следующих международных научных симпозиумах, конференциях и семинарах: 2-й Международный симпозиум по информатике в России (Екатеринбург, 2007). 13th Intern. Workshop " Concurrency: Specification and Programming" (Berlin, 2004); 1-ая и 2-ая Всероссийская научная конференция "Методы и средства обработки информации" (Москва: МГУ, 2003, 2005); 4-ый Сибирский Конгресс "Прикладная и Индустриальная Математика" (Новосибирск, 2000); Международный семинар "Распределенная обработка информации" (Новосибирск, 1998); 1st Intern. Workshop "Formal Description Technique, ESTELLE'98" (Evry, France, 1998);

Intern. Workshop "Discrete Event Systems" (Cagliari, Italy, 1998); Intern. Conference "Parallel Computing in Electrical Engineering" (Bialystok, Poland, 1998); 3rd Intern. Conference "Parallel Computing Technologies" (St. Petersburg, Russia, 1995, 1999); 1-ая Всесоюзная конференция "Проблемы создания супер-ЭВМ, супер-систем и эффективность их применения (Минск, 1987))"; 4th Int. Conference of Young Computer Scientists (Bratislava, 1984);

Кроме того, доклады по теме работы были сделаны на ряде семинаров Института информатики Университета г. Хильдесхайма (Германия), Института прикладной математики (г. Гренобль, Франция), Института кибернетики (г. Киев), Института программных систем РАН (г. Переславль-Залесский), Института математики СО РАН (г. Новосибирск), Института систем информатики СО РАН (г. Новосибирск), кафедр Новосибирского государственного университета и др.

Публикации. По теме диссертации опубликовано 30 научных работ, в том числе 3 в изданиях, рекомендуемых ВАК РФ; 1 монография; 9 в трудах международных симпозиумов, конференций и семинаров; 5 в трудах национальных симпозиумов, конференций и семинаров; 9 в сборниках научных трудов.

Участие в проектах и грантах. Результаты исследований, изложенные в диссертации, легли в основу ряда научно-исследовательских проектов, поддержанных в разные годы различными грантами Российского фонда фундаментальных исследований (гранты 93-01-00986, 96-01-01655, 00-01-00898, 03-07-90331, 07-07-00173), Фондом фирмы Фольксваген (грант 1/70 564), Фондом ИНТАС (грант 1010-СТ93-0048), Фондом ИНТАС-РФФИ (грант 95-0378) и др.

Личный вклад. Диссертация содержит результаты работ, выполненных автором в Вычислительном центре СО РАН с 1974 по 1990 гг. и в Институте систем информатики СО РАН с 1990 по 2008 гг.

Во всех работах опубликованных в соавторстве автор участвовал в постановке задач, разработке методов решения и анализе результатов. Также в работах [8,10,11,1317] диссертантом предложены синтаксис и семантика подъязыка управления языка Барс, алгоритмы управления вычислениями и программно реализованы соответствующие компоненты транслятора и симулятора. Результаты, изложенные в работах [6,44,45] получены автором самостоятельно, за исключением того, что разработка структуры и функций системы RT-MEC была выполнена совместно с И.Б. Вирбиц-кайте. В работах [1,24-29,33,90-94] диссертант принимал участие в создании модели ИВТ-сетей, им сформулированы требования и разработана архитектура программных комплексов XNES/SPV; он также участвовал в их программной реализации и отладке. Работы [9,7,12] написаны в неделимом соавторстве.

Структура и объем работы. Диссертация состоит из введения, четырех глав, заключения, списка литературы и приложения. Общий объем диссертации 136 е., основной текст - 126 е., приложение - 10 е., библиографический список - 121 наименование. Работа содержит 36 рисунков и 11 таблиц.

Основные результаты главы

• Разработан и реализован программный комплекс XNES (eXtended Net Editor , and Simulator), предназначенный для проектирования, симуляции и валидации распределенных систем, представленных моделями ИВТ-сетей (модификациями иерархических временных раскрашенных сетей Петри). Комплекс XNES базируется на мультиплатформенном языке Python, открытой библиотеке Petri Net Kernel и открытом формате хранения PNML (Petri Net Markup Language). XNES включает следующие основные модули: графический редактор для построения сетевых моделей; симулятор для имитационного моделирования и отладки ИВТ-сетей; трассировщик для протоколирования сеанса симуляции; ви-зуализатор для построения высоко-уровневой визуализационной модели протокола; подключаемые модули (плагины) для расширения возможностей системы XNES.

• С использованием системы XNES проведены эксперименты с рядом протоколов коммуникаций с целью анализа их корректности. В частности, исследовались сетевые модели таких протоколов, как InRes, ATMR, RE и i-протокол.

Заключение

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

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

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

• Разработан и реализован программный комплекс XNES (extended Net Editor and Simulator), являющийся одним из основных компонент системы SPV (SDL Protocol Verifier), предназначенной для проектирования, анализа и верификации протоколов коммуникаций, представленных моделями ИВТ-сетей (модификациями иерархических временных раскрашенных сетей Петри). С помощью комплекса проведены эксперименты с рядом протоколов коммуникаций с целью анализа их корректности, включая сетевые модели таких известных протоколов, как InRes-протокол, ATMR-протокол, i-протокол и кольцевой протокола RE.

1. Алексеев Г.И., Быстров А.В., Мыльников С.П., Реализация системы проектирования сетевых моделей в MS-WINDOWS // Сб.: Проблемы теоретического и экспериментального программирования. Новосибирск: ВЦ СО АН СССР, 1993. - С. 73-80.

2. Ачасова С.М., Бандман O.JI. Корректность параллельных вычислительных процессов. Новосибирск: Наука, 1990. - 252с.

3. Быстров А.В. Синхросети средство описания взаимодействия асинхронных процессов // Proc. 4th International Conference of Young Computer Scientists. - Bratislava, 1984. - P. 52-56.

4. Быстров А.В. Сетевые средства синхронизации процессов // Тр. Всесоюзного научно-технического семинара "Программное обеспечение многопроцессорных систем". Калинин, 1985. - С. 44-46.

5. Быстров А.В. Структурный анализ поведения непрерывно-временных сетей Петри // Препринт ИСИ СО РАН ССР. № 137. - Новосибирск: ИСИ СО РАН, - 2006. - 30 с.

6. Быстров А.В., Вирбицкайте И.Б. Автоматический анализ и верификация распределенных систем реального времени // Труды 6-ого межд. семинара "Распределенная обработка информации" (РОИ'98 & DDP'98). Новосибирск: Изд-во СО РАН, 1998. - С. 236-240.

7. Быстров А.В., Городняя JI.B. Обработка исключительных ситуаций в асинхронных программах // Сб.: Теоретические и прикладные вопросы параллельной обработки информации. Новосибирск: ВЦ СО АН СССР, 1984. -С. 91-99.

8. Быстров А.В., Городняя Л.В., Дудоров Н.Н. Основные черты базового языка // Высокопроизводительные вычислительные системы. Т. 11. - Москва: ИПУ АН СССР, 1981. - С. 32-38.

9. Быстров А.В., Городняя JI.B., Котов В.Е. Сетевой подход к преобразованию программ и процессов // Сб.: Оптимизация и преобразование программ. Ч. 1. - Новосибирск: ВЦ СО АН СССР, 1983. - С. 114-222.

10. Быстров А.В., Дудоров Н.Н., Котов В.Е. О базовом языке системы МАРС // Сб.: Языки и системы программирования. Новосибирск: ВЦ СО АН СССР, 1979. - С. 85-106.

11. Бульонков М.А., Быстров А.В., Дудоров Н.Н., Котов В.Е. Базовый язык параллельного программирования для многопроцессорных систем БАРС. (Описание языка) // Алгоритмы и программы. № 4(61). - Москва: ВМТМ Центр, 1984. - С. 23-25.

12. Бульонков М.А., Быстров А.В., Дудоров Н.Н. Сети с синхронизацией -функционирование и корректность // Сб.: Теория программирования и средства описания параллельных дискретных систем. Новосибирск: ВЦ СО АН СССР, 1985. - С. 115-127.

13. Бульонков М.А., Быстров А.В., Дудоров Н.Н., Котов В.Е. Предварительное описание языка Барс // Препринт ВЦ СО АН ССР. № 556. - Новосибирск: ВЦ СО АН ССР, 1985. - 44 с.

14. Бульонков М.А., Быстров А.В., Дудоров Н.Н., Котов В.Е. Базовый язык параллельного программирования Барс // Программирование. 1986. - № 6. -С. 32-40.

15. Вирбицкайте И.Б., Покозий Е.А. Метод параметрической верификации поведения временных сетей Петри // Программирование. 1999. - № 4. - С. 16-29.

16. Вишневский Ю.Л., Котов В.Е., Марчук А.Г. Модульная асинхронная развиваемая система // Кибернетика. 1984, № 3. - С. 22-29.

17. Зайцев С. С. Описание и реализация протоколов сетей ЭВМ. М.: Наука, 1989.

18. Котов В.Е. Модель асинхронных параллельных вычислений и ее языковая и архитектурная реализация // Диссертация на соискание ученой степени доктора физико-математических наук, Новосибирск. - 1980. - 343 с.

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

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

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

22. Сузи P. Python в подлиннике (+ CD-ROM) / Издательство: BHV. Серия: В подлиннике, 2002. 768 с.

23. Specification, verification and net models of concurrent systems. Novosibirsk: IIS SB RAS, 1994. - R 116-127.

24. Akaza M., Lee D., Kumagai S. Optimal cycle time and facility utilisation of production systems including repetitive process with set-up time modelled by time marked graphs // IEICE Transactions. 1992. - Vol. E75-A(10).

25. Alur R., Courcoubetis C., Dill D. Model-checking for real-time systems // Proc. 5th Symp. Logic in Comput. Sci. 1990. - P. 414-425.

26. Alur R., Courcoubetis C., Halbwachs N., Dill D., Wong-Toi H. Minimization of timed transition systems // Lect. Notes Comput. Sci. 1992. - Vol. 630. - P. 340-354.

27. Alur R., Dill D. The theory of timed automata // Lecture Notes in Computer Science. Vol. 600. - 1991. - P. 45-73.

28. Aura Т., Lilius J. Time processes for time Petri nets // Lecture Notes in Computer Science. 1997. - Vol. 1248. - P. 136-155.

29. Bause F., Kabutz H., Kemper P., Kritzinger P. SDL and Petri net performance analysis of communicating systems // Proc. IFIP 15th Intern. Symp. on Protocol Specifi-cation, Testing and Verification. Warsaw, Poland. - 1995. - P. 259-272.

30. Berthomieu В., Diaz M. Modelling and verification of time dependent systems using time Petri nets // IEEE Transaction on Software Engineering. 1991. -Vol. 17, N 3. - P. 259-273.

31. Best E., Grahlmann B. PEP more than a Petri Net tool // Lecture Notes in Computer Science. - 1996. - Vol. 1055. - P. 397-401.

32. E. Best, R.P. Hopkins. B(PN)2 a basic Petri Net Programming Notation. Lecture Notes in Computer Science. - Vol. 694. - 1993. - P. 379-390.

33. Budkowski S., Dembinski P. An introduction to Estelle: a specification language for distributed systems // Computer Networks. 1988. - Vol. 14. - P. 3-23.

34. Bystrov A.V., Virbitskaite, I.B. RT-Mec: a Tool for Validation and Verification of Petri Nets with Time Parameters // Proc. International Workshop on Discrete Event Systems. Cagliari (Italy), 1998. The IEE Publisher, London. - P. 510-514.

35. Bystrov A.V., Virbitskaite I.B. Implementing Model Checking and Equivalence Checking for Time Petri Nets by the RT-MEC Tool // Lecture Notes in Computer Science. 1999. - Vol. 1662. - P. 194-200.

36. Cherkasova L. A., Kotov V. E. Descriptive and analytical process algebras // Lecture Notes in Computer Science. 1989. - Vol. 424. - P. 77-104.

37. Чурина Т. Г., Аргиров В. С. Моделирование спецификаций языка SDL с помощью ИВТ-сетей. Препринт ИСИ СО РАН. № 124. - Новосибирск, 2005. -62 с.

38. Cohen, R., Segall, A.: An efficient reliable ring protocol // IEEE Transactions on Communications. Vol. 39 (11). - 1991. - P. 1616-1624.

39. Churina T. G., Okunishnikova E. V. Coloured Petri nets approach to the validation of Estelle specifications // Proc. Workshop on Concurrency, Specification and Programming. Warsaw, Poland, 1997. - P. 25-36.

40. Clarke E., McMillan K., Campos S., Hartonas-Gramhausen V. Symbolic Model Checking. Lecture Notes in Computer Science. Vol. 1102. - 1996. - P. 285-268.

41. Cohen R., Segall A. An efficient reliable ring protocol // IEEE Transact. Com-muns. 1991. - Vol. 39, N. 11. - P. 1616-1624.

42. Commoner F., Holt A.W., Even S,, Pnueli A. Marked Directed Graphs // Journal of Computer and System Sciences. 1990. - Vol. 5. - P. 511-527.

43. Desel J., Esparza J. Free-choice Petri nets // Cambridge Tracts in Theoretical Computer Science. 1995. - Vol. 40.

44. Dimitrov V., Petkov A. Verification oriented Estelle specification of communication protocols // Reseach into Networks and Distributed Applications. Amsterdam: North-Holland. - 1988. - P. 953-960.

45. Emersen E., Sistla A. Symmetry and model Checking // Lecture Notes in Computer Science. 1993. - Vol. 697. - P. 463-478.

46. Esparza J. Model checking using net unfoldings // Science of Computer Programming. 1994. - Vol. 23. - P. 151-195.

47. Esparza J., Silva M. A polinomial time algorithm to decide liveness of bounded free choice nets // Theoretical Computer Science. 1992. - Vol. 102(1).

48. Ferenc В., Hogrefe D., Sarma A. SDL with applications from protocol specification.- Englewood Cliffs, NJ: Prentice Hall, 1991.

49. Feldbrugge F. Petri net tools overview 1992 // Lecture Notes in Computer Science.- 1993. Vol. 674. - P. 169-209.

50. Ferenc В., Hogrefe D., Sarma A. SDL with applications from protocol specification // Prentice Hall, 1991.

51. Fernandez J.-C., Mounier L. 'On the fly' verification of behavioral equivalences and preorders // Lecture Notes in Computer Science. 1991. - Vol. 577. - P. 181-191.

52. Fisher J.,Dimitrov E. Verification of SDL'92 specifications using extended Petri nets // Proc. IFIP Fifteenth Intern. Conf. on Protocol Specification, Testing and Verification. Warsaw, 1995. - P. 455-458.

53. Fleischhack, H., Grahlmann, В.: A compositional Petri net semantics for SDL. Lecture Notes in Computer Science. Vol. 1420. - 1998. - P. 144-164.

54. Genrich H. J. Predicate/transition Nets // Lecture Notes in Computer Science. -Vol. 254. 1987. - P. 207-248.

55. Ghezzi C., Mandrioli D., Moraska S., Pezze M. A general way to put time in Petri nets // Proc. 5th Internat. Workshop on Software Specification and Design. -Pittsburg, Pennsylvania. May 1989. - P. 60-67.

56. Godefroid P. Partial-order methods for the verification of concurrent systems. An approach for state-explosion problem // Lecture Notes in Computer Science. -1996. Vol. 1032. - 143 p.

57. Grahlmann, В.: Combining Finite Automata. Parallel Programs and SDL using Petri Nets. Lecture Notes in Computer Science. Vol. 1384. - 1998. - P. 102-117.

58. Hansen P.B. Concurrent Programming Concepts // Computing Surveys. Vol. 5, No 4. - 1979.

59. Henzinger T.A., Manna Z., Pnueli A. Timed transition systems // Lecture Notes in Computer Science. 1991. - Vol. 600. - P. 226-251.

60. Holzmann G. I. Design and validation of computer protocols j j Englewood Cliffs, NJ: Prentice Hall. - 1991.

61. Hoogers P.W., Kleijn H.C.M., Thiagarajan P.S. An event structure semantics for general Petri nets // Theor. Comput. Sci. 1996. - Vol. 153. - P. 129-170.

62. Husberg, N., Manner, Т.: Emma: Developing an Industrial Reachability Analyser for SDL // Lecture Notes in Computer Science. Vol. 1708. - 1999. - P. 642-661.

63. Imai, K., Ito, Т., Kasahara, H., Morita, N.: ATMR: Asynchronous transfer mode ring protocol // Computer Networks and ISDN Systems. Vol. 26. - 1994. - P. 785-798.

64. Information Processing Systems Open Systems Interaction - ESTELLE: A Formal Description Technique Based on an Extended State Transition Model: Iner-national standard. - 1989. - ISO 9074.

65. Jensen К. Coloured Petri nets: A high level language for system design and analysis // Lecture Notes in Computer Science. Vol. 483. - 1991. - P. 343-416.

66. Jensen K. Coloured Petri nets. Springer-Verlag. - Vol. 1,2,3. - 1996.

67. Jensen K., Kristensen L., Wells L. Coloured Petri Nets and CPN Tools for modelling and validation of concurrent systems // Int. Journal on Software Tools for Technology Transfer. 2007. - Vol. 9, N. 3. - P. 213-254.

68. Kaivola R. Using Compositional preorders in the Verification of Sliding Window Protocol // Lecture Notes in Computer Science. Vol. 1254. - 1997. - P. 48-59.

69. Kindler E., Weber M. The Petri Net Kernel. Documentation of the Application Interface // http://www2.informatik.hu-berlin.de/top/pnk/literatur/PNK-Doc-engl.ps

70. Kozura V.E., Nepomniaschy V.A., Novikov R.M. Verification of distributed systems modeled by high-level Petri nets // Proc. Intern. Conf. on Parallel Computing in Electrical Engineering. Warsaw, Poland, IEEE Сотр. Society (2002) 61-66.

71. Kristensen, L.M., Christensen, S., Jensen, K.: The practitioner's guide to coloured Petri nets // Internat. J. Software Tools for Technology Transfer 2 (2) (1998) 98132

72. Lai R., Jirachiefpattana A. Verifying Estelle protocol specifications using numerical Petri nets // Comput. Syst. Sci & Eng. 1996. - Vol. 11, N. 1. - P. 15-33.

73. Lauer P.E., Campbell R.H. Formal Semantics for a Class of High-Level Primitives Coordinating Concurrent Processes // Acta Informaticaio N 5. - 1975. - P. 297-332.

74. Marsan M. A. Stochastic Petri nets: elementary introduction // Lecture Notes in Computer Science. Vol. 424. - 1989. - P. 1-29.

75. Merlin P., Faber D. J. Recoverability of communication protocols // IEEE Trans, of Communication. 1976. - Vol. COM-24(9).

76. McMilan, K. Using unfolding to avoid the state explosion problem in the verification of asynchronous circuits // Lecture Notes in Computer Science. Vol. 663. - 1992. - P. 164-177.

77. Nepomniaschy V.A., Alekseev G.I., Bystrov A.V., Churina T. G., Mylnikov S. P., Okunishnikova E. V. Petri net modelling of Estelle-specified communication protocols // Lecture Notes in Computer Science. 1995. - Vol. 964. - P. 94-108.

78. Nepomniaschy V.A., Alekseev G.I., Bystrov A.V., Churina T.G., Mylnikov S.P., Okunishnikova E.V. EPV — Petri Net Based Estelle Protocol Verifier // Proc. 1st Intern. Workshop on the Formal Description Technique Estelle. France, Evry, 1998. - P. 101-108.

79. Nielsen, M. Rozenberg, G. Thiagarajan, P.S. Behavioural notions for elementary net systems // Distributed Computing. 1990. - Vol. 4, No. 1. - P. 45-57.

80. Peng, H., Tahar, S., Khendek, F. SPIN vs. VIS: A case study on the formal verification of the ATMR protocol / Proc. 3rd Intern. Conf. on Formal Engineering Methods. IEEE Сотр. Society (2000) 79-87

81. Petri C. Concurrency // Lecture Notes in Computer Science. Vol. 84. - 1980. -P. 261-276.

82. Ramchandani C. Analysis of asynchronous concurrent systems by timed Petri nets // PhD Thesis. MIT TR-120. Cambridge (Mass). 1974.

83. Reisig W. Petri Nets: An Introduction // EATCS Monographs on Theoretical Computer Science. 1985. Vol. 10.

84. Richier J, L., Rodriguez C., Sifakis J., Voiron J. Verification in XESAR of the Sliding Window protocol // Proc. 7th IFIP Int. Symp. on Protocol Specification, Testing and Verification. 1987. - P. 235-248.

85. Rozenberg G., Thiagarajan P, S. Petri Nets: Basic Notions, Structure, Behaviour. Lecture Notes in Computer Science. Vol. 224. - 1986. - P. 585-668.

86. Roux J.-L,, Berthomieu B. Verification of local area network protocol with Tine, a software package for time Petri nets // Proc. 7th Europ. Workshop on Application and Theory of Petri Nets, 1986. P. 183-205.

87. Sifakis J. Performance evaluation of systems using nets // Lecture Notes in Computer Science. Vol. 84. - 1981. - P. 307-320.

88. Schneider S., Davies J., Jackson D.M., Reed G.M., Reed J.M., Roscoe A.W. Timed CSP: theory and practice // Lecture Notes in Computer Science. Vol. 600. -1991. - P. 640-675.

89. Specification and Description Language (SDL). Recommendation, Z.100, CCITT. -1992.

90. Starke P. Some properties of timed nets under the earliest firing time // Lecture Notes in Computer Science. Vol. 424. - 1990. - P. 418-432.

91. Starke P. INA: Integrated net analyzer. Handbuch, 1992.

92. Stenning N. V. A data transfer protocol // Computer Networks. 1976. - Vol. 1, N. 2. - P. 99-110.

93. H. Storrle. Tool Comparison, Manuscript, 1998.

94. Thiagarajan P. S. Elementary net systems. Lecture Notes in Computer Science. -Vol. 254. 1987. - P. 26-59.

95. Trompedeller M. Petri net tools, 1993. Last update: 1995, www.dsi.unimi.it/Users/Tesi/trompede/petri/alfa.html.

96. Valero V., de Frutos D., Cuartero F. Timed processes of timed Petri nets // Lecture Notes in Computer Science. Sci. 1995. - Vol. 935. - P. 490-509.

97. Varpaaniemi K., Halme J., Hiekkanen K., Pyssysalo T. PROD Reference Manual // Technical Report В 13. University of Helsinki. - 1995.

98. I.В. Virbitskaite. Characterizing time net processes categorically // Lecture Notes in Computer Science. Vol. 2127. - 2001. - P. 128-141.

99. Virbitskaite I.В., Pokozy E.A. A partial order method for the verification of time Petri nets // Lecture Notes in Computer Science. 1999. - Vol. 1684. - P. 547-558.

100. Wang F. Timing behavior analysis for real-time systems // Proc. 10th Symp. Logic in Comput. Sci, 1995, P. 112-122.

101. Wikarski D. Petri Net Tools a Comparative Study // Technical Report 97-4. -TU Berlin. - 1997.

102. Yoneda Т., Shibayama A., Schlingloff B.H., Clarke E.M. Efficient verification of parallel real-time systems // Lecture Notes in Computer Science. 1993. - Vol. 697. - P. 321-333.

103. Weber M., Kindler E. The Petri net markup language, Petri Net Technology for Communication Based Systems // Lecture Notes in Computer Science. 2003. -Vol. 2472. - P. 124-144.