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

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

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

Окунишникова Елена Валерьевна

МОДЕЛИРОВАНИЕ ESTELLE-СПЕЦИФИКАЦИЙ

РАСПРЕДЕЛЕННЫХ СИСТЕМ С ПОМОЩЬЮ РАСКРАШЕННЫХ СЕТЕЙ ПЕТРИ

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

Автореферат диссертации на соискание ученой степени кандидата физико-математических наук

Новосибирск, 2004

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

Научный руководитель: Официальные оппоненты:

Ведущая организация:

кандидат физико-математических наук Непомнящий В.А.

доктор физико-математических наук Ломазова И.А.

кандидат физико-математических наук Скопин И.Н.

Ярославский государственный университет (г. Ярославль)

Защита состоится 14 сентября 2004 года в 15 час. 00 мин. на заседании диссертационного совета К003.032.01 в Институте систем информатики им А. П. Ершова Сибирского отделения РАН по адресу:

630090, г.Новосибирск, пр. Лаврентьева, 6.

С диссертацией можно ознакомиться в читальном зале библиотеки ИСИ СО РАН (пр. Лаврентьева, 6).

Автореферат разослан " /О " августа 2004 г.

Ученый секретарь диссертационного совета К003.032.01

к.ф.-м.н. IЧ*,, ь, (_ Мурзин Ф.А

ОБЩАЯ ХАРАКТЕРИСТИКА РАБОТЫ

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

Распространение сетей Петри и их различных модификаций в качестве модели, используемой для спецификации распределенных систем, обусловлено тем, что они сочетают строгую, хорошо проработанную формальную теорию с наглядным графическим представлением. Систематическое изучение свойств сетей Петри началось на рубеже 60-х и 70-х годов и продолжается по сей день. Среди отечественных авторов, в разное время занимавшихся исследованиями в области сетей Петри, можно отметить Н.А.Анисимова, О.Л.Бандман, И.Б.Вирбицкайте, В.Е.Котова, И.А.Ломазову, В.А.Соколова, Л.А.Черкасову и многих других. Раскрашенные сети Петри (РСП), предложенные К.Йенсеном, получили широкое признание как удобный, мощный и эффективный механизм для спецификации и верификации свойств распределенных систем, что подтверждается ведущимися работами по принятию РСП в качестве стандарта ISO.

С другой стороны, на практике используются языки выполнимых спецификаций, "лидерами" среди которых являются языки Estelle (стандарт ISO) и SDL (стандарт ITU). Языки выполнимых спецификаций имеют формальный базис, а их близость к языкам программирования облегчает процесс последующей реализации. Однако способы анализа выполнимых спецификаций остаются предметом исследования. Поэтому широко используется практика отображения спецификаций в формальные модели, для которых существуют эффективные методы анализа и автоматические средства верификации. Известны примеры транс-

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

Опубликован ряд работ по трансляции SDL-спецификаций в различные классы сетей Петри, среди которых можно выделить два направления. Первое использует известные классы сетей Петри высокого уровня, такие как PrT-сети (работы Е. Кеттунена и Н. Хусберга) и М-сети (работы Б.Гралмана). Для второго характерно создание новых классов сетей Петри, ориентированных на язык (работы Й.Фишера и Ф.Баузе).

Для Estelle-спецификаций в работе Ж.Л.Ричье, Й.Сифакиса и др. предложен метод автоматического построения конечно-автоматных моделей посредством исчерпывающей симуляции, позволяющий верифицировать некоторые свойства коммуникационных протоколов. В работах В. Димитрова ограниченное подмножество Estelle отображается в ординарные сети Петри. А. Яновская и П. Яновский предлагают способ перевода подмножества Estelle, не включающего динамических возможностей Estelle, времени и приоритетов, в темпоральную логику TLA+.

В работах Р. Лая и А. Джирачифпаттаны предложен метод отображения Estelle-спецификаций в нумерические сети Петри, который рассматривает подмножество языка, включающее динамические конструкции. Однако время и приоритеты не рассматриваются. Помимо этого, данный метод требует предварительной ручной обработки Estelle-спе-цификаций. В более поздних работах Р. Лая и Т. Цанга для моделирования поведения, явно зависящего от времени, используются модульные сети Петри. Однако в этих работах авторы рассматривают не стандартный Estelle, а предлагают расширение языка, приближающее его к языкам реального времени. Кроме того, реализация предложенных методов упоминается только как тема для исследования. Моделирование выполняется отдельно для каждого примера, что приводит к необходимости верификации процесса моделирования.

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

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

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

Методы исследования базируются на применении аппарата сетей Петри и языка выполнимых спецификаций Estelle.

Научная новизна состоит в следующем.

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

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

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

Дано обоснование предложенного алгоритма. Введен аналог свойства безопасности — послойная безопасность. Показано, что сеть, мо-

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

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

Апробация работы. Основные научные и практические результаты подробно обсуждались на объединенном семинаре ИСИ СО РАН и кафедры программирования НГУ "Теоретическое и экспериментальное программирование", докладывались на следующих научных конференциях:

1. 3rd International Conference on Parallel Computing Technologies, St.Pe-tersburg, Russia, 1995.

2. IFIP 15th International Symposium on Protocol Specification, Testing and Verification, Warsaw, Poland, 1995.

3. Third International Workshop on Concurrency, Specification and Programming, Warsaw, Poland, October 1997.

4. 15-th IMACS World Congress on Scientific Computation, Modelling and Appl, Berlin, Germany, 1997.

5. International Conference on Parallel Computing in Electrical Engineering, Bialystok, Poland, 1998.

6. 1st International Workshop on the Formal Description Technique Estelle, Evry, France, 1998.

7. Четвертый Сибирский Конгресс по Прикладной и Индустриальной Математике (ИНПРИМ-2000), Новосибирск, Россия, 2000.

8. Конференция молодых ученых, посвященная 10-летию ИВТ СО РАН, Новосибирск, Россия, 2000.

Работа поддерживалась следующими грантами: РФФИ 93-01-986, 1993—1995; Международного Научного Фонда и Российского правительства, JCP 100, 1994; ИНТАС 1010-СТ93-0042, 1993-1994; ИНТАС-РФФИ N 95-0378, 1997—1999; Президиума СО РАН Поддержки международных проектов, 1997.

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

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

КРАТКОЕ СОДЕРЖАНИЕ РАБОТЫ

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

В первой главе дано описание языка формальных описаний Estelle и краткое напоминание основных понятий теории раскрашенных сетей, предложенных Йенсеном. Приставки Е- и N- используются для обозначения объектов (модуля, перехода) Estelle и сети соответственно.

В разд. 1.1 приводятся необходимые сведения о языке Estelle, основанном на объединении конечного автомата с языком программирования Pascal и добавлении элементов описания архитектуры системы, которая определяется иерархически организованным множеством модулей и структурой их взаимосвязей. Для взаимосвязи между модулями служат двунаправленные каналы между портами (точками взаимодействия).

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

его выходное место. Значения фишек определяются выражениями на соответствующих дугах.

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

В разд. 1.3 для РСП вводятся приоритеты и два временных механизма. Во временных сетях, предложеных Мерлином, каждому переходу приписывается интервал срабатывания где определяет минимальное время, которое должно пройти до того момента, как возможный переход сработает, а — максимальное время, в течение которого переход может оставаться возможным и не сработать. Второй механизм, предложенный Иенсеном, использует понятия глобальных часов и временных штампов фишек. Глобальные часы показывают текущее время в сети. Значение временного штампа определяет, когда фишка может быть использована: фишка остается недоступной для переходов, пока текущее время и значение ее временного штампа не станут равны. Временной штамп фишки может определяться как переходом, так и дугой, по которой фишка "поступила" в место.

Сети с приоритетами — это сети, в которых каждому переход}' сопоставлено некоторое неотрицательное целое число. Возможный переход может сработать, если его приоритет не меньше приоритета любого другого возможного перехода.

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

