Моделирование Estelle-спецификаций распределенных систем с помощью раскрашенных сетей Петри

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

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

Глава I. Базовые понятия

1.1 Обзор языка .

1.1.1 Понятие модуля.

1.1.2 Организация взаимодействия между модулями

1.1.3 Принцип структуризации и такт вычисления.

1.1.4 Концепция времени в

1.2 Сети Петри

1.2.1 Ординарные сети Петри .

1.2.2 Раскрашенные сети Петри

1.2.3 Декларации раскрашенной сети.
1.2.4 Пометка раскрашенной сети
1.2.5 Правила функционирования раскрашенных сетей
1.2.6 Структура иерархической раскрашенной сети
1.3 Расширение модели раскрашенных сетей
1.3.1 Временные раскрашенные сети .
1.3.2 Раскрашенные сети с приоритетами.
Глава II. Моделирование статических спецификаций посредством раскрашенных сетей
2.1 Отображение предопределенных типов
2.2 Отображение иерархии модулей
2.3 Формальные параметры и экспортируемые переменные
2.4 Точки взаимодействия и структура связей.
2.5 Отображение тела модуля..
2.6 Моделирование перехода
2.6.1 Приставка vi.
2.6.2 Представление стандартных операторов.
2.6.3 Отображение процедур и функций.
2.7 Моделирование отложенных Енереходов
2.8 Моделирование такта вычисления
2.8.1 Последовательное выполнение
2.8.2 Параллельное выполнение
2.9 Обоснование алгоритма построения и оценка размера сети
Глава III. Моделирование динамических спецификаций посредством раскрашенных сетей
3.1 Отображение иерархии модулей
3.2 Идентификация экземпляров модулей.
3.3 Формальные параметры и экспортируемые переменные
3.4 Точки взаимодействия
3.5 Операторы установления связи .
3.5.1 Соединение точек взаимодействия
3.5.2 Прикрепление точек взаимодействия
3.6 Операторы разъединения связей.
3.6.1 Отсоединение точек взаимодействия
3.6.2 Открепление точек взаимодействия.
3.7 Организация вводавывода
3.8 Отображение тела модуля
3.8.1 Моделирование модулейнаследников
3.8.2 Моделирование функциональности тела модуля.
3.9 Моделирование перехода
3.9.1 Специфические операторы
3.9.2 Процедуры и функции
3.9.3 Моделирование Епереходов с задержками .
3. Создание и уничтожение новых экземпляров модулей.
31 Создание экземпляра модуля
32 Уничтожение экземпляра модуля..
3. Моделирование такта вычисления.
3. Обоснование алгоритма построения и оценка размера сети
Глава IV. Эксперименты
4.1 Программный комплекс V.
4.2 Кольцевой протокол.
4.2.1 Описание протокола
4.2.2 спецификация протокола.
4.2.3 Сетевая модель протокола.
4.2.4 Эксперименты с кольцевым протоколом.
Заключение
Литература


Автоматическое построение сетевых моделей существенно сокращает трудоемкость по проведению экспериментов и избавляет от необходимости проводить валидацию самого процесса построения, а по-уровневое представление спецификации делает возможным построение сетевых моделей для систем реальной сложности. Предложенные алгоритм перевода и сетевая модель используются в системе EPV. Российского Фонда Фундаментальных исследований. JCP 0 от Международного Научного Фонда и Российского правительства. ИНТАС N -CT9S-. ИНТАС-РФФИ N -. Президиума СО РАН Поддержки международных проектов. International Conference on Parallel Computing Technologies, St. Peters-burg, Russia, . IF IP th International Symposium on Protocol Specification, Testing and Verification, Warsaw, Poland, . Third International Workshop on Concurrency, Specification and Programming, Warsaw, Poland, October . IMACS World Congress on Scientific Computation, Modelling and Appl. Berlin, Germany, . International Conference on Parallel Computing in Electrical Engineering, Bialystok, Poland, . International Workshop on the Formal Description Technique Estelle, Evry, France, . Четвертый Сибирский Конгресс no Прикладной и Индустриальной Математике (ИППРИМ-), Новосибирск, Россия, . Конференция молодых ученых, посвященная -летию И ВТ СО РАН, Новосибирск, Россия, . Кроме того, полученные результаты обсуждались на объединенном семинаре ИСИ СО РАН и кафедры программирования НГУ “Теоретическое и экспериментальное программирование”. Публикации. По теме диссертации опубликовано научных работ. Из них 8 работ [, , , , , , , ] — на конференциях, 2 работы [2, ) — в центральных изданиях и 6 работ [, , , , , ] — в местных изданиях. Структура работы. Диссертация состоит из введения, четырех глав, заключения, списка литературы и приложения. В данной главе дается описание языка формальных описаний Estelle, раскрашенных сетей Петри, а также вводятся два временных расширения сетевой модели. Язык формальных описаний Estelle [6, ] основан на объединении конечного автомата с языком программирования Pascal и добавлении элементов описания архитектурных особенностей систем. Базовым понятием языка Estelle является архитектура системы, которая определяется иерархически организованным множеством модулей и структурой их взаимосвязей. Для задания структуры взаимосвязей служат двунаправленные каналы между портами (точками взаимодействия). Количество экземпляров конкретного модуля и структура взаимосвязей может изменяться в процессе функционирования системы. Модуль определяется описанием, состоящим из заголовка и тела, связанного с заголовком. Тело модуля может текстуально включать в себя описания других модулей, которые называются наследниками данного модуля и могут, в свою очередь, содержать описания модулей. В результате образуется дерево описаний модулей. Охватывающий модуль называется родителем модулей, непосредственно описанных в его теле. Модуль, охватывающий все прочие модули системы, называется спецификацией системы. Неформальный ример вложенных описаний приведен на рис. Графически вложенность описаний представлена двумя способами — деревом (рис. В процессе выполнения Estelle-спецификации одновременно может существовать несколько экземпляров модуля, которые создаются как статически — при инициализации всей системы, так и динамически. Дерево описаний модулей образует статический прототип иерархии экземпляров модулей. Количество экземпляров конкретного модуля может изменяться, но позиция в общей иерархии остается неизменной и соответствует положению описания этого модуля в дереве описаний. Иерархии описаний модулей, изображенной на рис. Рис. Графическое представление вложенности описаний модулей соответствовать иерархия экземпляров модулей, приведенная на рис. Рис. С внешней точки зрения, экземпляр модуля представляет собой “черный ящик”. Взаимодействие с ним происходит через конечное число точек взаимодействия и экспортируемые переменные, причем доступ к последним имеет только экземпляр родительского модуля. Все экземпляры одного модуля обладают одинаковыми внешними признаками, характеристики которых определяются заголовком модуля, где описаны класс данного модуля, точки взаимодействия, экспортируемые переменные и формальные параметры.