Содержание к диссертации
Введение
Глава I. Базовые понятия 11
1.1 Обзор языка Estelle 11
1.1.1 Понятие модуля 11
1.1.2 Организация взаимодействия между модулями 15
1.1.3 Принцип структуризации и такт вычисления 19
1.1.4 Концепция времени в Estelle . 22
1.2 Сети Петри 23
1.2.1 Ординарные сети Петри 23
1.2.2 Раскрашенные сети Петри 23
1.2.3 Декларации раскрашенной сети , 24
1.2.4 Пометка раскрашенной сети 25
1.2.5 Правила функционирования раскрашенных сетей . 26
1.2.6 Структура иерархической раскрашенной сети 27
1.3 Расширение модели раскрашенных сетей 28
1.3.1 Временные раскрашенные сети 28
1.3.2 Раскрашенные сети с приоритетами 32
Глава II. Моделирование статических Estelle-спецификаций посредством раскрашенных сетей 34
2.1 Отображение предопределенных типов Estelle 35
2.2 Отображение иерархии модулей 36
2.3 Формальные параметры и экспортируемые переменные 39
2.4 Точки взаимодействия и структура связей 40
2.5 Отображение тела модуля 44
2.6 Моделирование Estelle-перехода 46
2.6.1 Приставка provided 50
2.6.2 Представление стандартных операторов 51
2.6.3 Отображение процедур и функций 53
2.7 Моделирование отложенных Е-переходов 54
2.8 Моделирование такта вычисления 59
2.8.1 Последовательное выполнение 59
2.8.2 Параллельное выполнение 63
2.9 Обоснование алгоритма построения и оценка размера сети . 65
Глава III. Моделирование динамических Estelle-спецификаций по средством раскрашенных сетей 72
3.1 Отображение иерархии модулей 73
3.2 Идентификация экземпляров модулей 74
3.3 Формальные параметры и экспортируемые переменные 77
3.4 Точки взаимодействия , 78
3.5 Операторы установления связи 80
3.5.1 Соединение точек взаимодействия 80
3.5.2 Прикрепление точек взаимодействия 82
3-6 Операторы разъединения связей 83
3.6.1 Отсоединение точек взаимодействия 84
3.6.2 Открепление точек взаимодействия 85
3.7 Организация ввода/вывода 87
3.8 Отображение тела модуля 89
3.8.1 Моделирование модулей-наследников 90
3.8.2 Моделирование функциональности тела модуля 91
3.9 Моделирование Estelle-перехода 92
3.9.1 Специфические операторы Estelle 93
3.9.2 Процедуры и функции . 96
3.9.3 Моделирование Е-переходов с задержками 96
3.10 Создание и уничтожение новых экземпляров модулей 100
3.10.1 Создание экземпляра модуля 100
3.10.2 Уничтожение экземпляра модуля 102
3.11 Моделирование такта вычисления 103
3.12 Обоснование алгоритма построения и оценка размера сети .105
Глава IV. Эксперименты 114
4.1 Программный комплекс EPV 114
4.2 Кольцевой протокол 118
4.2.1 Описание протокола 118
4.2.2 Estelle-спецификация RE-протокола 121
4.2.3 Сетевая модель RE-протокола 122
4.2.4 Эксперименты с кольцевым протоколом 123
Заключение 131
Литература 133
Приложение 141
- Принцип структуризации и такт вычисления
- Моделирование отложенных Е-переходов
- Соединение точек взаимодействия
- Обоснование алгоритма построения и оценка размера сети
Введение к работе
Большая сложность и многообразие функций, выполняемых современными информационно-вычислительными сетями, привели к разработке многочисленных формальных моделей, используемых в настоящий момент для спецификации распределенных систем. При этом возрастающая потребность в распределенных вычислительных системах и сетях ЭВМ требует не только реализации таких систем на основании формальных описаний, но и повышения эффективности методов проектирования путем создания инструментальных средств, предназначенных для автоматизации процессов проектирования и анализа.
Формальные модели, используемые в настоящий момент для спецификации распределенных систем можно классифицировать по различным признакам. Один из подходов подразделяет их на автоматные модели и модели последовательностей [6]. Автоматные модели рассматривают внутреннее состояние объекта спецификации и описывают все возможные изменения этого состояния при воздействии на объект. К моделям этого вида относят конечные автоматы, различные виды сетей Петри, автоматы, расширенные переменными и т. д. Модели последовательностей рассматривают только наблюдаемое извне поведение объекта, не делая никаких предположений о его внутренней структуре. К ним относят алгебры взаимодействующих процессов, описания, использующие временные логики и пр.
Известны примеры непосредственного моделирования распределенных систем с помощью методов первой или второй группы. Так в работах Р.Коэна и А.Сегала [37] и Г. И. Холцмана [46] использовались конечные автоматы, а в работе К. Сибертин-Бланка [75] — ординарные сети Петри, а Т. Pyssysalo и Л. Оджала [72] — PrT(predicate-transition)-ceTH. В России также велись исследования в этом направлении. Среди них следует отметить в частности, работы О. Л. Бандман [1, 3] — по спецификации поведения сетевых протоколов, Н. А. Анисимова [27, 28] — по ручному моделированию с использованием сетей Петри, А. Петренко [79], Н. В. Евтушенко [80], Ю. Г. Карпова [56] — по тестированию коммуникационных протоколов с помощью конечно-автоматных моделей, а В. А. Соколова и А. И. Легалова [19] — с помощью сетей Петри.
С другой стороны на практике широко используются языки выполнимых спецификаций, "лидерами" среди которых являются языки Estelle [6, 34, 48] и LOTOS [23, 63], являющиеся стандартами ISO, а также SDL [7, 73], при-
нятый в качестве стандарта ITU. Причем языки Estelle и SDL основаны на модели расширенного конечного автомата, a LOTOS — на теории исчисления взаимодействующих процессов. Основным достоинством языков выполнимых спецификаций, помимо их выразительной силы, является близость к языкам программирования, облегчающая процесс реализации алгоритмов, описанных на этих языках. Однако способы анализа выполнимых спецификаций остаются предметом исследования. Поэтому, несмотря на существование ряда программных средств, предназначенных для анализа и верификации выполнимых спецификаций, широко используется практика отображения спецификаций в формальные модели, для которых существуют эффективные методы анализа и автоматические средства верификации. Известны примеры трансляции выполнимых спецификаций в конечно-автоматные модели (Ж. Л. Ричье, Й. Сифакис и др. [74]), сети Петри (В. Димитров и А. Петков [39], С. Марчена [63]), алгебры процессов (А. Гаммелгард и Ж. Е. Кристенсен [42]) и темпоральные логики действий (А. Яновская, П. Яновский [49]).
Опубликован ряд работ по трансляции SDL-спецификаций в различные виды сетей Петри, в которых четко можно выделить два направления. Первое использует известные виды сетей Петри высокого уровня, такие как РгТ-сети [47, 57] и М-сети [43,45]. Для второго характерно создание новых классов сетей Петри, ориентированных на язык [41, 29]. Однако их применение требует разработки специальных методов анализа, неизбежно трудоемких в силу сложности сетей.
Для Estelle-спецификаций в работе Ж. Л. Ричье, Й. Сифакиса и др. [74] предложен метод автоматического построения конечно-автоматных моделей посредством исчерпывающей симуляции, позволяющий верифицировать некоторые свойства исходных спецификаций. В работах В. Димитрова и А. Петкова [39] ограниченное подмножество Estelle отображается в ординарные сети Петри. А. Яновская и П. Яновский в работе [49] предлагают способ перевода подмножества Estelle, не включающего динамических возможностей Estelle, времени и приоритетов, в темпоральную логику TLA+. При этом сами авторы отмечают, что их метод скорее подходит для верификации алгоритмов, описанных на достаточно высоком уровне абстракции, чем для протоколов с большим количеством деталей, относящихся к реализации. В работе [50] описана трансляция Estelle-спецификаций в язык описания протоколов Promela, представляющего систему в виде множества процессов, обменивающихся сообщениями. Для полученных таким образом описаний проводится верификация методом проверки на модели. Однако ограничения, касающиеся времени, приоритетов и вложенности модулей, сохраняются.
Наиболее близкий к нашему подход предложен в работах Р. Лая [60, 55].
Этот подход основан на отображении Estelle-спецификаций в нумерические сети Петри, причем рассматривается довольно широкое подмножество, включающее динамические конструкции. Однако имеется ряд отличий между предлагаемым нами алгоритмом и способом построения нумерической сети, рассматриваемом в работе [60]. Последний требует предварительной обработки Estelle-специфи-кации, в процессе которой все переходы в модулях приводятся к такому виду, чтобы моделирование перехода спецификации требовало бы ровно одного перехода сети. Например, Estelle-переход, содержащий условный оператор, заменяется двумя — по одному для каждой из ветвей условного оператора, что вызывает также модификацию предиката возможности Estelle-перехода. Очевидно, что такое преобразование спецификации требует дополнительных усилий. Кроме того, нет гарантий, что в процессе преобразования не возникнут новые ошибки, которые отсутствовали в исходном тексте спецификации.
Другое отличие заключается в том, что в работе [60] не рассматриваются Estelle-переходы с задержками и приоритетами. Причиной этого, по всей видимости, послужило отсутствие временного механизма в автоматической системе PROTEAN, которая использовалась для верификации нумерических сетей, полученных при трансляции Estelle-спецификаций. В более поздних работах [61] используются модульные сети Петри (Communicating Time Petri Nets), обладающие средствами для моделирования поведения, явно зависящего от времени. Однако авторы в этих работах рассматривают не стандартный вариант Estelle, а предлагают некоторое расширение языка, приближающее Estelle к языкам реального времени.
Кроме того, во всех перечисленных работах реализация предложенных методов упоминается только как тема для исследования. Моделирование распределенных систем, как правило, выполняется отдельно для каждого примера, что приводит к необходимости верификации процесса моделирования. Это, в свою очередь, является сложной проблемой для реальных распределенных систем. Таким образом, автоматический перевод выполнимых спецификаций в формальные модели, для которых существуют эффективные методы анализа и автоматические средства верификации, представляет значительный интерес. В частности, в книге К. Йенсена [54] поставлена проблема автоматического построения сетевых моделей SDL-спецификаций, развития средств их верификации, а также проведения экспериментов по обнаружению семантических ошибок распределенных систем с помощью этих средств. Несомненна актуальность аналогичной проблемы и для Estelle-спецификаций.
Наш подход состоит в автоматическом переводе Estelle-спецификаций в раскрашенные сети Петри, предложенные К. Йенсеном [52]. Среди большого числа различных, в том числе объектно-ориентированных [44, 62], расширений сетей
Петри выбор раскрашенных сетей в качестве базового формализма был обусловлен множеством причин, в частности компактностью графического представления, строгим математическим базисом модели, наличием автоматических средств симуляции и анализа [53, 54], а также богатым опытом практического использования раскрашенных сетей [54, 59]. Еще одним аргументом в пользу раскрашенных сетей является наличие естественного иерархического механизма, благодаря чему возможно поуровневое отображение Estelle-спецификаций. Последнее немаловажно при моделировании больших систем, так как "плоская" модель может оказаться необозримой.
Для моделирования Estelle-спецификаций используется расширенный вариант раскрашенных сетей. Модель расширена приоритетами [9] и явным временным механизмом. На момент разработки алгоритма трансляции статических Estelle-спецификаций для раскрашенных сетей не было определено собственного временного расширения. После изучения ряда временных механизмов, предложенных для сетей Петри [4,30,31,32,65, 76, 77, 81], для целей моделирования временного поведения Estelle был выбран механизм, предложенный Мерлином [31]. Выбор механизма был сделан на основании схожести временных ограничений, накладываемых на поведение сети и спецификации в языке Estelle [10]. Кроме того, для данного варианта временных сетей существуют методы анализа [5, 31], которые можно перенести на случай раскрашенных сетей. Позднее для раскрашенных сетей был разработан временной механизм, основанный на понятиях глобальных часов и временных штампов фишек [53]. Этот механизм реализован в системе Design/CPN, которая позволяет строить, симулировать и анализировать раскрашенные сети со временем или без него. Механизм глобальных часов используется автором при моделировании Estelle-спецификаций с динамическими конструкциями, хотя может использоваться и в статическом случае. Следует отметить, что временной механизм, предложенный Мерлином, напрямую не подходит для моделирования спецификаций, допускающих изменение числа экземпляров модулей в течение времени функционирования спецификации. Проблема может быть разрешена введением временных штампов, которые позволяют различать фишки не только по цвету, но и по времени их создания. С другой стороны, два варианта моделирования времени в Estelle сами по себе представляют достаточный интерес, как можно судить по работам, посвященным классификации и сравнительному анализу различных вариантов временных сетей [4, 30, 76, 77].
Вышеописанный подход к верификации распределенных систем начал разрабатываться с 1994 г., когда была реализована первая версия системы Net-Calc [24], а также построены и изучены сетевые модели некоторых протоколов, представленных на языках Estelle и SDL. В 1995 г. разработан метод транс-
ляции Estelle-спецификаций без задержек и приоритетов в раскрашенные сети Петри [18, 68], а также описан наш подход к верификации этих спецификаций, включающий "ручное" применение метода трансляции и использующий систему NetCalc для обнаружения семантических ошибок [67]. В 1997 г, этот метод трансляции расширен на Estelle-спецификаций с задержками и приоритетами [35, 69]. Трансляция осуществляется в эффективную сетевую модель — иерархические временные типизированные сети (ИВТ-сети) — вариант раскрашенных сетей. Проведена реализация метода трансляции, разработана и реализована улучшенная версия системы NetCalc, получившая название EPV (Es-telle Protocol Verifier), а также проведены эксперименты по отладке реализации алгоритма. В 1998 г. было предложено моделирование для многоуровневых Estelle-спецификаций с задержками и приоритетами [36], описаны результаты экспериментов [10, 70] по сетевому моделированию и поиску ошибок для версий четырех известных протоколов: со скользящим окном [74, 78], кольцевого [37], соединений [66], Inres[40]. В работе [71] предложена методика валидации сетевых моделей системы: EPV. Моделирование Estelle-спецификаций с динамическими конструкциями описано в [14, 15, .12]. В 2001 г. предложено обоснование алгоритмов моделирования Estelle-спецификаций с помощью модели раскрашенных сетей Петри. Параллельно в 1997 г. начались работы по моделированию SDL-спецификаций.. В 1998 г. описано построение сетевой модели для SDL-спецификаций без динамических конструкций [20]. В 1999 г. предложен способ моделирования динамических конструкций языка SDL [21], а в 2000 г. осуществлена генерация текстового формата сетевой модели [22], который является входным в системе Design/CPN.
Цель диссертации состоит в разработке эффективных методов и средств моделирования и валидации распределенных систем, в частности коммуникационных протоколов, представленных на языке Estelle. Для достижения указанной цели в работе решаются следующие задачи:
Разработка алгоритма перевода Estelle-спецификаций без динамических конструкций в раскрашенные сети.
Моделирование динамических средств Estelle посредством раскрашенных сетей.
Разработка эффективной сетевой модели — ИВТ-сетей. Проведение экспериментов, подтверждающих, что алгоритмы перевода эффективны и могут быть применены для исследования протоколов связи.
Методы исследования базируются на применении аппарата сетей Петри и языка выполнимых спецификаций Estelle. Научная новизна состоит в следующем. Разработан алгоритм перевода Estelle-спецификаций без динамических
конструкций в раскрашенные сети Петри. Проведено моделирование представительного подмножества языка Estelle-спецификаций, включающего отложенные переходы и приоритеты. Для моделирования последних предложена расширенная модель раскрашенных сетей, включающая в себя временной механизмом и приоритеты. На основании анализа сетевых моделей, получающихся в результате отображения статических Estelle-спецификаций, разработан вариант раскрашенных сетей — иерархические временные типизированные сети (ИВТ-сети), — одной из особенностей которого является отсутствие перебора вариантов связывания переменных, что позволяет существенно повысить эффективность моделирования при реализации.
Впервые предложено формальное обоснование алгоритма. Доказано, что сеть, моделирующая статические Estelle-спецификаций, — безопасна. Введено понятие эквивалентности состояния Estelle-модуля и разметки моделирующей его сети, и показано, что выполнение Estelle-перехода сохраняет эквивалентность состояния и разметки. Дана оценка размера моделирующей сети.
Разработан способ моделирования динамических средств Estelle и алгоритм перевода спецификаций с динамическими конструкциями в раскрашенные сети Петри. Впервые проведено моделирование, охватывающее практически полный язык Estelle, посредством раскрашенных сетей Петри, что позволяет решить проблему автоматического построения сетевых моделей Estelle-специфнкаций.
Дано обоснование предложенного алгоритма. Введен аналог свойства безопасности — послойная безопасность. Показано, что сеть, моделирующая динамические Estelle-спецификаций, — послойно безопасна. Расширено понятие эквивалентности состояния спецификации и разметки моделирующей сети. Доказано, что выполнение Estelle-перехода сохраняет эквивалентность состояния и разметки. Приведена оценка размера моделирующей сети.
Практическая ценность данных исследований заключается в их использовании при реализации трансляторов с языка Estelle в ИВТ-сети, а также в проведении экспериментов по валидации коммуникационных протоколов, в частности, кольцевого протокола. Автоматическое построение сетевых моделей существенно сокращает трудоемкость по проведению экспериментов и избавляет от необходимости проводить валидацию самого процесса построения, а по-уровневое представление спецификации делает возможным построение сетевых моделей для систем реальной сложности. Предложенные алгоритм перевода и сетевая модель используются в системе EPV.
Во время работы над диссертацией автор участвовал в научных проектах, поддержанных следующими грантами:
1. 93-01-986 Российского Фонда Фундаментальных исследований. 1993-1995.
JCP 100 от Международного Научного Фонда и Российского правительства. 1994-
ИНТАСN 1010-СТ93-0042. 1993-1994-
ИНТЛС-РФФИ N 95-0378. 1997-1999.
Президиума СО РАН Поддержки международных проектов. 1997.
Апробация работы проведена на следующих международных и отечественных научных конференциях:
Международные конференции:
3rd International Conference on Parallel Computing Technologies, St.Petersburg, Russia, 1995.
IFIP 15th International Symposium on Protocol Specification, Testing and Verification, Warsaw, Poland, 1995.
Third International Workshop on Concurrency, Specification and Programming, Warsaw, Poland, October 1997.
15-th IMACS World Congress on Scientific Computation, Modelling and AppL, Berlin, Germany, 1997.
International Conference on Parallel Computing in Electrical Engineering, Bialystok, Poland, 1998.
1st International Workshop on the Formal Description Technique Estelle, Evry, France, 1998.
Четвертый Сибирский Конгресс no Прикладной и Индустриальной Математике (ИНПРИМ-2000), Новосибирск, Россия, 2000.
Конференция молодых ученых, посвященная 10-летию МВТ СО РАН, Но
восибирск, Россия, 2000.
Кроме того, полученные результаты обсуждались на объединенном семинаре ИСИ СО РАН и кафедры программирования НГУ "Теоретическое и экспериментальное программирование".
Публикации. По теме диссертации опубликовано 16 научных работ. Из них 8 работ [11, 15, 16, 35, 67, 68, 70, 71] — на конференциях, 2 работы [2, 12] — в центральных изданиях и 6 работ [10, 13, 14, 18, 36, 17] — в местных изданиях.
Структура работы. Диссертация состоит из введения, четырех глав, заключения, списка литературы и приложения.
Принцип структуризации и такт вычисления
Для моделирования Estelle-спецификаций используется расширенный вариант раскрашенных сетей. Модель расширена приоритетами [9] и явным временным механизмом. На момент разработки алгоритма трансляции статических Estelle-спецификаций для раскрашенных сетей не было определено собственного временного расширения. После изучения ряда временных механизмов, предложенных для сетей Петри [4,30,31,32,65, 76, 77, 81], для целей моделирования временного поведения Estelle был выбран механизм, предложенный Мерлином [31]. Выбор механизма был сделан на основании схожести временных ограничений, накладываемых на поведение сети и спецификации в языке Estelle [10]. Кроме того, для данного варианта временных сетей существуют методы анализа [5, 31], которые можно перенести на случай раскрашенных сетей. Позднее для раскрашенных сетей был разработан временной механизм, основанный на понятиях глобальных часов и временных штампов фишек [53]. Этот механизм реализован в системе Design/CPN, которая позволяет строить, симулировать и анализировать раскрашенные сети со временем или без него. Механизм глобальных часов используется автором при моделировании Estelle-спецификаций с динамическими конструкциями, хотя может использоваться и в статическом случае. Следует отметить, что временной механизм, предложенный Мерлином, напрямую не подходит для моделирования спецификаций, допускающих изменение числа экземпляров модулей в течение времени функционирования спецификации. Проблема может быть разрешена введением временных штампов, которые позволяют различать фишки не только по цвету, но и по времени их создания. С другой стороны, два варианта моделирования времени в Estelle сами по себе представляют достаточный интерес, как можно судить по работам, посвященным классификации и сравнительному анализу различных вариантов временных сетей [4, 30, 76, 77].
Вышеописанный подход к верификации распределенных систем начал разрабатываться с 1994 г., когда была реализована первая версия системы Net-Calc [24], а также построены и изучены сетевые модели некоторых протоколов, представленных на языках Estelle и SDL. В 1995 г. разработан метод трансляции Estelle-спецификаций без задержек и приоритетов в раскрашенные сети Петри [18, 68], а также описан наш подход к верификации этих спецификаций, включающий "ручное" применение метода трансляции и использующий систему NetCalc для обнаружения семантических ошибок [67]. В 1997 г, этот метод трансляции расширен на Estelle-спецификаций с задержками и приоритетами [35, 69]. Трансляция осуществляется в эффективную сетевую модель — иерархические временные типизированные сети (ИВТ-сети) — вариант раскрашенных сетей. Проведена реализация метода трансляции, разработана и реализована улучшенная версия системы NetCalc, получившая название EPV (Eselle Protocol Verifier), а также проведены эксперименты по отладке реализации алгоритма. В 1998 г. было предложено моделирование для многоуровневых Estelle-спецификаций с задержками и приоритетами [36], описаны результаты экспериментов [10, 70] по сетевому моделированию и поиску ошибок для версий четырех известных протоколов: со скользящим окном [74, 78], кольцевого [37], соединений [66], Inres[40]. В работе [71] предложена методика валидации сетевых моделей системы: EPV. Моделирование Estelle-спецификаций с динамическими конструкциями описано в [14, 15, .12]. В 2001 г. предложено обоснование алгоритмов моделирования Estelle-спецификаций с помощью модели раскрашенных сетей Петри. Параллельно в 1997 г. начались работы по моделированию SDL-спецификаций.. В 1998 г. описано построение сетевой модели для SDL-спецификаций без динамических конструкций [20]. В 1999 г. предложен способ моделирования динамических конструкций языка SDL [21], а в 2000 г. осуществлена генерация текстового формата сетевой модели [22], который является входным в системе Design/CPN.
Цель диссертации состоит в разработке эффективных методов и средств моделирования и валидации распределенных систем, в частности коммуникационных протоколов, представленных на языке Estelle. Для достижения указанной цели в работе решаются следующие задачи: 1. Разработка алгоритма перевода Estelle-спецификаций без динамических конструкций в раскрашенные сети. 2. Моделирование динамических средств Estelle посредством раскрашенных сетей. 3. Разработка эффективной сетевой модели — ИВТ-сетей. Проведение экспериментов, подтверждающих, что алгоритмы перевода эффективны и могут быть применены для исследования протоколов связи. Методы исследования базируются на применении аппарата сетей Петри и языка выполнимых спецификаций Estelle. Научная новизна состоит в следующем. Разработан алгоритм перевода Estelle-спецификаций без динамических конструкций в раскрашенные сети Петри. Проведено моделирование представительного подмножества языка Estelle-спецификаций, включающего отложенные переходы и приоритеты. Для моделирования последних предложена расширенная модель раскрашенных сетей, включающая в себя временной механизмом и приоритеты. На основании анализа сетевых моделей, получающихся в результате отображения статических Estelle-спецификаций, разработан вариант раскрашенных сетей — иерархические временные типизированные сети (ИВТ-сети), — одной из особенностей которого является отсутствие перебора вариантов связывания переменных, что позволяет существенно повысить эффективность моделирования при реализации. Впервые предложено формальное обоснование алгоритма. Доказано, что сеть, моделирующая статические Estelle-спецификаций, — безопасна. Введено понятие эквивалентности состояния Estelle-модуля и разметки моделирующей его сети, и показано, что выполнение Estelle-перехода сохраняет эквивалентность состояния и разметки. Дана оценка размера моделирующей сети. Разработан способ моделирования динамических средств Estelle и алгоритм перевода спецификаций с динамическими конструкциями в раскрашенные сети Петри. Впервые проведено моделирование, охватывающее практически полный язык Estelle, посредством раскрашенных сетей Петри, что позволяет решить проблему автоматического построения сетевых моделей Estelle-специфнкаций.
Дано обоснование предложенного алгоритма. Введен аналог свойства безопасности — послойная безопасность. Показано, что сеть, моделирующая динамические Estelle-спецификаций, — послойно безопасна. Расширено понятие эквивалентности состояния спецификации и разметки моделирующей сети. Доказано, что выполнение Estelle-перехода сохраняет эквивалентность состояния и разметки. Приведена оценка размера моделирующей сети.
Практическая ценность данных исследований заключается в их использовании при реализации трансляторов с языка Estelle в ИВТ-сети, а также в проведении экспериментов по валидации коммуникационных протоколов, в частности, кольцевого протокола. Автоматическое построение сетевых моделей существенно сокращает трудоемкость по проведению экспериментов и избавляет от необходимости проводить валидацию самого процесса построения, а по-уровневое представление спецификации делает возможным построение сетевых моделей для систем реальной сложности. Предложенные алгоритм перевода и сетевая модель используются в системе EPV.
Моделирование отложенных Е-переходов
Вычислительная модель Estelle описана в терминах, не зависимых от времени.. Одним из принципиальных предположений является то, что о времени выполнения перехода ничего не известно, так как скорость выполнения полностью зависит от реализации. Утверждается только, что вычисления происходят не моментально, а на их выполнение затрачивается некоторое время. При этом ход времени одинаков для всех экземпляров модулей. Если в системе существует несколько переходов, выполнение которых было отложено, то по завершении очередного такта вычислений задержки этих переходов уменьшатся на одну и ту же величину.
Для соотнесения процесса вычислений с течением времени используется приставка delay, которая может входить в условие возможности некоторых переходов. Данная приставка служит для индикации того, что выполнение перехода (если он возможен) должно быть отложено. Задержка определяется двумя временными значениями: минимальным временем, на которое должно быть отложено выполнение перехода, и максимально возможным временем задержки. Иногда считают, что с каждым переходом, имеющим приставку delay, связан таймер, включение и выключение которого происходит во время очередной фазы управления после проверки условия возможности перехода.
Приставка delay имеет три синтаксические формы: delay (dl), delay(dl,d2) и delay(dl, ). Форма delay(dl) семантически эквивалентна delay(dl.dl), а символ служит для обозначения бесконечности. Приставка delay(dl,d2) указывает на то, что выполнение перехода должно быть задержано не менее чем на dl единиц времени и не может быть задержано более чем на d2 единиц времени с момента, как его выполнение стало возможно. Если за время, на которое отложено выполнение некоторого перехода, произошло выполнение другого перехода, которое, возможно, изменило значения переменных и локальное состояние модуля, но не нарушило условие возможности отложенного перехода, то задержка продолжает отсчитываться.
Обыкновенную, или ординарную, сеть Петри можно определить как размеченный ориентированный граф с вершинами двух типов: местами и переходами, соединенными дугами таким образом, что каждая дуга соединяет вершины различных типов [9]. Для изображения перехода используется, как правило, прямоугольник или барьер (вертикальная черта), места — окружность, а дуги — направленная стрелка; Места помечаются целыми неотрицательными числами -(разметка места). В графическом представлении сети разметка изображаются соответствующим числом точек — фишек — в месте.
Вершина х называется входной для вершины у, если в сети существует дуга, ведущая от вершины х к вершине у. Аналогично, вершина х называется выходной для вершины у, если в сети существует дуга, ведущая от вершины у к вершине х. Кроме того, будем называть дуги, ведущие к вершине я и от нее, соответственно входными и выходными дугами этой вершины, а все вершины, связанные с х дугами, — ее окружением.
Сеть Петри функционирует, переходя от разметки к разметке. Функционирование начинается при заданной начальной разметке. Смена разметок происходит в результате срабатывания одного из переходов. Переход может сработать при некоторой разметке, если все входные места перехода содержат хотя бы по одной фишке. Срабатывание перехода изымает по фишке из каждого входного места перехода и помещает по фишке в каждое его выходное место. Сеть Петри называется безопасной, если при любой разметке, достижимой во время функционирования сети, любое место содержит не более одной фишки. Таким образом, сеть Петри моделирует некоторую систему и динамику ее функционирования. При этом места и находящиеся в них фишки представляют состояние моделируемой системы, а переходы — изменение ее состояний. Неиерархические раскрашенные сети Петри являются расширением ординарных сетей Петри, предложенным Йенсеном [51, 52]. В отличие от ординарных сетей Петри, где все фишки считаются неотличимыми друг от друга, каждая фишка в раскрашенной сети обладает индивидуальностью — значением некоторого типа, которое по традиции называется цветом. Функционирование раскрашенной сети зависит не только от наличия фишек во входных местах переходов, но и от их цвета. Неиерархическая раскрашенная сеть состоит из трех частей: структуры сети (которая, по существу, не отличается от структуры ординарной сети), деклараций и пометки сети. Иерархическая раскрашенная сеть представляет собой множество неиерархических сетей, связанных между собой по определенным правилам и функционирующих как единое целое. Рассмотрим все составляющие раскрашенных сетей более подробно. Декларации состоят из описания множеств цветов (типов) и объявления переменных, каждая из которых принимает значения из некоторого множества цветов. Декларации также могут содержать определение операций и функций. Располагаются декларации, как правило, в верхней части страницы в прямоугольнике, ограниченном пунктирной линией. В иерархических раскрашенных сетях деклараций часто выносят на отдельную страницу. В раскрашенных сетях определено четыре базовых множества цветов, соответствующих стандартным типам: целый, вещественный, строковый и булевский. Базовым также является специальное множество цветов, состоящее из одного элемента, которое описывается как Фишки со значением е будем называть бесцветными. Чтобы не загромождать рисунки, выражение на дуге вида е, обозначающее, что в некоторое место сети помещается бесцветная фишка, будет опускаться. Множество цветов может описываться путем перечисления всех возможных значений, осуществляемым двумя различными способами: 1) перечисление относительно небольшого числа объектов, каждый из кото рых обладает уникальным именем: 2) перечисление класса объектов с общим именем и индивидуальными но мерами для отдельных элементов класса: В раскрашенных сетях также имеется несколько механизмов, обеспечивающих возможность конструирования нового множества цветов из уже продекларированных множеств. При моделировании Estelle-спецификаций в основном используются два — product и list. Декларация color РР = product АА ВВ СС определяет множество цветов, состоящее из всех троек вида (о, 6, с), где а є АА, Ъ Є ВВ и с Є СС. Элементами множества цветов LL, согласно декларации color LL = list АА, являются все списки, состоящие из элементов множества АА, Значения последнего множества цветов представляются как [uj, v2,..., vn\ либо в виде выражения h :: і, где h — первый элемент, или голова, списка, at — список без первого элемента, или хвост списка. Дія пустого списка используются обозначения [] или nil.
Соединение точек взаимодействия
В заключение, рассмотрим, каким образом в сети будет представлена линия связи, изображенная на рис. 1.5. Отображение цепочки прикреплений pl-p2-p3 и соединения между точками рЗ и р4 требует слияния шести пар мест. В результате такого слияния вся линия связи моделируется в сети двумя "концептуальными" местами. Из всех мест, обозначенных на рис. .1.5 именами M4_to_Ml и ЛП_о_М4, прототипами являются те, для изображения которых использованы более толстые линии. Все остальные — копии. Кроме того, копии мест M4_to_Ml и Ml_fo_M4 присутствуют на полстраницах N-модулей Ml и. М4. По правилам функционирования иерархической сети, если на полстранице N-модуля Ml какой-нибудь N-переход помещает фишку в место-копию Ml_to_MA, эта фишка становится одновременно доступна во всех "образах" этого места на всех страницах сети. Таким образом, N-переходы на полстранице N-модуля М4 могут использовать эту фишку, что соответствует передаче сообщения из конца в конец линии связи.
Для одного и того же модуля в Estelle-спецификации может быть описано несколько тел. На первом этапе моделирования все N-модули, соответствующие экземплярам Е-модуля, были созданы с одинаковой "внешностью", т. е. количество мест, инцидентность и ориентация дуг одинаковы для каждого из таких N-модулей. В разделе инициализации определяется, каким конкретным телом будет обладать экземпляр модуля. На полстранице N-модуля, сопоставленного экземпляру Е-модуля, создается подсеть, которая представляет внутреннюю структуру этого тела модуля.
Сеть, моделирующая тело экземпляра Е-модуля, располагается на полстранице N-модуля, который сопоставлен этому экземпляру. Построение такой сети не зависит от положения экземпляра модуля в иерархии Estelle-спецификации. Все типы, описанные в разделе описаний модуля, преобразуются в множества цветов. Множество локальных состояний модуля также становится множеством цветов, которое заносится в декларации сети.
Каждой переменной и каждому массиву на странице тела Е-модуля соответствует одно место с тем же именем. Фишки в месте-переменной принимают значения из множества цветов, соответствующего типу данной переменной. Как формируется множество цветов места, соответствующего массиву, описано в п. 2.1. На странице также создается место State множество цветов для которого определяется множеством локальных состояний Е-модуля. Все места на странице тела модуля получают начальную разметку. При инициализации фишки, помещаемые в места, имеют либо "нулевое" значение, либо значение, указанное в разделе инициализации. Под нулевым подразумевается значение О для тех типов данных, где оно присутствует, или значение, минимальное относительно порядка, который определен для соответствующего типа, например, для перечислимого типа таким значением будет первое из перечисленных. Если в модуле не определено множество локальных состояний, то место State инициализируется бесцветной фишкой.
В результате на странице тела экземпляра Е-модуля присутствуют следующие места: - по два места-копии для каждой внешней точки взаимодействия Е-модуля; - по два места для каждой внутренней точки взаимодействия; - по одному месту-копии для каждого параметра и экспортируемой переменной, описанных в заголовке Е-модуля; - по одному месту для каждой переменной и массива; - место State. Каждому Е-переходу, описанному в теле экземпляра Е-модуля, сопоставляется один N-модуль. Если Е-переход использует какой-нибудь ресурс (переменную, параметр или точку взаимодействия), то место, представляющее этот ресурс, становится входным и выходным для соответствующего N-модуля. Место State — входное и выходное для всех N-модулей. Построение сети на подстранице каждого из этих N-модулей.— следующий этап отображения Estelle-спецификации в раскрашенную сеть. Проиллюстрируем отображение тела Е-модуля на примере экземпляра ms модуля sender спецификации example, приведенной в п. 1.1.3. Данный модуль имеет два локальных состояния: wait и deliver. Следовательно, декларации сети будут дополнены новым множеством цветов: На странице присутствует четыре места (см. рис.2.6), соответствующих точкам взаимодействия. Места ms__to_mrl и mr_to_msl возникают при отображении соединения между точками si и rl, a ms_io_mr2 и mr_to_m$2 — между точками s2 и г2. Места ms_to_mrl и mr_tojms2 оказываются изолированными, т. е. не соединены ни с каким N-модулем. Это происходит из-за того, что через оба соединения поток сообщений идет только в одну сторону. Изолированные места никак не влияют на функционирование сети и могут быть удалены. Сеть содержит два N-модуля — transl, trans2 — по числу переходов в модуле sender. Место j соответствует переменной с теми же именами, его начальная разметка — фишка со значением 0. Начальная разметка места State — фишка цвета wait. Подробно рассмотрим соединение мест с переходом transl. Первый переход Е-модуля отправляет сообщение через точку s2. Значение параметра сообщения msg определяется значением переменной j. Поэтому в сети место ms_to_mr2 — входное и выходное для перехода trans 1. Входными и выходными для него будут также места j и State. Аналогичным образом происходит соединение с местами для перехода trans2.
Обоснование алгоритма построения и оценка размера сети
Структура моделирующей сети. Время задержки Е-перехода отсчиты-вается переходом timer с интервалом срабатывания [dl,d2]. Данный переход связан с местами switch и fir и не зависит от "внешних" мест, таких как место State, которые доступны переходам сети, относящимся к другим Е-переходам. Фишки в месте switch принимают значення из множества цветов {0, 1}. Наличие фишки со значением 0 в месте switch означает, что таймер задержки для рассматриваемого Е-перехода выключен. Фишка со значением 1 соответствует включенному таймеру. Начальная разметка места switch — 0. Место fir может содержать бесцветные фишки, изначально оно пустое.
Подсеть, служащая для моделирования приставки delay(dl,d2), содержит также места епЫ и s__ ch. Множеством цветов для места епЫ служит множество {0, 1}. Фишка цвета 0 в месте епЫ означает, что условие возможности для Е-перехода не выполнено. Фишка цвета 1 соответственно означает, что рассматриваемый Е-переход возможен. Начальная разметка места епЫ — фишка цвета 0. Место s_ ch может содержать бесцветные фишки. Начальная разметка данного места — одна бесцветная фишка.
Включение и выключение таймеров задержки Е-переходов после некоторого такта вычислений должны происходить до того, как начнется следующий такт вычислений. Поэтому первый переход подсети приставки provided получает максимальный приоритет. Интервал срабатывания [0,0] в этом случае не дает нужного результата, так как в сети может существовать переход timer, ожидающий 32 единиц времени. Чтобы проверка истинности приставки provided происходила только после завершения очередного такта вычислений, для каждого Е-перехода с задержкой создается место s_ ch — входное для первого перехода подсети для приставки provided. Кроме того, место s_ ch становится выходным для служебных переходов end всех подсетей, которые моделируют Е-переходы, принадлежащие тому же модулю, что и рассматриваемый. Таким образом, в начале моделирования спецификации происходит проверка истинности приставок provided всех Е-переходов с задержками, которые используют фишки, содержащиеся в местах s_ ch при начальной разметке. В дальнейшем проверка происходит только после того, как завершается выполнение некоторого Е-перехода.
Все места, за исключением места s_ ch, и переходы, входящие в подсеть приставки delay, располагаются на странице, где моделируется блок Е-перехода. Место з_ ch создается на странице тела Е-модуля, так как связано с переходами, относящимися ко всем остальными Е-переходам, принадлежащим тому же модулю. Оно является входным и выходным для N-модуля, сопоставленному рассматриваемому Е-переходу, и только выходным для всех остальных N-модулей на странице тела Е-модуля.
В результате проверки истинности приставки provided, т. е. срабатывания всех переходов моделирующей его сети, из места s__ch изымается бесцветная фишка, а в месте епЫ фишка заменяется на фишку, значение которой совпадает со значением предиката возможности, независимо от исходного значения фишки в месте епЫ. Все остальные фишки, значения которых использовались при вычислении, возвращаются в соответствующие места без изменений.
Переход set срабатывает, если значения фишек в местах епЫ и switch различаются, что происходит, когда переход впервые стал возможен либо произошло нарушение условия возможности из-за выполнения другого Е-перехода.
Включение таймера Е-перехода. Рассмотрим работу сети, моделирующей приставку delay(dl,d2). Пусть Е-переход впервые стал возможен. При этом после проверки истинности условия provided место епЫ содержит фишку со значением 1, а место switch — фишку со значением 0. Возможно срабатывание перехода set, при котором фишка в месте switch заменяется на фишку со значением 1, а в место епЫ фишка возвращается без изменения. С этого момента начинает отсчитываться задержка Е-перехода: его выполнение не может начаться, пока не сработает переход timer.
Если после этого происходит выполнение другого Е-перехода, которое не нарушает условия возможности рассматриваемого Е-перехода, то после вычисления значения приставки provided значения фишек в местах епЫ и switch по-прежнему совпадают. Переход set в такой ситуации не может сработать, и отсчет задержки продолжается.
Если условие возможности не было нарушено, переход timer срабатывает в некоторый момент времени из интервала [dl, d2] начиная с момента, когда моделируемый Е-переход впервые стал возможен. При этом фишка цвета 1 изымается из места switch, а в место fir помещается бесцветная фишка. Если в этот момент место епЫ все еще содержит фишку 1, то срабатывание перехода start начнет выполнение Е-перехода. При этом изымаются фишки из мест State и епЫ. По окончании выполнения Е-перехода служебный переход end возвращает фишку в место State, помещает по фишке в места s_ ch для всех Е-переходов, которые имеют задержки. Кроме того, происходит восстановление исходной разметки подсети, моделирующей задержку рассматриваемого Е-перехода: в места епЫ и switch помещается по фишке со значением 0.
Выключение таймера Е-перехода. Выключение таймера Е-перехода может осуществляться переходами set и reset. Если рассматриваемый Е-переход перестал быть возможным в результате выполнения другого Е-перехода, то в месте епЫ фишка со значением 1 заменяется фишкой 0, что делает невозможным срабатывание перехода start. После этого необходимо выключить таймер Е-перехода и восстановить разметку подсети, моделирующей приставку delay. Если срабатывание перехода timer еще не произошло, возможен переход set. Его срабатывание замещает фишку 1 в месте switch на фишку 0, что делает невозможным срабатывание перехода timer. В противном случае, срабатывание перехода reset изымает бесцветную фишку из места fir и помещает фишку 0 в место switch, восстанавливая исходную разметку подсети для приставки delay.
Моделирование приставок delay (dl) и delay (di, ) отличается от моделирования приставки delay(dl,d2) выбором интервала срабатывания перехода timer. Приставке delay (dl) соответствует интервал [dl, dl], а приставке delay (dl, ) — [dl, со].
Моделирование Е-переходов с задержками изменяет правило отображения приоритетов Е-переходов. Необходимо учитывать тот факт, что максимальным приоритетом среди переходов сети должны обладать только первые переходы подсетей для приставок provided. .. Поэтому, если среди Е-переходов имеется Е-переход с максимальным приоритетом, приоритеты всех Е-переходов необходимо уменьшить. В противном случае новый такт вычисления может начаться раньше, чем будет проверено условие возможности Е-переходов. Приоритет приписывают моделирующему N-переходу, если он один, или служебному переходу start в противном случае.
Как было отмечено, поведение модулей внутри подсистем синхронизируется, фазы управления чередуются с тактами вычисления. В течение фазы управления из множества готовых переходов выбираются переходы, которые будут выполняться на следующем такте вычисления. Выбирается не более одного перехода в каждом модуле. Выбор переходов управляется отношением родитель-наследник и классами модулей.