В разд. 2.1 рассматриваются правила преобразования предопределенных типов Estelle в множества цветов РСП.

В разд. 2.2 описывается отображение иерархии модулей в дерево страниц РСП. Корнем является страница, на которой представлена общая структура спецификации. Отображение Е-модуля происходит по одной схеме независимо от его положения в иерархии спецификации. Каждому экземпляру Е-модуля сопоставляется модуль сети. На подстранице этого ^модуля располагается сеть, которая отображает структуру тела Е-модуля и содержит по одному ^модулю для каждого из модулей-наследников, описанных в Е-модуле. Для каждого из наследников процедура повторяется.

В разд. 2.3 рассматривается моделирование формальных параметров и экспортируемых переменных- Каждый параметр или переменная представляются местом на странице тела модуля-родителя. Это место соединяется с ^модулем, соответствующим Е-модулю, где описан параметр или переменная.

Разд. 2.4 посвящен отображению структуры связей. Каждая точка взаимодействия Е-модуля представляется двумя местами, одно из которых представляет очередь исходящих сообщений, а второе — очередь сообщений, полученных Е-модулем через точку взаимодействия. Места, которые представляют две точки взаимодействия, связанные каналом, сливаются между собой таким образом, чтобы сохранялось направление передачи сообщений.

В разд. 2.5 описывается моделирование тела Е-модуля. Каждая переменная представлена на странице тела Е-модуля одним местом. Начальная разметка мест на странице тела Е-модуля определяется разделом инициализации спецификации. Каждому Е-переходу, описанному в теле Е-модуля, сопоставляется ^модуль. Если Е-переход использует какой-нибудь ресурс (переменную, параметр или точку взаимодействия), то место, представляющее этот ресурс, соединяется с соответствующим ^модулем.

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

ставляется фрагмент сети. Фрагменты последовательно соединяются с помощью служебных мест.

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

Разд. 2.7 содержит описание моделирования отложенных Е-пере-ходов. Подсеть, моделирующая Е-переход с задержкой, состоит из трех частей: 1-я часть представляет приставку provided, 2-я реализует механизм задержки Е-перехода, а 3-я — блок Е-перехода. Время задержки Е-перехода отсчитывается переходом timer, интервал срабатывания которого совпадает с интервалом, указанным в приставке delay.

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

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

Утверждение 1. Сеть, получающаяся в результате отображения Estelle-спецификации, безопасная.

Состояние Е-модуля и разметка моделирующей его сети называются эквивалентными при следующих условиях:

- значение фишки в месте State совпадает с текущим локальным состоянием Е-модуля;

- для каждой точки взаимодействия Е-модуля число сообщений в очереди этой точки совпадает с длиной списка в соответствующем месте, и порядок сообщений совпадает;

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

Утверждение 2. Если Е-переход возможен из некоторого состояния Е-модуля, то в сети из эквивалентной разметки может произойти

последовательное срабатывание всех переходов, входящих в сеть, которая моделирует этот Е-переход. Полученные таким образом состояние и разметка будут снова эквивалентны.

Пусть Е-модуль содержит var переменных, ip точек взаимодействия, par параметров и t переходов. Среди общего числа п операторов Е-модуля выделим с вызовов процедур н функций и к операторов, для моделирования которых заведомо требуется более одного перехода. Через att = var + 1 + 2 * ip + par обозначим число "значимых" мест.

Утверждение 3. Сеть, моделирующая Е-модуль, может иметь не более TN переходов и PN мест, где TN — (п + 4к) * (с + 1) + At, PN = (n + att + 4к) * (с + 1) + 51.

