авторефераты диссертаций БЕСПЛАТНАЯ  БИБЛИОТЕКА

АВТОРЕФЕРАТЫ КАНДИДАТСКИХ, ДОКТОРСКИХ ДИССЕРТАЦИЙ

<< ГЛАВНАЯ
АГРОИНЖЕНЕРИЯ
АСТРОНОМИЯ
БЕЗОПАСНОСТЬ
БИОЛОГИЯ
ЗЕМЛЯ
ИНФОРМАТИКА
ИСКУССТВОВЕДЕНИЕ
ИСТОРИЯ
КУЛЬТУРОЛОГИЯ
МАШИНОСТРОЕНИЕ
МЕДИЦИНА
МЕТАЛЛУРГИЯ
МЕХАНИКА
ПЕДАГОГИКА
ПОЛИТИКА
ПРИБОРОСТРОЕНИЕ
ПРОДОВОЛЬСТВИЕ
ПСИХОЛОГИЯ
РАДИОТЕХНИКА
СЕЛЬСКОЕ ХОЗЯЙСТВО
СОЦИОЛОГИЯ
СТРОИТЕЛЬСТВО
ТЕХНИЧЕСКИЕ НАУКИ
ТРАНСПОРТ
ФАРМАЦЕВТИКА
ФИЗИКА
ФИЗИОЛОГИЯ
ФИЛОЛОГИЯ
ФИЛОСОФИЯ
ХИМИЯ
ЭКОНОМИКА
ЭЛЕКТРОТЕХНИКА
ЭНЕРГЕТИКА
ЮРИСПРУДЕНЦИЯ
ЯЗЫКОЗНАНИЕ
РАЗНОЕ
КОНТАКТЫ

Формальные модели и анализ корректности параллельных систем и систем реального времени

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

Вирбицкайте Ирина Бонавентуровна

ФОРМАЛЬНЫЕ МОДЕЛИ И

АНАЛИЗ КОРРЕКТНОСТИ

ПАРАЛЛЕЛЬНЫХ СИСТЕМ И

СИСТЕМ РЕАЛЬНОГО ВРЕМЕНИ

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

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

Автореферат

диссертации на соискание ученой степени

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

Красноярск, 2001

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

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

доктор физико-математических наук, профессор Добронец Б.С.

доктор технических наук, профессор Марков Н.Г.

Ведущая организация: Институт программных систем РАН (г. Переславль-Залесский)

Защита состоится “ 20 ” декабря 2001 года в 14 час. 00 мин. на за седании диссертационного совета Д 212.098.03 в Красноярском государ ственном техническом университете по адресу: 660074, Красноярск, ул.

Киренского,

С диссертацией можно ознакомиться в читальном зале библиотеки Крас ноярского государственного технического университета Автореферат разослан “ 19 ” ноября 2001 г.

Ученый секретарь специализированного совета Д 212.098. кандидат технических наук Вейсов Е.А.

Общая характеристика работы

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

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

формальные модели, алгебры процессов, логики процессов.

Среди отечественных исследований в области разработки формаль ных методов анализа параллельных систем и процессов отметим работы Н.А. Анисимова, О.Л. Бандман, В.А. Вальковского, Ю.Г. Карпова, В.Е.

Котова, Р.М. Смелянского, В.А. Соколова, Л.А. Черкасовой.

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

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

детально проработана толь ко интерливинговая семантика параллельных процессов;

отсутствуют эквивалентностные понятия, отражающие базовые отношения на собы тиях распределенных систем;

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

эффективные верификационные алгоритмы (алгоритмы проверки на моделях) разработаны только для темпораль ной логики CTL;

имеет место значительное снижение эффективности верификации из-за проблемы ‘взрыва состояний’;

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

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

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

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

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

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

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



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

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

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

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

Практическая ценность. Разработанные автором диссертации ме тоды могут лечь в основу широкого спектра промышленных программ ных систем: блоков автоматического распараллеливания в транслято рах и интерпретаторах, систем построения семантических представле ний и эквивалентных преобразований параллельных процессов, систем верификации процессов реального времени. Результаты диссертацион ной работы были успешно реализованы в рамках экспериментальной системы RT-MEC (Real-Time Model and Equivalence Checker), которая поддерживает различные методы спецификации, анализа, верификации параллельных систем и систем реального времени, представленных раз личными сетевыми моделями с временными характеристиками, и кото рая является частью системы PEP (Programming Environement based on Petri nets), совместно разрабатываемой несколькими немецкими уни верситетами (г. Хильдесхайма, г. Ольденбурга, г. Мюнхена).

