Введение к работе
Актуальность. Информационный прогресс современного индустри-ільного общества основывается на использовании параллельных и рас-тределенных систем. Чтобы успешно решать задачи анализа и верификации все более сложных систем, необходимо дальнейшее развитие \ совершенствование математических методов их исследования. Для решения этих проблем предлагались различные формальные модели и летоды, такие как автоматы и системы переходов, алгебры процессов, DCS Р.Милнера, CSP Ч.Хоара, структуры событий, истории срабатыва-шя А.Мазуркевича, деревья синхронизации и другие формализмы, а также многообразные их модификации.
Среди многих существующих методов описания и анализа парал-іельньїх систем выделился подход, который основан на использова-іии сетевых моделей, восходящих к сетям Петри (СП), впервые пве-іенньїх в 1962 г. немецким ученым Карлом Петри. Сети Петри ока-ались удобными для моделирования и анализа параллельных и рас-(ределенных систем и, в частности, параллельных процессов, средств инхронизации, блоков операционных систем и т.п. Однако возмож-юстей сетей Петри оказалось недостаточно для описания и анализа истем, функционирование которых явным образом зависит от време-:и. Для спецификации и верификации систем, работадощих в режиме еального времени, был предложен ряд временных расширений орди-арных сетей Петри. Обычные сети также мало подходят для решения адач верификации и моделирования коммуникационных протоколов -дной из активно развивающихся областей формальной верификации. [ля решения этих задач было предложено расширение сетей Петри осредством цветных фишек, которые позволяют компактно описывать ложные системы и в то же время допускают большинство существующих методов анализа. Еще одно известное расширение сетей Петри иерархические сети Петри, которые служат для моделирования ие-архических систем. В настоящее время теория сетей Петри - это сло-сившееся направление, в рамках которого рассматриваются различие версии, модификации и расширения сетей Петри, что позволяет цаптироваться под конкретную прикладную область.
Следует отметить, что п;>:і практическом применении сущестБую-[их методов и средств, разработанных на основе общепризнанных фор-альных моделей, обнаруживаются некоторые недостатки, связанные неадекватным представлением параллелизма или отсутствием нарядного графического представления. Стандартные сети Петри, со-
вмещал в себе наглядность и адекватное представление параллелизма не обладают удовлетворительными средствами композициональності-и модульности.
В середине 80-х годов польский ученый Людвиг Чайя предложи/ новый формализм - причинно-следственные структуры (ПСС),- исполь зующий преимущества сетей Петри и дающий компактное алгебраи ческое представление для анализа поведения параллельных систем Эта модель, подобная в некотором смысле сетям Петри, имеет наглядное графическое представление, но в отличие от сетей граф причинно-следственной структуры имеет только один тип вершин - узлы. Взаимосвязи между узлами указаны в двух "индексах", приписанных каждому узлу и представляющих собой совокупность подмножеств узлов, обозначающих в верхнем "индексе" группы (альтернативные одна другой) предшественников данного узла, в нижнем "индексе" - группь: преемников данного узла. Эти индексы представляются двумя формальными полиномами с операциями сложения и умножения. Операция сложения моделирует альтернативный выбор вариантов передачу или получения активности данным узлом. Операция умножения моделирует синхронизацию передачи активности различными узлами D данный узел или из данного узла в группу независимых узлов.
В последнее время модель ПСС получила развитие в ряде зарубежных работ, которые посвящены анализу структурных, динамических и композициональных свойств ПСС. Была попытка обобщить операции + и *, определенные на множестве формальных полиномов, на множестве ПСС. Но, как отмечено, в частности, в работе Маджиолли-Щеттини и Маттеуси, в порожденной таким образом алгебре ПСС возникает ряд проблем: "непредсказуемость" операции -f, порождение операцией * структурных дедлоков. Кроме того, в алгебре ПСС аксиома дистрибутивности операций сложения и умножения выполняется только при дополнительном условии. Поэтому открыта проблема построения "корректной" алгебры ПСС, что позволило бы из простейших базисных ПСС с помощью операций 4-й * конструировать произвольную ПСС.
В последующих работах Чайя исследует четыре варианта семантики ПСС и их соотношение, расширяет класс ПСС введением семантики времени в двух вариантах - с минимальным (максимальным) временем задержки (пребывания) фишки в узле. В ряде работ исследуются некоторые взаимосвязи ПСС с сетя.ми Петри и другими формальными моделями. Рашунас, исследуя соотношение стандартного класса СП с обычными ПСС, пришел к следующему выводу: каждая ПСС имеет строго эквивалентную ей СП, но обратное не верно. Таким образом,
іткрьіта проблема обратного отображонил: выделение подкласса СП їли построение расширения класса ПСС, рагзпомощного класс}' СП в смысле строгой эквивалентности.
Актуальной является задача развития математического аппарата 'еории причинно-следственных структур , в частности, важным пред-тавляется решение таких открытых проблем, как построение "коррект-юй" алгебры ПСС, различные расширения класса ПСС для лучшей іримепимости в прикладных областях. Актуальной так же лвллет-я задача установления взаимосвязей и сравнительный анализ раз-[ичных формализмов. В частности, важными открытыми проблемами вляютсл установление взаимоотношений между классами ПСС и СП, ключал такие известные раширения класса СП, как цветные, иерархи-іеские и временные СП; построение обратного отображения из класса Ж в класс ПСС.
Цель работы, состоит в дальнейшей разработке теории ПСС, по-воляющей решить открытые проблемы взаимосвязи ПСС с СП. Для .остижения указанной цели решаются следующие задачи: . Анализ проблем, возникающих в алгебре ПСС, и построение на осно-е этого анализа расширения класса ПСС, в котором решались бы про-лемы обратного отображения и "корректной" алгебры. . Построение расширений класса ПСС на семантику цветных фишек и ерархически вложенных подструктур и разработка алгоритмов, ото-ражающих полученные расширения ПСС в эквивалентные расшире-ия класса СП.
Методы исследования базируются на применении аппарата теории зтей Петри и причинно-следственных структур, методов алгебраиче-хих теорий параллельных процессов, элементов общей алгебры, тео-ии множеств.
Научная новизна работы. Проведен анализ алгебры ПСС и предложено обобщение класса СС - двухуровневые причинно-следственные структуры (ДПСС), что озволило разрешить две главные трудности, возникшие на данном гапе разработки теории ПСС, а именно-.
Построена алгебра ДПСС, замкнутая относительно операций слоения и умножения и свободная от ограничений алгебры ПСС: по-эждения дедлоков, непредсказуемости альтернативной композиции вух ПСС, ограниченности аксиомы дистрибутивности. Это позволяет ізбить процесс анализа, конструирования и преобразования структур і. несколько более простых этапов.
Показано, что для ДПСС обратное отображение из класса СП
в класс ДПСС является взаимно-однозначным и сохраняет строгугс эквивалентность. С другой стороны, класс ПСС строго эквивалентен подклассу так называемых максимальных ДПСС.
Кроме того, класс ДПСС, сохраняя компактность и композициональ-ность аналитического представления ПСС, имеет более наглядное графическое представление.
2. Важным шагом в развитии теории ПСС является построение расширений класса ПСС на семантику времени, цветных фишек и иерархически вложенных подструктур. Обобщение ПСС на семантики цветных фишек и иерархии до настоящего времени не рассматривались.
Исследовано соотношение классов временных ПСС (ВПСС) и временных СП (ВСП). Установлено, что каждая ВПСС имеет строго эквивалентную ВСП, заданную в согласованной с предложенной Чайя для ВПСС семантике времени.
В обычных ПСС фишка, или активность узла, моделирует наличие контроля и/или некоторого ресурса в узле, не выделяя при этом качественных отличий ресурсов, проходящих через узел. При этом одновременно в узле не может находиться более одного ресурса-фишки. Но бывает важно качественно различать ресурсы, функционирующие в системе. Качественное различие моделируется различными цветами, приписываемыми фишкам. При этом в узле может находиться несколько фишек, но разных цветов. Предлагается рассматривать два эквивалентных взаимодополняющих представления семантики цвета в ПСС, преобразуемых одно в другое:
-
форма представления на основе обычных узлов, но содержащих несколько цветных фишек (ЦПСС), повышающая компактность и выразительную мощность класса ПСС;
-
форма представления на основе расширенного множества раскрашенных узлов (РПСС), наглядно согласующаяся с формой представления ПСС и позволяющая применить к цветным ПСС весь математический аппарат, наработанный в теории ПСС.
- Введение семантики иерархически вложенных подструктур
(ИПСС) существенно повышает компактность представления и свой
ство композициональности класса ПСС. Рассматривается расширение
ПСС до иерархических структур по типу, предложенному для СП Кото-
вым. В иерархических сетях Котова составными объектами являются
переходы, но в ПСС соответствующие им компоненты срабатывания
явно не заданы. В ПСС есть только один тип вершин - узлы, поэтому
они и представляются как составные объекты. Это значит, что вво
дится два типа узлов: локальные - моделирующие выполнение опре-
іеленного условия или наличие определенного ресурса, и глобальные моделирующие некоторый выделенный процесс и содержащие в се->е некоторую иерархическую ПСС- Для того чтобы класс ИПСС мог >ыть сравним, в некотором смысле, с классом иерархических СП, гло-іальиьіе узлы выделяются в некий особый подкласс узлов со своими іксиомами для операций + и *.
Показана эквивалентность данных расширений ПСС известным рас-иирениям СП - раскрашенным СП в смысле Иенсона и иерархическим Ш в смысле Котова.
Практическая ценность работы заключается в разработке соответ-твующих алгоритмов, позволяющих построить автоматическую си-тему перевода, которая полезна для моделирования параллельных и іаспределенньїх систем с использованием как графических средств СП, ак и аналитической компактности ПСС.
Участие и проектах. Представленные в диссертации исследования іроцодились в рамках бюджетной темы "Исследование формальных юделей и методов описания семантики, спецификации и верифика-;ии параллельных и распределенных систем", номер гос. регистрации 1.9.60 002068; проектов Российского фонда фундаментальных исследова-ий, грант 93-01-00986; Международного научного фонда и Российского [равительства, грант JCP100; Фонда INTAS, грант 1010-СТ93-0048.
Апробация работы. Основные научные и практические результаты аботы подробно обсуждались на объединенных семинарах Институ-а систем информатики СО РАН и Новосибирского государственного ниверситета с 1993 по 1996 гг., докладывались на семинаре Институ-а программных систем (г. Переяславль-Залесский, апрель 1997) и на іеждународиой конференции "Параллелизм, спецификации и програм-:ирование" (Варшава, Польша, 1995).
Публикация результатов работы. По теме диссертации опубликова-о 7 научных работ.
Структура и объем работы. Диссертация состоит из введения, че-ырех глав, заключения и списка литературы из 42 наименований, існовное содержание составляет 92 страницы. Работа включает 14 ри-унков.