В третьей главе предлагается алгоритм отображения динамических Estelle-спецификаций в РСП, расширенных приоритетами и временным механизмом Йенсена. Рассматриваются только спецификации, допускающие последовательное недетерминированное поведение. Подход основан на том, что текстуальная вложенность описаний модулей образует статический шаблон спецификации. Число экземпляров модуля может изменяться в процессе выполнения, но позиция в общей иерархии фиксирована. При моделировании Estelle-спецификаций статическая структура сети представляет иерархию описаний. Экземпляры модулей моделируются фишками, число которых изменяется при создании или уничтожении экземпляров модулей.

Разд. 3.1 посвящен построению дерева страниц моделирующей сети. Правила в целом подобны описанным в разд. 2.2, но элементы сети сопоставляются не конкретному экземпляру, а описанию Е-модуля определенного типа. Заголовку Е-модуля сопоставляется один N-модуль, на подстранице которого создается по одному N-модулю для каждого тела Е-модуля. Внутренняя структура тела Е-модуля моделируется на подстранице N-модуля, представляющего это тело.

В разд. 3.2 обсуждается проблема идентификации экземпляров модулей. Фишки, принадлежащие разным экземплярам, снабжаются уникальным признаком — персональным идентификатором модуля (ПИМ). Все фишки, принадлежащие одному экземпляру модуля, помечены одним и тем же ПИМ.

В разд. 3.3 рассматривается моделирование формальных парамет-

ров и экспортируемых переменных Е-модуля. От статического случая его отличают правила порождения множеств цветов и выражения на дугах: всюду хранится и передается не просто значение соответствующего типа, а пара (ПИМ, значение).

Разд. 3.4 посвящен отображению точек взаимодействия. Точка взаимодействия Е-модуля представляется тремя местами. К двум местам, представляющим очереди входящих и исходящих сообщений, добавляется место IPinfo, которое служит для хранения информации о том, какие связи установлены для точки взаимодействия IP.

В разд. 3.5 и 3.6 описывается моделирование операторов установления и разрыва связей соответственно. Так как связи между точками могут изменяться, слияния мест, содержащих очереди сообщений, не происходит. Связь между точками взаимодействия, которая может возникнуть в процессе функционирования спецификации, представляется двумя переходами. Каждая пара переходов моделирует перемещение сообщений по соединяющему точки каналу. Установление и разрыв связей изменяют значения фишек в местах IP info для точек взаимодействия, между которыми была создана или уничтожена связь.

В разд. 3.7 рассматривается организация ввода/вывода с учетом того, что Е-модуль может иметь доступ к очередям точки взаимодействия только в том случае, если эта точка является концом линии связи.

Разд. 3.8 посвящен моделированию тела Е-модуля. Каждому типу модулей-наследников, описанных в теле, сопоставляется N-модуль, отображаются точки взаимодействия и возможные связи между ними. Для каждого типа модулей-наследников Т создаются места T_inst, Т_тИ и Т_Ы1 Место T_inst хранит информацию о существующих на данный момент экземплярах модулей типа Т, а места Tinit и Т_кШ используются при создании и уничтожении экземпляров модулей этого типа. Построение той части сети, которая определяет функционирование Е-модуля, в целом подобно статическому случаю.

В разд. 3.9 описывается отображение Е-переходов. Рассматриваются библиотечные фрагменты, моделирующие операторы all, for one и exist, которые позволяют оперировать с экземплярами модулей-наследников. Обсуждается структура сети, моделирующей отложенные Е-переходы в терминах временной модели Йенсена.

В разд. 3.10 рассматривается создание и уничтожение экземпляров Е-модулей. Создание нового экземпляра некоторого типа заключается в размещении по всем "значимым" местам сети, моделирующей тело Е-модуля, набора фишек, который помечен новым ПИМ. Уничтожение экземпляра представляет собой обратное действие. Из мест сети удаляются все фишки, которые помечены ПИМ, полученным от модуля-родителя.

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

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

Утверждение 4. Сеть, полученная в результате отображения ЫеПе-спецификаций, содержащих динамические конструкции, послойно безопасна.

Состояние Е-модуля и разметка моделирующей его сети называются эквивалентными при следующих условиях:

- выполняются условия эквивалентности, приведенные в разд. 2.9;

- фишки в местах IP_info описывают текущую структуру связей согласно правилам, описанным в разд. 3.4-3.6;

- каждый модуль-наследник М типа Т представлен в месте T_inst фишкой, содержащей информацию о типе тела и ПИМ экземпляра наследника.

Утверждение 5. Если Е-переход возможен из некоторого состояния Е-модуля, то в сети из эквивалентной разметки может произойти последовательное срабатывание всех переходов, входящих в сеть, которая моделирует этот Е-переход. Полученные таким образом состояние

и разметка будут снова эквивалентны.

Пусть Е-модуль содержит var переменных, ip точек взаимодействия, par параметров и t переходов. Среди общего числа п операторов Е-модуля выделим с вызовов процедур и функций и к операторов, для моделирования которых заведомо требуется более одного перехода. Число "значимых" мест в модуле будет равно

Утверждение 6. Сеть, моделирующая Е-модуль, может иметь не более TN переходов и PN мест, где TN = {п + 5к) * (с + 1) + 2t, PN = (n + att + 4Jt) * (с + 1) + 4t.

В четвертой главе в разд. 4.1 описана система EPV, представляющая собой интегрированный программный комплекс для проектирования, анализа и симуляции сетевых моделей распределенных систем. В качестве сетевых моделей используются ИВТ-сети, являющиеся вариантом раскрашенных сетей. В ИВТ-сетях используется концепция времени, предложенная Мерлином, допускается тип массив и могут присутствовать места-очереди, где новая фишка "помещается в очередь" и остается недоступной, пока из места не будут извлечены все фишки, поступившие до нее.

