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

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

СПЕЦИФИКАЦИЯ И АНАЛИЗ РАСПРЕДЕЛЕННЫХ СИСТЕМ

С ИСПОЛЬЗОВАНИЕМ ИНСТРУМЕНТАЛЬНЫХ СРЕДСТВ,

ПОДДЕРЖИВАЮЩИХ МОДЕЛИ СЕТЕЙ ПЕТРИ

05.13.11 математическое и программное обеспечение

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

АВТОРЕФЕРАТ

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

Новосибирск – 2008

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

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

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

доктор технических наук, Глинский Б.М.

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

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

Лаврентьева,

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

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

Ученый секретарь специализированного совета К 003.032. к.ф.-м.н. Мурзин Ф.А.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

и в Институте систем информатики СО РАН с 1990 по 2008 гг.

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

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

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

Работа содержит 39 рисунков и 11 таблиц.

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

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

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

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

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

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

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

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

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

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

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

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

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

Для разрешения таких конфликтов предложена специальная процедура арбитража.

Третья глава посвящена анализу временных сетевых моделей по средством системы RT-MEC. В качестве моделей распределенных си стем реального времени рассматриваются модель дискретно-временной сети Петри (ДВСП) DT N = (P, T, F, M0, D) (с функцией D, сопоставля ющей каждому переходу целочисленную временную длительность его срабатывания) и модель непрерывно-временной сети Петри (НВСП) CT N = (P, T, F, M0, D) (с функцией D, сопоставляющей каждому пе реходу временной интервал с целочисленными границами его срабаты вания).

В разделе 3.1 разрабатываются методы структурного анализа НВСП.

Считается, что НВСП имеет корректное таймирование, если D(t1 ) D(t2 ) = для всех • t1 • t2 =.

Теорема 3.1. Пусть N = (P, T, F, M0 ) ограниченная (безопасная) СП. Тогда CT N = (N, D) ограниченная (безопасная) НВСП при лю бом корректном таймировании D.

Теорема 3.2. Пусть N = (P, T, F, M0 ) живая СП, удовлетворяющая следующим условиям: p P |p• | 1 и p, q P p• q • = любом корректном таймировании.

Теорема 3.3. Пусть CT N = (P, T, F, M0, D) живая (дивергентная, ограниченная, безопасная) НВСП с корректным таймированием. Тогда N = (P, T, F, M0 ) СП.

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

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

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

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

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

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

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

Для ДВСП устанавливается изоморфизм между множеством RSS(T ESDT N ) достижимых временных конфигураций временной пер вичной структуры T ESDT N, упорядоченным отношением смены конфи гураций (), и множеством ST P (DT N ) временных бесконфликтных сетей-процессов, упорядоченным отношением вложения ().

Теорема 3.6. Для ДВСП DT N верно, что частично-упорядоченные множества (RSS(T ESDT N ), ) и (ST P (DT N ), ) изоморфны.

Далее вводится понятие временных локальных структур событий и разрабатывается семантика "истинного параллелизма" для безопас ных НВСП. Приводится построение, позволяющее по безопасной НВСП CT N получить временную локальную структуру событий tptes(CT N ) такую, что множество seq(SF S(CT N )) последовательностей шагов НВСП, упорядоченное отношением вложения (), и множество ExecSet(tptes(CT N )) выполнений временной локальной структуры событий, упорядоченное отношением вложения (), изоморфны.

Теорема 3.7. Для НВСП CT N верно, что частично-упорядоченные множества (seq(SF S(CT N )), ) и (ExecSet(tptes(CT N ))), ) изоморф ны.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

3. Разработан и реализован программный комплекс XNES (eXtended Net Editor and Simulator), являющийся одним из основных компо нент системы SPV (SDL Protocol Verier), предназначенной для проектирования, анализа и верификации протоколов коммуни каций, представленных моделями ИВТ-сетей (модификациями иерархических временных раскрашенных сетей Петри). С помо щью комплека проведены эксперименты с рядом протоколов ком муникаций с целью анализа их корректности, включая сетевые модели таких известных протоколов, как 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 Com puter Scientists. – Bratislava, 1984. – P. 52–56.

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

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

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

7. Bystrov A.V., Virbitskaite, I.B. RT-Mec: a Tool for Validation and Verication 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., Mylnikov S.P., Okunishnikova E.V. Towards Verication of Estelle-specied 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., Mylnikov S.P., Okunishnikova E.V. EPV — Petri Net Based Estelle Protocol Verier // 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 verication of SDL specied distributed systems using high-level Petri nets // Proc.

13th Intern. Workshop ”Concurrency, Specication 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 Modied Coloured Petri Nets to Modeling and Verication of SDL Specied 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. 303– 314.

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

13. Быстров А.В. 8 Сетевые средства синхронизации процессов // Тр.

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

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

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

16. Непомнящий В.А., Алексеев Г.И., Аргиров В.С., Быстров А.В., Мыль ников С.П., Новиков Р.М., Чурина Т.Г. Моделирование и верификация коммуникационных протоколов, представленных на языке SDL, с помо щью сетей Петри высокого уровня // Тр. 1-ой Всероссийской научной конференции "Методы и средства обработки информации". – Москва:

МГУ, 2003. – С. 454-460.

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

МГУ, 2005. – С. 407–413.

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

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

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

20. Быстров А.В., Городняя Л.В., Дудоров Н.Н. Основные черты базо вого языка // Высокопроизводительные вычислительные системы. – Т.

11. – Москва: ИПУ АН СССР, 1981. – С. 32–38.

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

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

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

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

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

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

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

Прочие:

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

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

– Новосибирск: ВЦ СО АН ССР, 1985. – 44 с.

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

г.Бердск, ул. Островского, 55, оф. 02, тел. (383) 214 45