Апробация работы. Основные идеи и конкретные результаты дис сертационной работы обсуждались на следующих всесоюзных и меж дународных научных симпозиумах, конференциях и семинарах: Всесо юзная школа-семинар ‘Распределенная обработка информации’ (Львов, 1987, Львов 1989);

Всесоюзная конференция ‘Однородные вычислитель ные среды и систолические структуры’ (Львов, 1990);

International Conference of Young Computer Scientists (Beijing, 1993);

International Seminar ‘Concurrency:

Specication and Programming’ (Nieborow, Poland, 1993;

Berlin 1994;

Warsaw, 1999;

Berlin, 2000);

International Conference ‘Formal Methods in Programming and their Applications’ (Novosibirsk, 1993);

A.P Ershov International Memorial Conferences on Perspectives of System Informatics (Novosibirsk, 1996;

Novosibirsk, 2001);

International Conference ‘CONPAR 94 - VAPP VI’ (Linz, Austria, 1994);

4th International Conference on Applied Logics (Irkutsk, Russia, 1995);

International Symposium on Fundamentals of Computation Theory (Krakow, Poland, 1997;

Iassy, Romania 1999;

Riga, 2001);

International Workshop on Logic, Language, Information and Computation (Fortaleza, Brazil, 1997;

Natal, Brazil, 2000);

IMACS World Congress on Scientic Computation, Modelling and Applied Mathematics (Berlin, 1997);

International Workshop on Distributed Data Processing (Novosibirsk, 1998);

International Workshop on Discrete Event Systems (Cagliari, Italy, 1998);

MFCS’98 International Workshop on Concurrency (Brno, Chezh Republic, 1998);

International Conference on Parallel Computing Technology (Sankt-Peterburg, 1999;

Novosibirsk 2001).

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

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

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

Содержание работы Во введении обосновывается актуальность рассматриваемых во просов;

формулируются цели исследований, представленных в диссер тации;

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

приводится краткое описание содержания диссертации по главам.

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

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

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

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

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

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

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

Потоковая схема (далее просто (базовая) схема) характеризуется вершинами и дугами. Вершины делятся на акторы и вершины связи.

Имеются четыре типа акторов (операторы, распознаватели, клапаны и акторы модификации тега, т.е. акторы генерации нового тега и акторы восстановления старого тега) и два типа вершин связи (информацион ные и управляющие). Дуги, соединяющие акторы с вершинами связи и вершины связи с акторами, называются информационными или управ ляющими дугами в соответствии с типом вершины связи. Потоковая схема с тегированными фишками (п-схема) CDS состоит из базовой схемы, множества информационных и управляющих фишек, множества тегов и функции тегирования фишек. Разметка п-схемы — это функ ция, сопоставляющая наборы фишек дугам так, что типы фишек совпа дают с соответствующими типами дуг. Разметка называется начальной (обозначается Min ), если для любой входной дуги п-схемы теги любых двух различных фишек, сопоставленных этой дуге, различны, а всем другим дугам фишки не сопоставлены. Пусть (CDS, Min ) обозначает начально размеченную п-схему. Интерпретация для (CDS, Min ) зада ется областью значений и сопоставлением каждому оператору функции и каждому распознавателю предиката. Определяются правила сраба тывания вершин, понятие процесса и наиболее важные поведенческие свойства (живости, безопасности, ‘очищаемости’) п-схемы.

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

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

разбиения мно жества информационных фишек на непересекающиеся подмножества:

фишек с именами массивов, фишек с индексами, фишек со значениями массивов;

аналогичного разбиения множества информационных вершин связи;

введения в множество вершин подмножества вершин обработки массивов, состоящего из непересекающихся подмножеств: вершин по рождения массивов, вершин модификации значения элемента массива, вершин выбора значения элемента массива. Определения правил сраба тывания вершин, процесса и свойств п-схемы CDS являются коррект ными и для п-схемы с массивами CDSA. Структурированная п-схема с массивами — это обобщение структурированной п-схемы путем расши рения множества примитивных схем схемами с вершинами обработки массивов. Дополнительные структурные ограничения состоят в следу ющем: для каждого имени массива существует не более одной верши ны модификации значения в массиве. В теореме 1.2.2 устанавливается, что структурированная п-схема с массивами является бесконфликтной, живой, ‘очищаемой’.





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

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

В разделе 1.3 обсуждается проблема использования и реализации конструкций традиционных императивных языков на потоковых ЭВМ.

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

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

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

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