Основными компонентами комплекса являются транслятор, конвертор, графический редактор и симулятор. Транслятор осуществляет автоматический перевод Estelle-спецификации во внутреннее представление ИВТ-сети. Конвертор переводит ИВТ-сети в текстовое представление, являющееся входным для системы Design/CPN. Таким образом, система EPV позволяет использовать средства анализа системы Design/CPN. Средствами многооконного графического редактора ИВТ-сетей осуществляется построение и изменение сетевой модели и контроль структурной корректности иерархических сетевых моделей. Си-мулятор интегрирован с редактором и визуализирует функционирование ИВТ-сетей, а также позволяет протоколировать сеанс симуляции.

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

ция покидает кольцо, разрыва кольца не происходит: кадр передается сквозь нее далее по кольцу.

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

В приложении приведена Е81е11е-спецификация ЯЕ-протокола.

Основные выводы и результаты

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

♦ Разработан алгоритм перевода статических Ейе11е-спецификаций с задержками и приоритетами в расширенную модель раскрашенных сетей. Доказано, что алгоритм дает безопасные сети. Дано обоснование предложенного алгоритма. Получены верхние оценки размера моделирующей сети, подтверждающие эффективность алгоритма.

♦ Разработан способ моделирования Ые11е-спецификаций с динамическими конструкциями и алгоритмы перевода последних в раскрашенные сети Петри. Для моделирующей сети доказан аналог свойства безопасности. Дано обоснование предложенного алгоритма. Приведена оценка размера моделирующей сети.

♦ Метод перевода статических Ые11е-спецификаций адаптирован для модели ИВТ-сетей, реализованной в системе ЕРУ. Проведены эксперименты по поиску семантических ошибок в коммуникационных протоколах. В ходе экспериментов с кольцевым протоколом, известным как КЕ-протокол, обнаружена неэффективность в поведении протокола. Предложено исправление протокола, устраняющее эту неэффективность.

ПУБЛИКАЦИИ ПО ТЕМЕ ДИССЕРТАЦИИ

1. Окунишникова Е. В. Отображение Estelle-спецификаций в раскрашенные сети Петри и его обоснование. — Новосибирск, 2001. — 59 с. — (Препр./Сиб. отд-ние РАН. ИСИ; N 90)

2. Непомнящий В. А., Алексеев Г. И., Быстрое А. В., Мыльников С. П., Окунишникова Е. В., Чубарев П. А., Чурина Т. Г. Верификация коммуникационных протоколов, представленных на языке Estelle, с помощью сетей Петри высокого уровня // Программирование. — 2001. — N. 2. - С. 5-20.

3. Окунишникова Е. В. Моделирование Estelle-спецификаций посредством раскрашенных сетей Петри // Тр. конф. молодых ученых, посвященной 10-летию ИВТ СО РАН. Т. I: Информационные технологии, задачи поддержки принятия решений. — Новосибирск: Пн-т вычислит, технологий СО РАН, 2001. - С. 59-61.

4. Окунишникова Е. В. Моделирование Estelle-спецификаций посредством раскрашенных сетей Петри // Тез.докл. IV сибирского конгресса по прикладной и индустриальной математике (ИНПРИМ-2000): — Новосибирск: Ин-т математики СО РАН, 2000. - С. 124.

5. Непомнящий В. А., Алексеев Г. И., Выстров А. В., Мыльников С. П., Окунишникова Е. В., Чубарев П. А., Чурина Т. Г. Верификация коммуникационных протоколов, представленных на языках Estelle и SDL // Там же. — С. 123.

6. Окунишникова Е. В. Моделирование динамических конструкций языка Estelle посредством раскрашенных сетей Петри. — Новосибирск, 2000.

- 70 с. - (Препр./Сиб. отд-ние РАН. ИСИ; N 78)

7. Алексеев Г. И., Быстрое А. В., Куртов С. А., Мыльников С. П., Непомнящий В. А., Окунишникова Е. В., Чубарев П. А., Чурина Т. Г. Использование сетей Петри для верификации распределенных систем, представленных на языке Estelle // Известия РАН. Сер. Теория и системы управления. — 1999. — N. 5. — С. 105-116.

8. Окунишникова Е. В. Представление временных конструкций Estelle в различных моделях временных сетей Петри. — Новосибирск, 1999. — 32 с.

- (Препр./Сиб. отд-ние РАН. ИСИ; N 70)

9. Непомнящий В. А., Алексеев Г. И., Выстров А. В., Куртов С. А., Мыльников С. П., Окунишникова Е. В., Чубарев П. А., Чурина Т. Г. Верификация Estelle-сиецификаций распределенных систем посредством раскрашенных сетей Петри. — Новосибирск: ИСИ СО РАН, 1998.

- 140 с.

10. Churina T. G., Okunishnikova E. V. Modelling Estelle specifications using Coloured Petri nets.// Joint Bulletin ofthe NCC and the IIS . Ser. Computer Science. - 1998. - N 8. - P. 19-39.

11. Nepomniaschy V. A., Alekseev G. I., Bystrov A. V., Churina T. G., Mylnikov S. P.,Okunishnikova E. V. Towards Verification of Estelle-specified Communication Protocols: Coloured Petri Net Approach // Proc. Int. Conf. on Parallel Computing in Electrical Engineering. — Bialystok, Poland, 1998, P. 141-147.

12. Nepomniaschy V. A., Alekseev G. I., Bystrov A. V., Churina T. G., Mylnikov S. P., Okunishnikova E. V. EPV — Petri Net Based Estelle Protocol Verifier // Proc. 1st Intcrnati. Workshop on the Formal Description Technique Estelle. — Evry, France, 1998. — P. 101-108.

13. Churina T. G., Okunishnikova E. V. Coloured Petri nets approach to the validation of Estelle specifications // Proc. of Workshop on Concurrency, Specification and Programming. — Warsaw, Poland, 1997. — P. 25—36.

