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

РГ'8 ОД

Д ^РОССИЙСКАЯ АКЛЛЕМИЯ НАУК * СИБИРСКОЕ ОТДЕЛЕНИЕ

ИНСТИТУТ СИСТЕМ ИНФОРМАТИКИ ИМ. А.П. ЕРШОВА

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

Тарасюк Игорь Валерьевич

Эквивалентностные понятия для моделей параллельных и распределенных систем

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

сетей

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

Новосибирск 1997

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

Научные руководители:

кандидат физ.-мат. наук Вирбицкайте И.В., доктор физ.-мат. наук Поттосин И.В.

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

доктор технических наук Бандман О.Л., кандидат физ.-мат. наук Ломазова И.А.

Ведущая организация: Институт Математики СО РАН.

Защита состоится 26 декабря 1997 г. в 14 час. 30 мин. на заседании специализированного совета К0003.93.01 в Институте систем информатики им. А.П. Ершова СО РАН по адресу:

630090, г. Новосибирск, пр. акад. Лаврентьева, 6.

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

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

специализированного совета К0003.93.01

к.ф.-м.н.

Бульонков М.А.

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

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

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

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

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

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

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

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

• Очевидно значение эффективных методов редукции систем с сохранением поведения по модулю эквивалентностей.

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

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