В алгоритме A2, осуществляющем преобразование ациклической с схемы SS в потоковый вид, элиминации подлежат только логически узловые распознаватели. Для каждого логически узлового оператора определяется множество LP распознавателей, от которых логически зависит данный оператор. При преобразовании вершин с-схемы (за ис ключением распознавателей) и их информационных зависимостей вы полняются те же действия, что и в алгоритме A1. При преобразовании условных конструкций с-схемы используется вспомогательный рекур сивный алгоритм ACG2, в котором при преобразовании вершин (за ис ключением логически узловых операторов) условной конструкции и их информационно-логических зависимостей выполняются соответствую щие действия алгоритма ACG1, а при преобразовании логически узло вого оператора построение соответствующей потоковой вершины и ее выходных вершин связи осуществляется при преобразовании первого распознавателя из соответствующего множества LP, а построение ее входных вершин связи — при преобразовании последнего распознавате ля из множества LP, что позволяет корректно отображать логические зависимости данного логически узлового оператора. В теореме 1.3. показывается, что построенная конструкция A2(SS) является п-схемой, эквивалентной исходной с-схеме SS.

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

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

Алгоритм A4 осуществляет преобразования с-схемы SS, содержа щей циклические конструкции, включающие неструктурированные услов ные конструкции, в потоковый вид и является развитием алгоритма A2. Предварительно аналогично алгоритму A2 осуществляется анализ информационно-логических зависимостей в SS и ее модификация, а затем — преобразование ее элементов в потоковый вид. При преобра зовании циклических конструкций выполняются действия алгоритма ALG1, а при преобразовании условных конструкций — действия алго ритма ACG2. В теореме 1.3.4 показывается, что построенная конструк ция A4(SS) является п-схемой, эквивалентной с-схеме SS.

Алгоритм A5 представляет собой развитие алгоритма A3 на случай с-схем с массивами SSA. Предварительно наряду с анализом инфор мационно-логических зависимостей и модификацией с-схемы SSA вы полняется переименование массивов так, чтобы предотвратить повтор ные присваивания значений элементам массивов. Дополнительно для каждого имени массива строится вершина порождения массива;

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

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

Отметим, что предложенные алгоритмы имеют линейную сложность относительно размера исходной с-схемы. Кроме того, данные алгорит мы были протестированы в рамках ЭСПП (Эспериментальная Система Потокового Программирования), которая была реализована автором в системе программирования Барроуз и общий объем которой составил тыс. ПЛ-строк.

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

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

