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

• Автор: Быстров, Александр Васильевич
• Шифр специальности: 05.13.11
• Научная степень: Кандидатская
• Год защиты: 2008
• Место защиты: Новосибирск
• Количество страниц: 136 с. : ил.

Содержание
Введение

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

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

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

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

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

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

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

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

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

1.5 Раскрашенные СП
1.5.1 Неиерархические раскрашенные сети Петри
1.5.2 Временные раскрашенные СП
1.5.3 Раскрашенные СП с приоритетами
1.5.4 Иерархические раскрашенные СП
1.6 Обсуждение возможностей инструментальных средств, поддерживающих сетевые модели
2 Сетевые средства спецификации управления в языке параллельного программирования Барс
2.1 Структуры управления
2.2 Типы управления
2.2.1 Описание типов управления
2.2.2 Программирование с типами управления
2.3 Базовый язык асинхронного параллельного программирования Барс
2.4 С-язык
2.5 Программная симуляция иерархических сетей с ожиданием

3 Анализ временных сетевых моделей посредством систе-
мы ИТ-МЕС
3.1 Структурный анализ ВСП
3.1.1 Теоретическое обоснование
3.1.2 Анализ живости НВСП
3.1.3 Анализ на основе б'-компонент
3.1.4 Анализ на основе Т-компонент
3.2 Семантический анализ ВСП
3.2.1 Семантика ДВСП в терминах временных первичных структур событий
3.2.2 Семантика НВСП в терминах временных локальных структур событий
3.3 Концепции, организация и возможности системы КГ-МЕС
3.3.1 Структура и функции
3.3.2 Реализация и эксперименты
4 Проектирование, симуляция и валидация иерархических временных раскрашенных сетевых моделей посредством системы ХХЕБ
4.1 ИВТ-сети
4.2 Особенности структурной и функциональной организации системы ХИЕЭ
4.2.1 Графический редактор
4.2.2 Симулятор
4.2.3 Трассировщик
4.2.4 Визуализатор
4.2.5 Подключаемые модули (плагины)
4.2.6 Эксперименты
Заключение
Список литературы
Приложение

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

Первая сумма определяет удаляемые фишки, а вторая сумма — добавляемые фишки при выполнении шага Y. Запись М [Y > М2 означает, что М2 непосредственно достижима из М посредством выполнения шага Y.
Последовательность выполнений — это конечная или бесконечная последовательность разметок и шагов
M1[Yl > M2[Y2 > Ms ... Mn[Yn > Mn+i
такая, что Мг[Уг > М1+г для всех i 6 N {0}. Здесь Mi называется началом и Мп+г — концом (в случае конечной последовательности выполнений) заданной последовательности срабатываний. Разметка М достижима из разметки М', если существует конечная последовательность выполнений имеющая началом М1 и концом М, то есть для некоторого п € N+ существует последовательность шагов У), УД... Yn такая, что М'[У1 > M...M[Yn > М.
1.5.2 Временные раскрашенные СП
В работе [77] разработаны временные модели раскрашенных СП. Для представления времени вводится понятие глобальных часов, значение которых представляет текущее модельное время. Начальное модельное время, т. е. значение часов, при котором сеть начинает функционировать, задается при описании временных раскрашенных СП. При этом множества цветов (все или их часть) получают признак timed.
Фишка, принимающая значения из множества, обладающего признаком timed, в дополнение к основному цвету несет временное значение (временной штамп), определяющее момент времени, раньше которого фишка не может использоваться при срабатывании какого-либо перехода. Например, разметка некоторого места, имеющая вид З‘р@[2,4,6], соответствует наличию в месте трех фишек цвета р, одна из которых несет временной штамп, равный 2, вторая — 4, третья — 6. Фишки, принимающие значения из множеств, не имеющих признака timed, временного штампа не несут. Последнее означает, что фишка готова к использованию с момента своего появления в месте.
Временной штамп вновь появившейся фишки вычисляется как текущее модельное время плюс задержка, величина которой определяется выражением @ + D. Это выражение называется также временной пометкой и может быть связано с переходом и/или с выходной дугой. Если временная пометка связана только с переходом, то во все выходные места перехода помещаются фишки с одинаковыми временными штампами. Временная пометка на дуге определяет значение временного штампа только для фишки, помещаемой в место, для которого данная дуга входная. Если временная пометка присутствует и на переходе, и на дуге, то значения задержек суммируются. На рис. 14 присутствуют оба типа пометок. Переход t, определяя временной штамп фишки, увеличивает текущее значение глобальных часов на три. Таким образом определяется временной штамп фишки, помещаемой в место С. Дуга от перехода t к месту D имеет собственную временную пометку, которая увеличивает значение временного штампа, определенного переходом, на единицу. В результате,