14. Nepomniaschy V. A., Alekseev G. I., Bystrov A. V., Churina T. G., Mylnikov S. P., Okunishnikova E. V. Petri net modelling of Estelle-specified communication protocols // Proc. 3rd Int. Conf. Parallel Computing Technologies. — Berlin a. o.: Springer-Verlag, 1995. — P. 94—108. — (Lect. Notes Comput. Sci., Vol. 964).

15. Окунишникова Е. В., Чурина Т. Г. Способ построения раскрашенных сетей Петри, моделирующих Estelle-спецификации // Проблемы спецификации и верификации параллельных систем. — ПСИ СО РАН, Новосибирск, 1995. — С. 95-123.

16. Nepomniaschy V. A., Churina Т. G., Okunishnikova E. V. Translation of Estelle protocol specification in coloured Petri nets. Extended Abstract // Proc. IFIP 15th Intern. Sympos. on Protocol Specification, Testing and Verification. — Warsaw, Poland, 1995. — P. 447-450.

Личный вклад автора

Все включенные в диссертацию результаты, касающиеся моделирования динамических возможностей Estelle, получены автором самостоятельно. В работах по моделированию статических Estelle-спецификаций, выполненных в соавторстве, Е. В. Окунишннкова внесла следующий вклад: разработано отображение в РСП точек взаимодействия модулей Estelle и связей между ними, моделирование Е-переходов с простым блоком, а также процедур и функций; разработаны принципы представления в сети временных конструкций Estelle; доказана безопасность моде-

лирующей сети, обоснована корректность алгоритма построения, даны оценки размера моделирующей сети; на основании разработанного алгоритма выделен эффективный подкласс РСП, получивший название ИВТ-сетей, использованный в дальнейшем при создании системы EPV; проведены и описаны эксперименты с кольцевым протоколом.

Окунишникова Елена Валерьевна

МОДЕЛИРОВАНИЕ ESTELLE-СПЕЦИФИКАЦИЙ РАСПРЕДЕЛЕННЫХ СИСТЕМ С ПОМОЩЬЮ РАСКРАШЕННЫХ СЕТЕЙ ПЕТРИ

Объем 1,0 уч.-изд.л. Тираж 100 экз.

Подписано в печать 27.07.04 Формат бумаги 60x84 1/16

ЗАО РИЦ "Прайс-курьер" 630090, г. Новосибирск, пр. Акад. Лаврентьева, 6, тел. (383-2) 34-22-02,

14239

Введение

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

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

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

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

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

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

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. Моделирование статических Estelle-спецификаций посредством раскрашенных сетей

2.1 Отображение предопределенных типов Estelle.

2.2 Отображение иерархии модулей

2.3 Формальные параметры и экспортируемые переменные.

2.4 Точки взаимодействия и структура связей.

2.5 Отображение тела модуля.

2.6 Моделирование Estelle-перехода.

2.6.1 Приставка provided.

2.6.2 Представление стандартных операторов.

2.6.3 Отображение процедур и функций.

2.7 Моделирование отложенных Е-переходов.

2.8 Моделирование такта вычисления.

2.8.1 Последовательное выполнение.

2.8.2 Параллельное выполнение.

2.9 Обоснование алгоритма построения и оценка размера сети

Глава III. Моделирование динамических Estelle-спецификаций посредством раскрашенных сетей

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 Моделирование Estelle-перехода.

3.9.1 Специфические операторы Estelle.

3.9.2 Процедуры и функции.

3.9.3 Моделирование Е-переходов с задержками

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

3.10.1 Создание экземпляра модуля.

3.10.2 Уничтожение экземпляра модуля.

3.11 Моделирование такта вычисления.

3.12 Обоснование алгоритма построения и оценка размера сети

Глава IV. Эксперименты

4.1 Программный комплекс EPV.

4.2 Кольцевой протокол.

4.2.1 Описание протокола

4.2.2 Estelle-спвцификация RE-протокола.

4.2.3 Сетевая модель RE-протокола

4.2.4 Эксперименты с кольцевым протоколом.

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

Формальные модели, используемые в настоящий момент для спецификации распределенных систем можно классифицировать по различным признакам. Один из подходов подразделяет их на автоматные модели и модели последовательностей [6]. Автоматные модели рассматривают внутреннее состояние объекта спецификации и описывают все возможные изменения этого состояния при воздействии на объект. К моделям этого вида относят конечные автоматы, различные виды сетей Петри, автоматы, расширенные переменными и т. д. Модели последовательностей рассматривают только наблюдаемое извне поведение объекта, не делая никаких предположений о его внутренней структуре. К ним относят алгебры взаимодействующих процессов, описания, использующие временные логики и пр.

Известны примеры непосредственного моделирования распределенных систем с помощью методов первой или второй группы. Так в работах Р.Коэна и А.Сегала [37] и Г. И. Холцмана [46] использовались конечные автоматы, а в работе К. Сибертин-Бланка [75] — ординарные сети Петри, а Т. Pyssysalo и JI. Оджала [72] — PrT(predicate-transition)-ceTH. В России также велись исследования в этом направлении. Среди них следует отметить в частности, работы О. JI. Бандман [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 (Estelle Protocol Verifier), а также проведены эксперименты по отладке реализации алгоритма. В 1998 г. было предложено моделирование для многоуровневых Estelle-спецификаций с задержками и приоритетами [36], описаны результаты экспериментов [10, 70] по сетевому моделированию и поиску ошибок для версий четырех известных протоколов: со скользящим окном [74, 78], кольцевого [37], соединений [66], Inres[40]. В работе [71] предложена методика валидации сетевых моделей системы ЕРV. Моделирование 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.

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

1. 93-01-986 Российского Фонда Фундаментальных исследований. 1993-1995.

2. J CP 100 от Международного Научного Фонда и Российского правительства. 19943. ИНТАС N 1010-СТ93-0042. 1993-1991

4. ИНТАС-РФФИ N 95-0378. 1997-1999.

5. Президиума СО РАН Поддержки международных проектов. 1997.

Апробация работы проведена на следующих международных и отечественных научных конференциях:

• Международные конференции:

1. 3rd International Conference on Parallel Computing Technologies, St.Peters-burg, Russia, 1995.

2. IFIP 15th International Symposium on Protocol Specification, Testing and Verification, Warsaw, Poland, 1995.

3. Third International Workshop on Concurrency, Specification and Programming, Warsaw, Poland, October 1997.

4. 15-th IMACS World Congress on Scientific Computation, Modelling and Appl, Berlin, Germany, 1997.

5. International Conference on Parallel Computing in Electrical Engineering, Bialystok, Poland, 1998.

6. 1st International Workshop on the Formal Description Technique Estelle, Evry, France, 1998.

7. Четвертый Сибирский Конгресс 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] — в местных изданиях.

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