Данный раздел состоит из двух частей. В первой сначала опреде ляется понятие первичной структуры событий (prime event structure) E = (E,, #), где E — множество событий, на котором определены отношение причинной зависимости (частичный порядок), удовле творяющее принципу ‘конечности причин’, и отношение # конфликта (иррефлексивное и симметричное отношение), удовлетворяющее прин ципу ‘наследования конфликта’. Два события, не связанные ни отноше нием причинной зависимости, ни конфликта, считаются параллельны ми. Конфигурацией структуры называется левозамкнутое (относитель но причинной зависимости) подмножество бесконфликтных событий.

Начальная конфигурация — это пустое множество. Далее вводится ряд определений ‘аксиом параллельности’. Свойства K-, N -плотности и K перекрестности предназначены для изучения отношений причинной за висимости (li) и параллелизма (co) и основаны на пересечении линий, образованных множествами событий, находящихся в указанных отно шениях. Свойства L-плотности и L-перекрестности являются обобщени ем соответствующих K-свойств на отношения причинной зависимости (li) и недетерминированного выбора (cf ). Оказалось, что конечность первичной структуры гарантирует свойства K- и L-‘перекрестности’, которые являются ослаблением свойств K- и L-плотности соответствен но. Установлено, что для всего класса первичных структур событий свойства L-плотности и L-перекрестности совпадают, тогда как совпа дение свойств K-плотности и K-перекрестности обеспечивается только при выполнении свойства N -плотности. В отличие от сетей-процессов и частично упорядоченных множеств, рассматриваемая модель первич ных структур позволила ввести и изучить ряд новых понятий — свой ства R-плотности и N -плотности, ориентированные на отношения па раллелизма (co) и недетерминированного выбора (cf ). Устанавливается, что данные свойства совпадают для структур с бинарными отношения ми параллелизма и конфликта. Далее вводится свойство M li -плотности (M co -плотности, M cf -плотности), основанное на пересечение двух плос костей, одна из которых образована отношениями li и co (co и cf, cf и li соответственно), а другая — отношениями li и cf (co и li, cf и co со ответственно). Благодаря этому стало возможным установление тесных взаимосвязей между различными формулировками понятия плотности.

В частности, в теореме 2.1.1 для конечных и беступиковых первичных структур показывается совпадение следующих свойств: K- и M cf -плот ности, L- и M co -плотности, а также R- и M li -плотности.

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

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

Сначала для каждого процесса (последовательности срабатыва ний вершин) из множества процессов R начально размеченной струк турированной п-схемы (CF S, Min ) строится з-граф, G ((CF S, Min )) = (V, E, l ), где V — множество вершин, соответствующих срабатыва ниям из, E — множество дуг, отражающих причинные зависимости между срабатываниями из, l — функция, помечающая дуги графа со ответствующими срабатываниями. Вводится понятие проекции з-графа на множество срабатываний операторов и распознавателей — G = (V, E, ), которое позволяет обобщить несущественные зависимости l в з-графе. Пусть G обозначает множество конечных проекций з-графов для начально размеченной п-схемы (CF S, Min ). На множестве G вво дится отношение частичного порядка G G обычном образом.

Далее на основе множества G строится структура E((CDS, Min )) = (E,, #, l), где E = R (V );

= R (E ) ;

любые два события e и e находятся в отношении конфликта (e # e ), eсли и только если e и e одновременно не принадлежат множеству вершин ни одного з графа из G;

l = R l. Доказано, что E((CDS, Min )) — помеченная структура событий. Пусть C обозначает множество конечных конфигу раций в E((CDS, Min )). В теореме 2.2.1 показано, что (G, ) и (C, ) — изоморфные множества, а в теореме 2.2.3 установлено, что (G, ) и (C, ) — когерентные, первично алгебраические и ограниченные час тично-упорядоченные множества.

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

Пусть E — структура событий, помеченная над множеством дей ствий Act, и C(E) — множество ее конфигураций. Определим ряд от p ношений на конфигурациях C, C C(E): а) C E C (отношение при чинности), если C C и C \ C = p (p — частично упорядоченное мультимножество над Act);

б) C E C (отношение конфликта), если не существует такой конфигурации C, что C C и C C ;

в) C E C (отношение параллелизма), если не выполняется ни одно из условий:

C C, C C и C E C.

Интерливинговой бисимуляцией (обозначается i ) между структу рами событий E и F называется отношение B C(E) C(F ) такое, что пара, состоящая из начальных конфигураций данных структур, при a надлежит B, и для всех пар (C, D) B выполняется: а) если C E C, a то найдется конфигурация D в F такая, что D F D и (C, D ) B;

б) то же верно для конфигурации D. При этом если для всех (C, D) B сужение E на множество C изоморфно сужению F на множество D, то B называется сохраняющей историю бисимуляцией (обозначается h ).

Пусть {i, h}. В определении обратных бисимуляций (обозначают ся b ) вместо пары (C, D) B рассматривается пара (C, D ) B и наоборот, отношение причинности на конфигурациях рассматривает ся в обратном направлении. В определении сохраняющих параллелизм бисимуляций (обозначаются c ) вместо отношения причинности рас сматривается отношение параллелизма на конфигурациях, а в опреде лении сохраняющих конфликт бисимуляций (обозначаются a ) — от ношение конфликта на конфигурациях. Для каждого события структу ры вводится понятие локальной конфигурации как множества событий, являющихся предшественниками (по причинной зависимости) данного события.

Пусть {a, b, c}. Определяя аналогичные эквивалентностные от ношения на множествах локальных конфигураций структур событий E и F, получаем l-бисимуляции (обозначаются l ). Структура событий называется структурой без автопараллелизма, если любые два одина ково помеченных события не параллельны;

— структурой с конечным автоконфликтом, если любое множество одинаково помеченных ее со бытий, состоящих в конфликте друг с другом, конечно. В этом разделе мы ограничимся рассмотрением структур без автопараллелизма и с ко нечным автоконфликтом. В утверждениях 2.3.1-2.3.3 и теореме 2.3. устанавливаются следующие равенства и строгие включения:

а) h i, ib =hb, hb =hc ( {a, c}, {a} );

б) a, c ( {b, c}, {a} );

в) h l ;

la l, lb l, lc l ( {b, c}, {a, c}, {a, b} ).