• Разработка эквивалентностных понятий для расширений известных формальных моделей (например, понятием аб-

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

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

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

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

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

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

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

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

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

Реализация результатов работы заключается в их исполь-

зовании при создании модуля проверки сетевых эквивалент-ностей для системы PEP (Programming Environment based on Petri nets), совместно разрабатываемой Институтом информатики г. Хильдесхайма (Германия) и ИСИ СО РАН. Кроме того, автором: написана программа CANON, реализующая проверку семантической эквивалентности алгебраических формул.

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

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

1. Исследование методов анализа и верификации параллельных вычислительных систем, программ и процессов. Российский фонд фундаментальных исследований (РФФИ), грант 9301-00986, руководитель к.ф.-м.н. В.А. Непомнящий, 19931995.

2. Models for formal semantics of reactive systems. International Association for Promotion of Cooperation with Scientists from the Former Soviet Union (INTAS), грант 1010-CT93-0048, руководитель к.ф.-м.н. В.А. Непомнящий, 1993-1995.

3. Formal methods in design of concurrent / distributed systems. Volkswagen Stiftung (VS), грант 1/70 564, руководители Prof. Dr. Еже Best и к.ф.-м.н. И.Б. Вирбицкайте, 1995-1997.

4. Разработка и исследование семантических методов и средств спецификации и верификации параллельных систем и процессов. РФФИ, грант 96-01-01655, руководитель к.ф.-м.н. И.В. Вирбицкайте, 1995-1997.

5. Methods and Tools for Verification and Analysis of Distributed Systems. 1NTAS-RFBR, грант 95-0378, руководитель к.ф.-м.н. В.А. Непомнящий, 1997-1999.

6. International Soros Science Education Program (ISSEP); грант a97-683, 1997. Автору присвоено звание Соросовского Аспиранта.

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

1. 4th International Conference on Applied Logics - 95 (AL'95), Иркутск, Россия, 15-18 июня 1995.

2. 5<л Workshop on Concurrency, Specification and Programming - 96 (CSP'96), Берлин, Германия, 25-27 сентября 1996.

3. 4<л Symposium on Logical Foundations of Computer Science - 97 (LFCS'97), Ярославль, Россия, 6-12 июля 1997.

4 4f> Workshop on Logic, Languages, Information and Computation -97 (WoLLIC'97), Форталеза (Lleapa), Бразилия, 19-22 августа 1997.

Кроме того, доклады по теме работы были сделаны на ряде семинаров Института информатики г. Хильдесхайма (Германия) во время работы автора с 01.12.95 по 29.02.96 и с 01.03.97 по 30.04.97 в рамках совместного научного проекта по гранту VS 1/70 564. Полученные результаты обсуждались также на совместных семинарах кафедры программирования H ГУ и лаборатории теоретического программирования ИСИ СО РАН.

Структура и объем работы. Диссертационная работа состоит из введения, трех глав, заключения, трех приложений и списка литературы. Объем основной части работы составляет 151 страница, объем приложений и списка литературы — 40 страниц. Список литературы состоит из 293 наименований. Работа включает 90 рисунков и 1 таблицу.

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

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

Глава 1 посвящена исследованию эквивалентностей на сетях Петри.

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

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

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

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

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

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

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

По степени учета параллелизма мы различаем интерливин-говые, шаговые, частичных слов (ЧС), частично упорядоченных мультимножеств (ЧУММ) и процессные эквивалентности (в их обозначениях пишутся соответственно буквы {,в,рш,рот, рг).

Пусть *,** € {г, в,рт,рот,рг}. По степени учета конфликта мы различаем следовые (=*), обычные бисимуляционные (±±*), БТ-бисимуляционные (±±*5т)> сохраняющие историю бисимуляционные эквивалентности, а также сохраняющие

конфликт эквивалентности мультиструктур событий (МСС) (нте<), О-процессов (~осс) и изоморфизм (~).

Кроме упомянутых базисных эквивалентностей, мы рассматриваем обратные-прямые бисимуляционные эквивалентности (£±*б**/)> которые требуют взаимного моделирования систем не только в прямом, но и в обратном направлениях. Они тесно связаны с эквивалентностями логик, имеющих модальности "прошлого".

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

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

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

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

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

Рисунок 1. Эквивалентности сетей Петри с видимыми переходами

" систем. В результате выяснено, какие эквивалентностные отношения могут быть использованы при нисходящей разработке систем. Мы рассматриваем один из видов детализации — БМ-детализацию, заменяющую переходы сетей на особый подкласс автоматных сетей (БМ-сети). На рис. 1 эквивалентности, обладающие свойством сохранения при ЯМ-детализациях, помещены в овалы, причем утолщенные овалы соответствуют полученным нами новым результатам.

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

Раздел'1.3 посвящен исследованию эквивалентностей на се-

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

Пусть -к,-к* £ {г,в,рги,рот). Рассматриваются такие базисные т-эквивалентности, как т-следовые (=£), обычные т-бисимуляционные БТ-т-бисимуляционные (¿¿15т)> сохра-

няющие историю т-бисимуляционные (^±р0тд), а. также сохраняющие конфликт т-эквивалентности мультиструктур событий (МСС) (=^е,) и изоморфизм (~).

Так как сети с невидимыми переходами — более широкий класс, чем сети с видимыми переходами, возникает ряд новых базисных т-эквивалентностей (они совпадают с названными эквивалентностями на сетях с видимыми переходами). Среди них сохраняющие историю БТ-т-бисимуляционные (±±р0тА5тО> обычные (±±-Ьг) и сохраняющие историю (£±р0ТпЛЬг) ветвистые т-бисимуляционные.

Кроме упомянутых базисных эквивалентностей, мы рассматриваем обратные-прямые т-бисимуляционные эквивалентности (±±*ь**/)-

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

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

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

Исследована взаимосвязь эквивалентностей на двух подклассах сетей с невидимыми переходами: сетях с видимыми

Рисунок 2. т-еквивалентиости сетей Петри с невидимыми переходами

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

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

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

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

В разделе 2.1 даются основные определения, связанные с временными сетями.

Раздел 2.2 посвящен исследованию эквивалентностей на временных сетях с видимыми переходами.

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

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

Рассматриваются следующие временные эквивалентности: следовая (={) и бисимуляционная (*->,), не-временные: следовая (=„) и бисимуляционная (±±и), а также изоморфизм (~).

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

Проводится сравнение всех рассмотренных сетевых эквивалентностей и устанавливается полная картина их взаимосвязей, представленная на рис. 3.

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

Рисунок 3, Эквивалентности временных сетей Петри с видимыми переходами

временных систем. На рис. 3 эквивалентности, обладающие этим свойством, помещены в овалы.

Исследуется взаимосвязь эквивалентностей на на одном из подклассов временных сетей: не-временных сетях, позволяющая выявить природу этих отношений и упростить их проверку.

Раздел 2.3 посвящен исследованию эквивалентностей на временных сетях с невидимыми переходами.

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

Рассматриваются временные т-эквивалентности: г-следовая (=[) и т-бисимуляционная (<->[). не-временные: г-следовая (=£) и г-бисимуляционная (<-»„). а также изоморфизм

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

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

Все т-эквивалентности проверяются на сохранение при операции временной 8М-детализации. На рис. 4 т-эквивалентнос-ти, обладающие этим свойством, помещены в овалы.

Исследуется взаимосвязь эквивалентностей на двух подклассах временных сетей с невидимыми переходами: не-вре-менных сетях и временных сетях с видимыми переходами.

Глава 3 посвящена исследованию эквивалентностей на формулах процессных алгебр.

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

о

г

<5D

í

■ т :t!

т

Рисунок 4' т-эхвивалентности временных сетей Петри с невидимыми

пер еходами

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

В разделе 3.1 рассматривается исчисление AFP-¡.

Алгебра AFP2 (Algebra of Finite Processes), введенная B.E. Ko-товым и JI.А. Черкасовой, относится к третьей группе исчислений и основана на семантике частично упорядоченных мно-

т

-осс

\ -рг

Рисунок S. Взаимосвязь сетевых и алгебраических еквивалентностей AFLP2

жеств (ЧУМ) с не-действиями и тупиковыми действиями, с помощью которых сохраняется информация о недетерминизме. Она объединяют механизмы как для описания параллельных недетерминированных процессов, так и для исследования их свойств. Синхронизация действий в AFP2 происходит по имени, т.е. несколько одноименных действий, которые встречаются в разных частях формулы этой алгебры, синхронизируются. Считается, что этим действиям соответствует одно событие.

В литературе было показано, что средствами AFP-i можно анализировать поведение особого подкласса ациклических строго помеченных сетей — A-сетей. В данном разделе рассмотренные ранее эквивалентности изучаются на этом подклассе сетей. Семантические эквивалентности AFP% (=Df.2 и модификация этой эквивалентности, абстрагирующаяся от недействий и тупиковых действий =^,4 ) переносятся на А-сети

F3

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

Предлагается метод автоматизации проверки семантической эквивалентности формул на основе системы правил переписывания RWSi. Данный метод реализован в виде программы CANON на языке Си объемом около 3000 строк.

В разделе 3.2 вводится новое исчисление AFLP2.

Алгебра AFLP-¿ (Algebra of Finite Labelled Processes) строится на основе AFP2 с помощью введения глобальной пометки на символах событий, которые комбинируются в формулы. Таким образом, формулы алгебры AF"Lp2 описывают помеченные недетерминированные процессы, в которых два различных события могут быть помечены одним и тем же действием. В рамках ал-

-vF3 ■

=1

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

На базе помеченных частично упорядоченных множеств (ПЧУМ) в ÁFLP-i вводится денотационная семантика. На основе денотационной семантики определяются эквивалентности формул AFLP2 (=vFL2 и ее модификация абстракцией от несобытий и тупиковых событий ). Строится полная и корректная система аксиоматизация семантической эквивалентности =tvi2.

Отмечена возможность использования программы CANON для автоматизации проверки семантической эквивалентности AFLP2.

Определяется операционная семантика AFLP2 на базе системы переходов, основанной на срабатываниях ПЧУМ событий. Устанавливается соответствие между денотационной и операционной семантиками.

Показано, что средствами AFLP2 можно анализировать поведение слабо помеченных A-сетей (расширение A-сетей допуском нескольких одинаково помеченных переходов). Рассмотренные ранее эквивалентности изучены на этом подклассе сетей. Эквивалентности на формулах AFLP2 переносены на слабо помеченные A-сети и исследована их взаимосвязь с сетевыми эквивалентностями, что позволило лучше понять природу алгебраических эквивалентностей. На рис. б представлена взаимосвязь сетевых и алгебраических эквивалентностей.

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

В приложение А перенесен ряд больших по объему доказательств.

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

В приложении С приводятся примеры преобразования фор-

— Ргьа

I

—шел * —осс

1 I

——ротк -

I I

—гЭТ -- —-—ротЭТ --^гБТ

\ \ \ \

£2» ----- ±г.рхи --5Ирот -- ±1рг

\ _1 \ _1 _1

—I -— —а - —ры --рот - —рг

Рисунок 6. Взаимосвязь сетевых и алгебраических эквивалентностей АЕЬР2

мул АР Р2 к каноническому вилу с помощью этой программы.

3. ОСНОВНЫЕ РЕЗУЛЬТАТЫ И ВЫВОДЫ

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

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

опальной разработке временных параллельных систем.

3. Предложено расширение известного алгебраического исчисления AFP') функцией пометки — алгебра помеченных недетерминированных параллельных процессов AFLPn.. Дана операционная характеризация, полная и корректная аксиоматизация семантических эквивалентностей указанных алгебр. Проведено сравнение алгебраических и сетевых эквивалентностей и их перенос из одной модели в другую и обратно. Разработан и программно реализован способ автоматизации проверки формул алгебр на семантическую эквивалентность.

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

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

1. Тарасюк И.В. Приведение формул алгебры AFP2 к каноническому виду.// Проблемы теоретического и экспериментального программирования. — Новосибирск, 1993. — С. 47-59.

2. Тарасюк И.В. Исследование сетевых эквивалентностей.// Материалы 4-й Международной конференции по прикладной логике - 95 (AL'95). — Иркутск: ИГУ, 1995. — С. 74-75.

3. Тарасюк И.В. Алгебра AFLP2: исчисление помеченных недетерминированных параллельных процессов.// Проблемы спецификации и верификации параллельных систем. — Новосибирск, 1995 — С. 22-49.

4. Tarasyuk I.V. Equivalences on Petri nets.// Specification, Verification and Net Models of Concurrent Systems. — Novosibirsk, 1994. — P. 35-57.

5. TARASYUK I.V. An investigation of equivalence notions on some subclasses of Petri nets.// Balletin of the Novosibirsk Computing Center, Series Computer Science. — 1995. — Vol. .3. — P. 89100.

6. tarasyuk I.V. Equivalence notions for design of concurrent systems using Petri nets. — Hildesheim, 1996. — 19 p. — (Prepr./ Hildesheimer Informatik-Bericht; No. 4, Part 1).

7. tarasyuk I.V. Lposets with non-actions: a model for labelled non-deterministic processes. — Hildesheim, 1996. — 18 p. — (Prepr./ Hildesheimer Informatik-Bericht; No. 4, Part 2).

8. tarasyuk I.V. Petri net equivalences for design of concurrent systems./ / Proceedings of 5<A Workshop on Concurrency, Specification and Programming - 96 (CSP'96), September 25-27, 1996. — P. 190204. — (Institut für Informatik, Humboldt-Universität zu Berlin. Informatik Bericht No. 69).

9. Tarasyuk I.V. An algebra of labelled nondeterministic processes.// Joint Novosibirsk Computing Center and Institute of Informatics Systems Bulletin, Series Computer Science. — 1996. ;— Vol. 5.

— P. 75-90.

10. Tarasyuk I.V. Back-forth, equivalences for design of concurrent systems.// Eds. S. Adian, A. Nerode: Proceedings of 4"' International Symposium on Logical Foundations of Computer Science - 97 (LFCS'97), Yaroslavl, 1997. — P. 374-384. — (Lect. Notes Comput. Sei.; Vol. 1234).

a full version of this paper is: tarasyuk I.V. An investigation of back-forth and place bisimulation equivalences. — Hildesheim, 1997.

— 30 p. — (Prepr./ Hildesheimer Informatik-Bericht; No. 8).

11. Tarasyuk I.V. An investigation of r-equivalences. — Hildesheim, 1997. — 28 p. — (Prepr./ Hildesheimer Informatik-Bericht; No. 9).

12. Tarasyuk I.V. Equivalences for behavioural analysis of multilevel systems.// Joint Novosibirsk Computing Center and Institute of Informatics Systems Bulletin, Series Computer Science. — 1997. —

13. vlrbltskaíte I.B., Tarasyuk I.v. Investigating equivalence notions for time Petri nets.// Proceedings of 4th Workshop on Logic, Languages, Information and Computation (WoLLIC'97), Fortaleza (Ceará), Brazil, August 19-22, 1997. — (Logic J. of the IGPL. — 1997. — Vol. 5, No. 6).

Vol. 7.

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

18.11.97 г. Объем 1.1 уч.-изд.л.

Заказ 85.

Ротапринт ИВМ и МГ СО РАН, Новосибирск-90.