Выводы, сделанные на основании симуляции, подтверждаются результатами экспериментов в системе PNV (Petri net verifier), которая реализует метод проверки моделей для РСП, ограниченных системами с конечным числом состояний, относительно мю-исчисления [8, 58]. Эксперименты проводились для ограниченной модели, не рассматривающей все возможные сбои в работе среды. Тем не менее был промоделирован ряд достаточно общих случаев. После внесения в протокол предложенных выше изменений модель не содержала состояний с повторно принятыми сообщениями.

Заключение

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

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

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

• Метод перевода статических Estelle-спецификаций адаптирован для модели ИВТ-сетей, реализованной в системе EPV. Проведены эксперименты по поиску семантических ошибок в коммуникационных протоколах. В ходе экспериментов с кольцевым протоколом, известным как RE-протокол, обнаружена неэффективность в поведении протокола. Предложено исправление протокола, устраняющее неэффективность.

Остановимся на достоинствах подхода, представленного в настоящей работе. Подмножество языка Estelle, выделенное в гл. 2, позволяет работать со спецификациями, в которых не происходит динамического создания и уничтожения экземпляров модулей, а также не изменяется структура связей. При этом сохраняется возможность использования задержек и приоритетов переходов, что позволяет представить достаточно широкий класс протоколов. Если спецификация не содержит процедур и функций, то оценка размера сети линейна по отношению к количеству операторов, точек взаимодействия, переменных и параметров Estelle-спецификации, в противном случае — квадратичная. Автоматический перевод в ИВТ-сети, реализованный в системе EPV, позволяет проводить валидацию коммуникационных протоколов. Алгоритм перевода генерирует квазибезопасные сети, что избавляет от необходимости перебора вариантов связывания переменных при срабатывании переходов и значительно повышает эффективность моделирования. Реализация предложенного алгоритма существенно сокращает трудоемкость экспериментов и позволяет проводить их на реальных протоколах. Кроме того, автоматический перевод не требует дополнительного процесса проверки правильности построенной сетевой модели протокола.

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

Практическую ценность предложенного подхода подтвердили успешные эксперименты по обнаружению семантических ошибок в различных протоколах. Отметим, что во всех этих примерах размер результирующих сетей значительно меньше теоретических верхних оценок. Среди полученных результатов наиболее интересным является исследование RE-протокола. В диссертации для этого протокола впервые показано, что, невзирая на доказанное в литературе отсутствие live — lock'a,, присутствующего в родственных версиях кольцевых протоколов, RE-протокол содержит существенную неэффективность, которая часто приводит к появлению "лишних" сообщений. Показано, что добавление одного оператора позволяет существенно повысить надежность протокола, что подтверждается результатами верификации методом проверки моделей.

1. Ачасова С. М., Бандман О. JI. Корректность параллельных вычислительных процессов. — Новосибирск: Наука, 1990. — 252 с.

2. Бандман О. JI. Проверка корректности сетевых протоколов с помощью сетей Петри //Автоматика и вычислительная техника. — 1986. — N 6. — С. 82-91.

3. Бестужева И. И., Руднев В. В Временные сети Петри. Классификация и сравнительный анализ //Автоматика и телемеханика. — 1990. — N 10. — С. 3-21.

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

5. Зайцев С. С. Описание и реализация протоколов сетей ЭВМ. — М.: Наука, 1989.

6. Карабегов А. В., Тер-Микаэлян Т. М. Введение в язык SDL. — М.: Радио и связь, 1993.

7. Козюра В. Е., Непомнящий В. А., Новиков Р. М. Верификация раскрашенных сетей Петри методом проверки моделей. — Новосибирск, 2001.- 26 с. (Препр./Сиб. отд-ние РАН. ИСИ; N 89)

8. Котов В. Е. Сети Петри. — М.: Наука, 1984.

9. Непомнящий В. А., Алексеев Г. И., Быстров А. В., Куртов С. А., Мыльников С. П., Окунишникова Е. В., Чубарев П. А., Чурина Т. Г. Верификация Estelle-спецификаций распределенных систем посредством раскрашенных сетей Петри. — Новосибирск, 1998. — 140 с.

10. Окунишникова Е. В. Представление временных конструкций Estelle в различных моделях временных сетей Петри. — Новосибирск, 1999. — 32 с. (Препр./Сиб. отд-ние РАН. ИСИ; N 70)

11. Окунишникова Е. В. Моделирование динамических конструкций языка Estelle посредством раскрашенных сетей Петри. — Новосибирск, 2000. — 70 с. (Препр./Сиб. отд-ние РАН. ИСИ; N 78)

12. Окунишникова Е. В. Моделирование Estelle-спецификаций посредством раскрашенных сетей Петри// Тез.докл. IV сибирского конгресса по прикладной и индустриальной математике (ИНПРИМ-2000). — Новосибирск: Ин-т математики СО РАН, 2000. — С. 124.

13. Окунишникова Е. В. Отображение Estelle-спецификаций в раскрашенные сети Петри и его обоснование. — Новосибирск, 2001. — 59 с. — (Препр./Сиб. отд-ние РАН. ИСИ; N 90)