С целью логической характеризации введенных выше бисимуляци онных эквивалентностей на конфигурациях определяются расширения логики ветвящегося времени CT L посредством введения новых опера торов: CT L с операторами ветвящегося прошлого, CT L с оператором c b параллелизма, CT L с оператором конфликта и CT L — комбинация a abc указанных логик, которая отражает все отношения (причинную зави симость, параллелизм и конфликт) между событиями систем. Пусть {a, b, c, abc}. Нам понадобятся два типа логик: CT L, в которых в качестве множества атомарных пропозиций рассматривается множе ство всех частично-упорядоченных мультимножеств над Act, и 0 CT L, в которых в качестве атомарных пропозиций используются только дей ствия из Act. В записи: CT L, где {., 0}, символ ‘.’ обознача ет ‘пусто’. Вычислением в структуре событий E называется макси a мальная последовательность конфигураций C0 C1... такая, что Ci E Ci+1 для всех i 0. Формально определяется выполнимость CT L - формулы на вычислении в момент времени n = 0, 1,... (обознача ется, n |= CT L ). Используем E |= CT L для обозначения того, что, n |= CT L для любого вычисления в E и любого момента времени n. Для структур событий E и F модальная эквивалентность, порождаемая логикой CT L (обозначается E CT L F ), определяется def следующим образом: E CT L F (E |= CT L F |= CT L для всех CT L -формул ). В теореме 2.3.1 устанавливается следую щее:

а) E i F E 0 CT L F ;

б) E h F E CT L F.

Затем в данном разделе описывается темпоральная логика L1, вве денная Мукундом и Тиагараджаном для логических спецификаций пер вичных структур событий. Отличительной чертой этой логики является то, что в ней наряду со стандартными темпоральными модальностями будущего и прошлого используются модальности параллелизма и неде терминированного выбора. Для наших целей удобно в качестве множе ства атомарных пропозиций взять множество действий Act. Семантика логики L1 интерпретируется с использованием локальных конфигура ций. Определяется понятие выполнимости L1 -формулы на локаль ной конфигурации e (обозначается e |=L1 ). Модальная эквива лентность, порождаемая логикой L1 (обозначается L1 ), определяется def следующим образом: E L1 F (E |=L1 F |=L1 для любой L1 -формулы ). В теореме 2.3.2 устанавливается следующее:

E L1 F E labc F.

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

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

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

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

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

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

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

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

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

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

В разделе 3.1 разрабатываются методы ‘проверки на модели’ (model checking) с использованием аппарата темпоральных логик реального времени. Сначала предлагается базовый метод верификации поведенче ских свойств систем реального времени, представленных сетями Петри с непрерывным временем, основанный на темпоральной логике реального ветвящегося времени T CT L. С целью повышения эффективности мето да применяются техники частичных порядков, зон и параметризации.

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

В начале раздела приведены определения, связанные с понятием временной сети Петри T N = (P, T, F, D, M0 ), которая характеризуется непересекающимися конечными множествами мест P и переходов T, от ношением инцидентности F (P T )(T P ), начальной разметкой M и временной функцией D, сопоставляющей каждому переходу времен ной интервал. Ограничимся рассмотрением однобезопасных временных сетей. Во временной сети смена одного состояния другим осуществля ется либо при истечении некоторого времени, либо при срабатывании некоторого перехода. Поведение временной сети моделируется путями – последовательностями состояний, связанных срабатыванием переходов или истечением времени.

Далее приводятся синтаксис и семантика известной темпоральной логики реального времени T CT L. Данная логика является расшире нием языка ветвящегося времени CT L за счет добавления временных ограничений на его операторы. Семантика T CT L определяется на со стояниях и путях временной сети.

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

Размер G(T N, ) экспоненциален относительно размера T N.

Алгоритм верификации T CT L-формулы на временной сети T N состоит в построении графа регионов G(T N, ) и пометке его вершин подформулами формулы или их отрицанием. Устанавливается кор ректность алгоритма пометки. В теореме 3.1.2 утверждается, что суще ствует алгоритм, проверяющий, удовлетворяет ли временная сеть Петри T N T CT L-формуле, который линеен по длине и размеру G(T N, ) (и, следовательно, экспоненциален по размеру T N ).

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

Особенность предложенной редукции состоит в учете как параллелиз ма сети, так и существенности временных ограничений при проверке выполнимости заданного свойства. Идея редукции состоит в следую щем: для каждой вершины v строящегося редуцированного графа реги онов GR (T N, ) при порождении следующих вершин рассматриваются не все срабатывающие переходы (как при построении G(T N, )), а их подмножество и, кроме того, истечение времени, если в вершине v вре мя существенно для данной вершины и формулы. Вводится понятие временной статтеринг-эквивалентности для графов регионов, позволя ющее осуществлять их корректную редукцию. В теореме 3.1.3 для за данных временной сети Петри T N и T CT L-формулы показывается, что графы регионов G(T N, ) и GR (T N, ) статтеринг-эквивалентны.

