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

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

Формальные модели, используемые в настоящий момент для спецификации распределенных систем можно классифицировать по различным признакам. Один из подходов подразделяет их на автоматные модели и модели последовательностей [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 от Международного Научного Фонда и Российского правительства. 19 943. ИНТАС 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-протокол содержит существенную неэффективность, которая часто приводит к появлению «лишних» сообщений. Показано, что добавление одного оператора позволяет существенно повысить надежность протокола, что подтверждается результатами верификации методом проверки моделей.