14. Окунишникова Е. В., Чурина Т. Г. Способ построения раскрашенных сетей Петри, моделирующих Estelle-спецификации // Проблемы спецификации и верификации параллельных систем. — Новосибирск, 1995. — С. 95— 123.

15. Соколов В. А., Легалов А. И. Применение сетей Петри для анализа программ, написанных на языке параллельного программирования //Моделирование и анализ информационных систем. — Ярославль, 1993. — N 1. — С. 27-44.

16. Чурина Т. Г. Способ построения раскрашенных сетей Петри, моделирующих SDL-системы. — Новосибирск, 1998. — 56 с. — (Препр./Сиб. отд-ние РАН. ИСИ; N 56)

17. Чурина Т. Г. Моделирование динамических конструкций языка SDL посредством раскрашенных сетей Петри. — Новосибирск, 1999. — 35 с. — (Препр./Сиб. отд-ние РАН. ИСИ; N 71)

18. Чурина Т. Г. Трансляция SDL-спецификаций в раскрашенные сети Петри// Тез.докл. IV сибирского конгресса по прикладной и индустриальной математике (ИНПРИМ-2000). — Новосибирск: Ин-т математики СО РАН, 2000. С. 128.

19. A Formal description technique based on the temporal ordering of observational behaviour. ISO DP 8807, 1984.

20. Algayres B. et al. VESAR: a pragmatic approach to formal specification and verification // Computer Networks and ISDN Systems. — 1993. — Vol. 25, N 7.- P. 779-790.

21. Algayres B. et al. The AVALON Project: a VALidatiON Environment For SDL/MSC Descriptions //Proc. Int. Conf. on SDL'93. Using Objects — 1993. — P. 221-235.

22. Anisimov N. A., Koutny M. On compositionality and Petri nets in protocol engineering. // Proc. IFIP 15th Intern. Symp. on Protocol Specification, Testing and Verification. — Warsaw, Poland, 1995. — P. 57—72.

23. Anisimov N. A., Kovalenko A. A., Postupalski P. A. Two-levels Formal Model for Protocol Specification Based on Petri Nets //Proc. IFIP TC6 Intern. Symp. Network Information Systems. — Bulgaria, 1993. — P. 143—154.

24. Bause F. et al. SDL and Petri net perfomance analysis of communicating systems // Proc. IFIP 15th Intern. Symp. on Protocol Specification, Testing and Verification. — Warsaw, Poland, 1995. — P. 259—272.

25. Cerone A. A net-based approach for specifying real-time systems: Ph.D.thesis.

26. TD-16/93, Dipartimento di Informatica, University di Pisa, Pisa, Italy, 1993.

27. Berthomieu В., Diaz M. Modelling and verification of time dependent systems using time Petri nets // IEEE Transact, on Software Eng. — 1991. — Vol. 17, N 3. P. 259-273.

28. Bucci G., Vicario E. Compositional validation of time-critical systems using communicating time Petri nets // IEEE Transact, on Software Eng. — 1995. — Vol. 21, N 12. P. 969-991.

29. Budkowski S. Estelle development toolset (EDT) // Computer Networks and ISDN Systems. 1992. - Vol. 25, N 1. - P. 63-82.

30. Budkowski S., Dembinski P. An introduction to Estelle: a specification language for distributed systems // Computer Networks and ISDN Systems. — 1988. — Vol. 14, N 1. P. 3-23.

31. Churina T. G., Okunishnikova E. V. Coloured Petri nets approach to the validation of Estelle specifications // Proc. of Workshop on Concurrency, Specification and Programming. — Warsaw, Poland, 1997. — P. 25—36.

32. Cohen R., Segall A. An efficient reliable ring protocol // IEEE Transact. Communs. 1991. - Vol. 39, N 11. - P. 1616-1624.

33. Courtiat J. P., de Saqui-Sannes P. ESTIM: an integrated environment for the simulation and verification of OSI protocols specified in Estelle // Computer Networks and ISDN Systems. 1992. - Vol. 25, N 1. — P. 83-98.

34. Dimitrov V., Petkov A. Verification oriented Estelle specification of communication protocols // Reseach into Networks and Distributed Applications. — Amsterdam: North-Holland, 1988. — P. 953—960.

35. Ferenc В., Hogrefe D., Sarma A. SDL with applikations from protocol specification. — Englewood Cliffs, NJ: Prentice Hall, 1991.

36. Fisher J., Dimitrov E. Verification of SDL'92 specifications using extended Petri nets // Proc. IFIP 15th Intern. Conf. on Protocol Specification, Testing and Verification. — Warsaw, Poland, 1995. — P. 455—458.

37. Gammelgaard A., Kristensen J.E. A correctness proof of a translation from SDL to CRL //Proc. of the sixth SDL Forum. Darmstadt, 1993. - P. 205— 290.

38. Grahlmann B. Combining Finite Automata, Parallel Programs and SDL using Petri Nets //Proc. Intern. Conf. TACAC'98. — Berlin a.o.: Springer-Verlag, 1998. P. 102-117. - (Lect. Notes Comput. Sci., Vol. 1384).

39. Farwer В., Lomazova I. Systematic approach towards object-based Petri Net formalisms // Proc. 4rd Int. Conf. Perspectives of System Informatics. — Berlin a. o.: Springer-Verlag, 2001. — P. 255—267. — (Lect. Notes Comput. Sci., Vol. 2244).

40. Fleischhack H., Grahlmann B. A compositional Petri Net Semantics for SDL //Lect.Notes Comput. Sci. 1998. - Vol. 1420. P. 144-164.

41. Holzmann G. I. Design and validation of computer protocols. — Englewood Cliffs, NJ: Prentice Hall, 1991.