Таким образом, алгоритм пометки для графа регионов G(T N, ) сво дится к алгоритму пометки для редуцированного графа GR (T N, ).

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

В следующем пункте раздела делается попытка редуцировать число анализируемых сетевых состояний с использованием техники зон. Вво дится понятие временной сети с зонами ZN = (P, T, F, Z, M0 ), которая является модификаций временной сети Петри за счет использования функции Z, связывающей с каждым переходом зону временной задерж ки его срабатывания. (Временной) зоной Z называется многогранник из Rn (n N), содержащий все решения конечного числа некоторых линейных неравенств. Как и во временной сети Петри, так и во времен ной сети с зонами, смена одного состояния другим осуществляется либо при истечении некоторого времени, либо при срабатывании некоторо го перехода сети. Вводятся понятие обобщенного состояния, являюще еся аналогом региона, но с использованием временных зон, и понятие стабильного разбиения сетевых состояний на обобщенные состояния, которое означает, что все состояния из обобщенного состояния, принад лежащего, эквивалентны относительно их достижимости. Таким обра зом, проблема достижимости состояний может быть сведена к проблеме достижимости обобщенных состояний при стабильном разбиении. На вход верификационного алгоритма поступают временная сеть с зонами ZN, начальное разбиение 0 множества состояний временной сети с зо нами и свойство сети, представленное T CT L-формулой. Суть данного алгоритма состоит в следующем: строится конечное графовое представ ление сетевого поведения — граф обобщенных состояний при начальном разбиении 0, G(ZN, 0 );

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

Устанавливается корректность данного алгоритма и дается оценка его сложности.

Далее определяется понятие параметрической временной сети PN = (P, T, F, T, M0 ), которая является модификацией временной сети Пет ри за счет введения функции T, сопоставляющей каждому переходу некоторый временной предикат, индуктивно определяемый следующим образом: = f alse | t | 1 2, где – параметр или натуральное число, t – переход в PN, 1 и 2 – временные предикаты и — од но из бинарных отношений,, =,,. Ограничимся рассмотрением однобезопасных параметрических временных сетей. Вводится понятие означивания как функции, сопоставляющей каждому параметру неко торое натуральное число. Означивание называется c-ограниченным для некоторого натурального числа c, если оно сопоставляет каждому пара метру значение, не превышающее c. Через PN обозначим параметри ческую временную сеть PN с означенными посредством параметра ми. Задача анализа параметрической временной сети PN относительно T CT L-формулы, T BA(PN, ), состоит в нахождении такого означи вания, что формула выполняется в PN при означивании.

Граф регионов G для PN определяется так же, как и для вре менной сети Петри. Граф регионов G параметрической временной сети PN строится как объединение графов регионов G по всем возможным cPN :

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

Данное понятие позволяет выразить время произвольного пути в гра фе регионов через времена простых путей и циклов. Алгоритм решения задачи T BA(PN, ) заключается в построении графа регионов G и по метке пар (v, ) (v – вершина графа G и – некоторая подформула формулы ) некоторой формулой логики первого порядка L(v, ), на зываемой условием, с параметрами в качестве свободных переменных.

Будем говорить, что является решением задачи T BA(PN, ), если для начальной вершины v0 графа G означивание удовлетворяет усло вию L(v0, ). В теореме 3.1.4 показана корректность данного алгоритма анализа, а в теореме 3.1.5. устанавливается существование алгоритма решения задачи T BA(PN, ), который линеен по размеру и дважды экспоненциален по размеру PN.

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

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

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

Проблема распознавания временной бисимуляционной эквивалент ности в контексте временных процессов решается с использованием ме тодов теории категорий. Сначала определяется категория временных процессов и выделяется подкатегория конечных временных слов про цессов. Затем в рамках категории временных сетей вводится традици онное понятие теории категорий — понятие T W -открытого морфизма.

В теореме 3.2.5 формулируется критерий T W -открытости, а в теореме 3.2.8 показывается разрешимость данного понятия с применением тех ники регионов. Далее определяется вспомогательное подобие по времен ным словам и показывается его разрешимость с использованием раз решимости T W -открытости морфизмов;

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

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

Алгоритм распознавания временной трассовой эквивалентности (вре менной тестовой эквивалентности, временной бисимуляции) состоит из следующих шагов: 1) конструирования раскруток МакМиллана базо вых сетей ДВСП;

2) вычисления множеств корректных таймирований сконструированных раскруток;

3) конструирования временных экспан сий данных раскруток на основе корректных таймирований;

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

В разделе 3.3 сначала представляется краткий аналитический об зор инструментальных систем, базирующихся на сетевых моделях. При этом обосновываются достоинства ряда программных комплексов, сре ди которых отмечается система PEP (Programming Environment based on Petri nets). Предлагается программный комплекс RT-MEC (Real Time Model and Equivalence Checher), поддерживающий спецификацию, валидацию и верификацию параллельных систем реального времени, представленных различными моделями временных сетей Петри, и функ ционирующий в составе системы PEP. Рассматриваются структура и функции предлагаемого программного комплекса RT-MEC. Особенное внимание уделено модулям, поддерживающим анализ, симуляцию и ве рификацию временных расширений сетей Петри. В комплексе RT-MEC aнализ осуществляется посредством исследования структуры модели руемой системы, валидация — путем имитационного моделирования (симуляции), а верификация — с помощью как ‘проверки на модели’, так и проверки на поведенческую эквивалентность. Отличительная чер та комплекса RT-MEC состоит в том, что делается попытка объединить в единое целое различные методы анализа и верификации распределен ных систем реального времени с возможностью последующего их срав нения. Также описываются состояние реализации и результаты экспе риментов, проведенных средствами RT-MEC.

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

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

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

Диссертация содержит результаты работ, выполненных автором в Вычислительном центре СО РАН с 1986 по 1990 гг. и в Институте си стем информатики СО РАН с 1990 по 2001 гг. В целом, результаты, изложенные в диссертации, получены автором самостоятельно. Исклю чение составляет следующее: в разработке модели сетей Петри с времен ными параметрами и алгоритма верификации временных сетей Петри с использованием техники частичных порядков (см. раздел 3.2) прини мала участие аспирантка НГУ Е.А. Покозий, а также система RT-MEC (см. раздел 3.3) была реализована при участии с.н.с. ИСИ СО РАН А.В.

Быстрова и группы студентов ММФ НГУ.

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

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

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

– введена формальная модель тегированных потоковых схем (п-схем), определены наиболее важные их поведенческие свой ства (живости, безопасности и ‘очищаемости’);

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

– введены различные классы обогащенных (с массивами и с процедурами) п-схем и исследованы их поведенческие свой ства;

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

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

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

установлена иерархия взаимосвязей этих аксиом;

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

– для структурированных потоковых сетей с тегированными фишками введена семантика ‘истинного параллелизма’ в тер минах структур событий и установлены взаимосвязи между данным семантическим представлением и графом зависи мостей (модификацией традиционного семантического пред ставления — информационно-логического графа) с точно стью до изоморфизма;

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

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

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

– введена и исследована модель структур событий с глобаль ным непрерывным временем, разработаны временные экви валентные отношения в семантиках интерливинг/‘истинный параллелизма’ и линейное/ветвящееся время;

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

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

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

– с целью повышения эффективности верификационных алго ритмов введены и исследованы новые модели параллельных систем реального времени — временные сети с зонами и па раметрические временные сети, а также предложены и оце нены алгоритмы поведенческого анализа данных моделей;

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

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

Основные публикации по теме диссертации 1. Вирбицкайте И.Б. О программной реализации системы имитации потоковых вычислений // Тр. VI Всесоюз. шк.-сем. "Распреде ленная обработка информации". – Львов, 1987. – С. 20–22.

2. Вирбицкайте И. Б. Обработка последовательных фрагментов на устройствах потокового типа // Тр. VII Всесоюз. шк-сем. "Рас пределенная обработка информации". – Львов, 1989. – С. 44–45.

3. Вирбицкайте И. Б. ЭВМ, управляемые потоками данных. – Но восибирск, 1989. – 60с. – (Препр./АН СССР. Сиб. отд-ние. ВЦ;

№ 822).

4. Virbitskaite I.B. Investigating Dataow Networks with Token Colouring // Methods of Theoretical and Experimental Computer Science. – Novosibirsk, 1989. – P. 142–157.

5. Virbitskaite I.B. Behavioral Notions for Eager Data Flow Computing with I-structures // Current Topics in Informatics Systems Research.

– Novosibirsk, 1991. – P. 81–92.

6. Virbitskaite I. The Relative Strength of Density and Crossing Properties for Event Structures // Proc. Intern. Conf. Young Computer Scientists.