42. Husberg N., Manner T. Emma: Developing an Industrial Reachability Analyser for SDL // Proc. Intern. Condress on Formal Methods'99. — Berlin a.o.: Springer-Verlag, 1999. — P. 642—661. — ( Lect. Notes Comput. Sci., Vol. 1, 1708.)

43. Information Processing Systems — Open Systems Interaction — ESTELLE: A Formal Description Technique Based on an Extended State Transition Model: Inernational standard. — ISO 9074, 1989. — 1989.

44. Janowska A., Janowski P. Varification of Estelle Specification Using TLA+ // Proc. of 1st. Inter. Workshop on the Formal Description Technique Estelle. Evry, France, 1998. - P. 109-130.

45. Janowska A., Pakula M. Model cheking of Estelle specifications with SPIN //Proc. Workshop on Concurrency, Specification k, Programming. — Humbold-University Berlin, Informatik-Bericht N 140, — Vol. 1. — 2000.

46. Jensen K. Coloured Petri nets: A high level language for system design and analysis // Lect. Notes Comput. Sci. — 1991. — Vol. 483 — P. 343-416.

47. Jensen K. Coloured Petri nets: Basic concepts, analysis methods and practical use. Vol. 1. Basic concepts. — Berlin a. o.: Springer-Verlag, 1996.

48. Jensen К. Coloured Petri nets: Basic concepts, analysis methods and practical use. Vol. 2. Analysis methods. — Berlin a. o.: Springer-Verlag, 1996.

49. Jensen K. Coloured Petri nets: Basic concepts, analysis methods and practical use. Vol. 3. Practical use. — Berlin a. o.: Springer-Verlag, 1997.

50. Jirachiefpattana A., Lai R. Uncovering ISO ROSE protocol errors using Estelle // Computer Standards & Interfaces. — 1995. — N. 17. — P. 559—583.

51. Kettunen E., Montonen E., Tuuliniemi T. An interactive PrT-Net tool for verification of SDL-specifications: Technical Rep. No.3. — Helsinki University of Technology, Digital System Laboratory, 1988.

52. Kozura V.E., Nepomniaschy V. A., Novikov R.M. Verification of de-stributed systems modelled by high-level Petri nets //Proc. Int. Conf. on Parallel Computing in Electrical Engineering. — Warsaw, Poland, 2002, P. 61—66.

53. Kristensen L. M., Christensen S., Jensen K. The practitioner's guide to coloured Petri nets // Internat. J. Software Tools for Technology Transfer — 1998. Vol. 2, N 2. - P. 98-132.

54. Lai R., Jirachiefpattana A. Verifying Estelle protocol specifications using numerical Petri nets // Comput. Syst. Sci & Eng. — 1996. — Vol. 11, N 1. — P. 15-33.

55. Lai R., Tsang T. Specification and verification of multimedia synchronisation scenarios using Time-Estelle // Software Practice and Experience. — 1998. — Vol. 28, N 11. P. 1185-1211.

56. Lakos C., Lamp J. The incremental Modelling of the Z39.50 Protocol with Object Petri Nets // Lect. Notes Comput. Sci. -1999. Vol. 1605. - P. 37-68.

57. Marchena S., Leon G. Transfomation from LOTOS specs to Galileo nets // Intern. Conf. on Formal Description Techniques I. — Amsterdam: North-Holland, 1989. P. 217-230.

58. Miller R. E. Protocol verification: the first ten years, the next ten years; some personal observations // Proc. IFIP Intern. Sympos. on Protocol Specification, Testing and Verification X. — Amsterdam: North-Holland, 1990. — P. 199-225.

59. Morasca S., Pezze M., Ghezzi C., Mandrioli D. A Unified High-Level Petri Net Formalism For Time-Critical Systems. // IEEE Trans, on Softw. Eng. 1991. - Vol. 17, N 2. - P. 160-173.

60. Murphy S. L., Shankar A. U. Connection management for the transport layer: service specification and protocol verification // IEEE Transact. Com-muns. 1991. - Vol. 39, N 12. - P. 1762-1775.

61. Nepomniaschy V. A. Distributed system verification using net and program models // Proc. 15th IMACS World Congress on Scientific Computation, Modelling and Appl. Math. Berlin, 1997. - Vol. 4. - P. 373-375.

62. Pyssyalo Т., Ojala L. Modelling of a "Video on Demand" system using Pr/T-net formalism — a case study //Proc. Workshop on Concurrency, Specification k, Programming. — Humbold-University Berlin, 1994.

63. Recommendation Z.100 CCITT Specification and Description Language (SDL)

64. Richier J. L., Rodriguez C., Sifakis J., Voiron J. Verification in XESAR of the Sliding Window protocol // Proc. IFIP Intern. Sympos. on Protocol Specification, Testing and Verification VII. — Amsterdam: North-Holland, 1987. — P. 235-248.

65. Sibertin-Blanc C. A client-server protocol for the composition of Petri nets // Lect. Notes Comput. Sci. 1993. - Vol. 691. - P. 377-396.

66. Sifakis J. Perfomance evaluation of systems using nets // Lect. Notes Comput. Sci. 1980. - Vol. 84. - P. 307-319.

67. Starke P. H. A memo on time constraints in Petri nets // Humbold-University Berlin, Informatik-Bericht N 46. — 1995.

68. Stenning N. V. A data transfer protocol // Computer Networks. — 1976. — Vol. 1, N 2. P. 99-110.

69. Tan Q. M., Petrenko A., Bochmann G. V. Modelling Basic LOTOS by FSMs for Conformance Testing // Proc. IFIP 15th Intern. Symp. on Protocol Specification, Testing and Verification. — Warsaw, Poland, 1995. — P. 123—138.

70. Petrenko A., Yevtushenko N., Bochmann G. V. and Dssouli R. Testing in context: framework and test derivation.81. van der Aalst W. M. P. Interval timed coloured Petri nets and their analysis // Lect. Notes Comput. Sci. — 1993. Vol. 691. - P. 453-472.