– Beijing, China, 1993. – P. 547–552.

7. Virbitskaite I. Observing Some Properties of Event Structures // Lect. Notes Comp. Sci. – 1993. – Vol. 735. – P. 229–250.

8. Virbitskaite I. Some Characteristics of Nondeterministic Processes // Parallel Processing Letters. – 1993. – Vol. 3, N 1. – P. 99–106.

9. Вальковский В.А., Вирбицкайте И.Б. Потоковые вычислитель ные системы // Системная информатика. – Новосибирск: Наука, 1993. – Т. 2. – С. 38–72.

10. Вирбицкайте И.Б., Вотинцева А.В., Шкляев Д.А. О семантиче ских аспектах потоковых вычислений с цветными фишками // Программирование. – 1996. – № 3. – С. 17–35.

11. Вирбицкайте И.Б. О некоторых свойствах структур событий // Кибернетика и системный анализ. – 1997. – № 3. – С. 45–55.

12. Virbitskaite I., Votintseva A. Behavioural Characterizations of Partial Order Logics // Lect. Notes Comput. Sci. – 1997. – Vol. 1279. – P.

463–474.

13. Virbitskaite I. On the Semantics of Concurrency and Nondeterminism:

Bisimulations and Temporal Logics // Electronic Notes in Theoretical Computer Science. – 1998. – Vol. 18.

14. Virbitskaite I. An Event Structure Model for Dataow Computing // Computers and Articial Intelligence. – 1999. – Vol. 18, N 1. – P.

73–93.

15. Вирбицкайте И.Б., Покозий Е.А. Использование техники частич ных порядков для верификации временных сетей Петри // Про граммирование. – 1999. – № 1. – С. 28–41.

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

17. Virbitskaite I.B., Bystrov A.V. Implementing Model Checking and Equivalence Checking for Time Petri Tets by the RT-MEC Tool // Lect. Notes Comp. Sci. – 1999. – Vol. 1662. – P. 194–200.

18. Virbitskaite I.B., Pokozy E.A. Parametric Behaviour Analysis for Time Petri Nets // Lect. Notes Comp. Sci. – 1999. – Vol. 1662. – P 134–140.

19. Virbitskaite I.B., Pokozy E.A. A Partial Order Method for the Verication of Time Petri Nets // Lect. Notes Comp. Sci. – 1999. – Vol. 1684. – P. 547–558.

20. Вирбицкайте И.Б. Семантические модели в теории параллелиз ма. – Новосибирск: ИСИ СО РАН, 2000. – 196 с.

21. Вирбицкайте И.Б., Боженкова Е.Н. Исследование тестовой эк вивалентности временных структур событий // Программирова ние. – 2000. – № 5. – С. 18–30.

22. Virbitskaite I.B. Towards Decision of Testing Equivalence for Time Petri Nets. – Oxford University Press. Logic Journal of IGPL. – 2000.

– Vol. 8, N 6. (Proc. 7th Intern. Workshop on Logic, Lang., Inform.

and Comput., 2000, Natal, Brazil). – P. 181–190.

23. Andreeva M.V., Bozhenkova E.N., Virbitskaite I.B. Analysis of Timed Concurrent Models Based on Testing Equivalence // Fundamenta Informaticae. – 2000. – Vol. 43, N 1–4. – P. 1–20.

24. I.B. Virbitskaite. A Verication Method for Timed Concurrent Systems Using Timing Zones // Proc. Internat. Conf. on Concurrency, Specication and Programming. – Berlin: Humboldt University, 2000. – P. 323– 334.

25. I.B. Virbitskaite. Characterizing Time Net Processes Categorically // Lect. Notes Comp. Sci. – 2001. – Vol. 2127. – P. 128–141.

26. Moskaleva N.S., I.B. Virbitskaite. On the Category of Event Structures with Dense Time // Lect. Notes Comp. Sci. – 2001. – Vol. 2138. – P. 287–298.

27. I.B. Virbitskaite. An Observation Semantics for Timed Event Structures // Lect. Notes Comp. Sci. – 2001. – Vol. 2244. – P. 215–225.

Подписано в печать 14.11.2001г.

Формат бумаги 6084 1/16 Объем 2 уч.-изд.л.

Тираж 100 экз.

НФ ООО ИПО “Эмари” РИЦ, 630090, г. Новосибирск, пр. Акад. Лаврентьева,

 

Похожие работы:





 
2013 www.netess.ru - «Бесплатная библиотека авторефератов кандидатских и докторских диссертаций»

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