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

Российская академия наук

Сибирское отделение '

Институт систем информатики ^ г

им. А.П.Ершова ' ' ■

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

Чурина Татьяна Геннадьевна

МОДЕЛИРОВАНИЕ И ВАЛИДАЦИЯ КОММУНИКАЦИОННЫХ ПРОТОКОЛОВ, ПРЕДСТАВЛЕННЫХ НА ЯЗЫКАХ ESTELLE И SDL, С ПОМОЩЬЮ СЕТЕЙ ПЕТРИ ВЫСОКОГО УРОВНЯ

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

Автореферат

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

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

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

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

доктор технических наук Бандман О.Л.

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

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

Защита достоится 15 декабря 2000 года в 14 час. 30 мин. на заседании диссертационного совета К0003.93.01 в Институте систем информатики Сибирского отделения РАН по адресу:

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

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

Автореферат,разо^ан,"14".ноября 2000 г.

Ученый секретарь специализированного совета К0003.93.01 к.ф.-м.н.

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

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

^¡ЬьНб, о

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

~ Актуальность. В последние годы анализ, валидация и верификация коммуникационных протоколов становятся все более актуальными проблемами. На практике используются два основных подхода к проблеме верификации коммуникационных протоколов. Первый состоит в применении так называемых техник формального описания (FDT), к которым относятся, главным образом, языки выполнимых спецификаций Estelle, являющиеся стандартами ISO, а также SDL, принятый в качество стандарта ITU. Преимущество языков Estelle и SDL в их выразительной силе, однако именно оно затрудняет анализ и верификацию протоколов' связи, способы анализа выполнимых спецификаций остаются предметом исследования. Второй подход базируется на использовании таких моделей, как конечные автоматы, сети Петри и их обобщения, и состоит в моделировании коммуникационных протоколов и верификации полученных моделей. Хотя, по сравнению с FDT, модели более удобны для анализа и верификации, однако при использовании данного подхода моделирование распределенных систем, как правило, выполняется отдельно для каждого примера, что приводит к необходимости верификации процесса моделирования, а это, в свою очередь, является сложной проблемой для реальных распределенных систем.

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

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

ритетов. Однако для адекватного представления' протоколов важно рассматривать Estelle-спецификации с задержками и приоритетами. Кроме того, реализация данного метода не описана, а упомянута в качестве темы исследования. -

По сравнению с Estelle язык SDL вызывает большой интерес и широко применяется на практике. Опубликован ряд работ по трансляции SDL-спецификаций в различные сетевые модели. Развитие методов трансляции SDL-спецификаций осуществлялось по двум направлениям. При нервом используются сети Петри высокого уровня, такие как PrT(predicate-transition)-cera (работы Е.Кеттунена и Н.Хусберга) и М-сети (работы Б.Гралмана). Моделирование с использованием РгТ-сетей не является полным моделированием всей спецификации, а оно осуществляется только для верхних уровней спецификации, в которых отражаются поток управления и связи между объектами спецификации.

При втором направлении (работы И.Фишера и Ф.Баузе) используются новые классы сетей Петри высокого уровня — SDL-сети, ориентированные на язык. Однако их применение требует разработки специальных методов анализа, неизбежно трудоемких в силу сложности сетей. Как в работах И.Фишера, так и в работах Ф.Баузе описаны сетевые модели, в которых каждому экземпляру процесса соответствует подсеть, и предложены методы построения графа достижимости. В последней работе представлена техника анализа эффективности SDL-сетей, но для применения этих методов требуются дальнейшие исследования, поскольку графы достижимости весьма громоздки и обычные способы их обработки неэффективны.

В России также велись исследования по верификации коммуникационных протоколов. Отметим в частности, работы О.Л.Бандман — по спецификации поведения сетевых протоколов, Н.А.Анисимова — но ручному моделированию с использованием сетей Петри, А.Петренко, Н.В.Евтушенко, Ю.Г.Карпова — по тестированию коммуникационных протоколов с помощью конечно-автоматных моделей, а В.А.Соколова — с помощью сетей Петри.

Среди различных сетей Петри высокого уровня можно выделить раскрашенные сети Петри (РСП), принятые в качестве международного стандарта. Для них разработаны и реализованы практические методы анализа. Кроме того, существует доступная система D.esign/CPN, активно используемая в практических исследованиях. В книге Иенсе-на поставлена проблема автоматического построения сетевых моделей

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

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

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

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

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

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

—.Разработаны способ моделирования SDL-спецификаций с динамическими конструкциями и алгоритмы перевода динам!^ских конструкций в раскрашенные сети Петри. При моделировании SDL-спецификаций с динамическими конструкциями ИВТ-сетей недостаточно, поскольку экземпляры процессов мы отображаем фишками, а существование нескольких экземпляров одного процесса предполагает наличие в местах нескольких фишек. Поэтому моделирование SDL-спецификаций

осуществляется посредством раскрашенных сетей Петри. Полученные сетевые модели можно исследовать в системе Design/CPN. Впервые проведено моделирование, охватывающее практически полный язык SDL88, посредством раскрашенных сетей Петри, что позволяет решить проблему, поставленную Иенсеном.

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

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

3rd International Conference on Parallel Computing Technologies, St.Petersburg, Russia, 1995. (Lect. Notes Coraput. Sei., Vol. 964).

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.

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.

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

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

Структура работы. Диссертация состоит из введения, трех глав, заключения, списка литературы из 67 наименований и приложения. Основное содержание составляет 125 страниц, объем приложения 15 страниц. Работа включает 43 иллюстрации и 2 таблицы.

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

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

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

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

Некоторые термины, такие как модуль и переход, используются и в языке Estelle, и в сетях, поэтому будем использовать приставки Е- и N-для обозначения объектов Estelle и сети соответственно.

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

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

При построении сети, моделирующей тело модуля, каждому Е-пе-реходу сопоставляется один N-модуль, а переменной — одно место. На странице также создается место State, тип которого определяется множеством локальных состояний Е-модуля. Место Stute является входным и выходным для каждого N-модуля и обеспечивает выполнение только одного Е-нерехода. Если Е-нереход использует какой-нибудь ресурс (переменную, параметр или точку взаимодействия), то место, соответствующее этому ресурсу, соединяется с N-модулем, представляющим Е-переход. Действие Е-перехода представляется сетью, которая располагается на под странице, связанной с N-модулем, сопоставленным Е-переходу. Блок перехода разбивается па последовательность подблоков. Каждому подблоку сопоставляется фрагмент сети..Фрагменты соединяются друг с другом с помощью служебных мест в том же порядке, что и подблоки. Подблок, являющийся последовательностью операторов присваивания, и, возможно, операторов посылки сообщений, представляется в сети одним N-переходом, причем, ни один из операторов присваивания не использует переменной, ранее измененной н этом же подблоке. При этом операторы, образующие подблок, преобразуются в выражения на датах. Оператор вызова процедуры или функции в сети Е-перехода представляется N-модулем. Сеть, моделирующая соответствующую процедуру или функцию, размещается на странице, связанной с этим N-модулем. При моделировании условных операторов и циклов используются библиотечные фрагменты. Цепочку фрагментов, представляющих блок Е-перехода, ограничивают два служебных перехода — start и end. Место State является входным для перехода start и выходным для перехода end, обеспечивая тем самым атомарность вы-

полпенни Е-перехода. Фрагмент сети, соответствующий задержке перехода, помещается между фрагментом, моделирующим условие возможности этого перехода, и переходом stört, так как отсчет задержки происходит, когда условие возможности Е-псрехода проверено и выполняется. Время задержки Е-перехода отсчитывается специальным переходом с интервалом срабатывания, указанным в задержке; все прочие N-переходы имеют интервал срабатывания [0,0].

В разделе 1.4 рассматривается алгоритм генерации сетевых моделей для иерархических спецификаций. Для спецификации строится сеть, иерархия страниц которой повторяет общую иерархию системы. Первая страница представляет уровень системных модулей. Если какой-нибудь Е-модуль имеет наследников, то подстраница, связанная с соответствующим ему N-модулем, содержит по одному N-модулю для каждого экземпляра модуля-наследника. Затем для каждого из полученных N-модулей строится дерево страниц, повторяющее иерархию подсистемы с корнем в соответствующем системном Е-модуле. Трансляция модулей осуществляется по одной схеме, которая не зависит от положения модуля в иерархии Estelle-спецификации. Для каждой подсистемы создается дополнительная конструкция, которая связывает все модули в подсистеме и реализует правило выбора Е-перехода для выполнения на следующем такте. Родительский модуль управляет вычислениями наследников с помощью контрольных мест. Все модули-наследники класса activity делят одно контрольное место, что делает возможным выполнение перехода только одного из Е-модулей. Каждый модуль-наследник класса process имеет собственное контрольное место. Фишки появляются во всех местах одновременно, что соответствует параллельному выполнению.

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

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

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

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

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

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

чия в отображении точки присоединения маршрутов к каналу. Сигнал, поступающий к блоку по входному каналу, может передаваться по нескольким подсоединенным к нему маршрутам. Для оптимизации сети предложенный алгоритм поддерживает три способа распределения сигналов, а именно: передачу сигнала из входного канала только в один присоединенный маршрут; в каждый присоединенный маршрут, по которому этот сигнал может передаваться; всем экземплярам процессов, которые связаны с этим каналом.

При построении сети для экземпляра процесса множество состояний процесса, все сорта, определения сигналов и списков сигналов, описанные в декларативной части процесса, преобразуются в множества цветов. Порт экземпляра процесса представляется местом queue, которое соединяется с копиями мост, соответствующих входным маршрутам процесса, посредством служебных переходов link. Множество состояний процесса определяет множество цветов служебного места State, роль этого места точно такая же, что и в ИВТ-сетях. Кроме того, в сети, представляющей экземпляр процесса, создается служебный переход delete, моделирующий удаление первого сигнала из порта экземпляра процесса в том случае, если экземпляр, находясь в определенном состоянии, не воспринимает этот сигнал.

Если SDL-спецификация содержит процессы, использующие таймер-ные конструкции, то па первой странице сети создается место now, которое содержит одну фишку целого значения, несущую временной штамп, а также переход add, имеющий временную пометку @+ 1. Место now • входное и выходное для этого перехода. В процессе функционирования моделирующей сети временной штамп фишки в месте now определяет текущий момент в системе. Сеть, представляющая SDL-переход с оператором установки таймера, содержит копию места now и место, моделирующее таймер. Текущее время в модели но изменяется до тех пор, пока остаются переходы, имеющие возможность сработать. Изменение значения глобальных часов происходит тогда, когда в сети остаются только переходы, которым не позволяют сработать временные штампы фишек. Для того чтобы переход add имел равные возможности по отношению к другим переходам, на каждой входной к месту State дуге устанавливается временная пометка из некоторого интервала, который определяется исходя из предположений о длительности выполнения перехода в системе. В данном разделе подробно описаны фрагменты сети, моделирующие такие конструкции, как установка и сброс таймера, средство

сохранения сигнала SAVE и сеть для перехода с разрешающим условием, функционирование которых нарушает дисциплину FIFO-очереди и вызывает трудности в сетевом моделировании.

Раздел 2.4 является логическим продолжением предыдущего и предлагает способ перевода в раскрашенные сети спецификаций с динамическими конструкциями. Здесь описаны основные моменты, которые возникают при моделировании создания и уничтожения-экземпляров процессов во время функционирования системы. Моделирование основано на том, что многоуровневое описание системы в SDL имеет статический шаблон. Число экземпляров процесса может измениться в процессе функционирования системы, но позиция каждого экземпляра в общей иерархии системы остается неизменной. Статический шаблон моделируется структурой сети, а экземпляры процессов — фишками. Структура результирующей сети в целом аналогична той, что описана в разделе 2.3. Основное отличие состоит в том, что в сети N-модуль сопоставляется не экземпляру процесса, а его описанию, а фишки, принадлежащие конкретному экземпляру процесса, помещаются в места сети при создании экземпляра процесса и удаляются, когда он входит в состояние STOP. Поскольку фишки, принадлежащие экземплярам одного и того же процесса, располагаются в одних и тех же местах, возникает необходимость в их дополнительной идентификации. Для этого фишки снабжаются уникальным признаком — ПИ Д. Для генерации ПИД используется специальное место PId, которое располагается на самой верхней странице сети и содержит одну фишку из множества цветов integer, значение которой определяет личный идентификатор экземпляра процесса при его создании во время функционирования сети. Копия места PId присутствует на каждой странице, где происходит моделирование порождения нового экземпляра процесса, и является входным и выходным местом для N-переходов, осуществляющих это моделирование.

Особенности моделирования порождения одного экземпляра процесса другим отражаются в сети в том, что для N-модуля, соответствующего порождаемому процессу, создается дополнительное служебное место cr_id (где id имя порождаемого процесса). Оно является для этого N-модуля входным и выходным для N-модуля, представляющего родителя. При срабатывании N-перехода, моделирующего запрос на создание экземпляра процесса, в служебное место cr_id добавится элемент, значение первого поля которого есть ПИД создаваемого экземпляра!,

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

, Раздел 2.5 содержит описание результирующей сетевой модели и оценки ее размера. Если в спецификации не содержится процедур, то оценка становится линейной. При отображении спецификаций с динамическими конструкциями создается сетевая модель, в которой в каждом месте содержится не более одной фишки, моделирующей конкретный экземпляр процесса. Это факт позволяет повысить эффективность моделирования, так как существенно уменьшает перебор вариантов связывания переменных при срабатывании переходов. Следует отметить, что формальной семантики языка SDL не существует. Обычно системы, моделирующие SDL, определяют семантику используемых конструкций и вносят определенные ограничения. Поэтому, можно считать, что предложенный алгоритм задает сетевую семантику языка SDL88.

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

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

В разделе 3.2 описана реализация алгоритмов перевода в сетевые модели. На первом проходе трансляции строится внутреннее представление программы в виде атрибутированного дерева разбора, а иа втором — как для Estelle-, так и для SDL-спецификаций — генерируется внутреннее представление ИВТ-сети в системе ESPV. Процесс построения сетей производится по уровням, соответствующим этапам в описании алгоритмов трансляции, представленных в гл. 1 и 2. Все уровни сети, кроме нижних, используют модули системы ESPV. На завершающем шаге — оптимизации сети — удаляются все пустые переходы, т>. е. имеющие пустые тела и не имеющие выражений на выходных дугах, и сливаются в один два последовательно выполняющихся перехода, обладающие определенным набором свойств. После создания внутреннего представления сети осуществляется размещение ее элементов на плоскости, т. е. каждому элементу приписываются координаты на соответствующих страницах системы ESPV. При этом фрагменты сети, реализующие стандартные конструкции, размещаются типовым образом. При трансляции SDL-спецификаций сеть переводится в текстовое представление системы Design/CPN, которая не предоставляет средств для автоматического построения сети, но имеет возможность загружать сетевые диаграммы в текстовом представлении ("interchange"формате), базирующемся на языке SGML (Standard Generalized Markup Language).

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

В разделе 3.4 описаны эксперименты с протоколами скользящего окна, такими как протокол Стеннинга и г-протокол, представленными на языке Estelle, а также с протоколом Inres, представленным на SDL. Протоколы скользящего окна состоят из двух компонентов: передатчика и приемника, взаимодействующих между собой через ненадежную среду,' в которой возможны потеря, дублирование и переупорядочение сообщений. Протокол должен обеспечить передачу сообщений от пользователя-передатчика пользователю-приемнику, причем к последнему они должны поступить в том же самом порядке, в каком были отправлены пользователем-передатчиком. Протокол Стеннинга в качестве сообщений отправляет номера последовательности по модулю N и помещает номер-сообщение в буфер, называемый окном передатчика. Во время эксперимента с протоколом с помощью пошаговой симуляции была воспроизведена специфическая последовательность событий, которую описал Каивола и которая приводит к рассогласованию между перепосылкой сообщений передатчиком и отправлением подтвержден ний приемником. В итоге на уровне протокола наблюдается непрерывная активность, тогда как на уровне пользователя всякая деятельность останавливается: со стороны передатчика новые сообщения не генерируются и со стороны приемника передачи новых сообщений на верхний уровень не происходит.

¿-протокол является частью пакета GNU UUPC от Free Software Fondation и используется для передачи данных по линиям связи. По своей сути г-протокол — вариант протокола скользящего окна, отличительная особенность ¿-протокола — минимизация числа перепосылок по сравнению с другими вариантами протокола скользящего окна. Основой для написания Estelle-спецификации ¿-протокола послужила спецификация на языке Promela. В ходе эксперимента в среде ¿-протокола была воспроизведена последовательность событий, приводящая к ошибке Каи-волы в протоколе Стеннинга. Было выяснено, что несмотря на то, что любое подтверждение воспринимается передатчиком корректно (в отличие от протокола Стеннинга), воспроизведение этой последовательности событий приводит к ситуации live — lock в ¿-протоколе. Более того, на основании проделанных экспериментов можно утверждать, что такая ситуация возникает в ¿-протоколе в результате любой последовательности событий, приводящей к состоянию, когда окна передачи полностью заполнены и ни одно подтверждение не получено.

Протокол Inres описывает взаимодействия между двумя протоколь-

пыми объектами. Связь между ними происходит через ненадежную сроду передачи, которая может терять сообщения, по не может их копировать или переупорядочивать. Каждый сеанс связи между протокольными объектами разбит на две фазы: фазу установления связи и фазу передачи данных. При написании системы Inres для организации моделирования действий пользователя дополнительно были реализованы процессы-пользователи. Кроме того, система была расширена для работы с многими пользователями. Для этой цели был реализован процесс, который во время функционирования по истечении установленного в таймере времени, создает экземпляры процессов пользователей и протокольных объектов. Эксперимент с протоколом Inres проводился в системе Design/CPN. Во время эксперимента была обнаружена семантическая ошибка, состоящая в дублировании данных, передаваемых между протокольными объектами. Такая ситуация возникает в том случае, если установленного в таймере времени в передающем протокольном «объекте недостаточно для того, чтобы протокольные объекты успели обменяться сообщениями. При предположениях о времени, необходимом объекта.м для обмена данных, в протоколе были изменены временные характеристики, в результате чего поведение сети стало соответствовать ожидаемому.

В приложении приведены Promela- и Estelle-спецификации ¿-протокола.

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

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

— Разработан алгоритм перевода Estelle-спецификаций без динамических конструкций, но с задержками и приоритетами в ИВТ-сети.

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

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

— Реализованы разработанные алгоритмы перевода Estelle- и SDL-спецификаций в соответствующие сетевые модели и проведены экспери-

менты по поиску семантических ошибок для таких коммуникационных протоколов, как протокол Стеннинга, ¿-протокол, Inres. В ходе экспериментов были обнаружены новые эффекты поведения протоколов.

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

\

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

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

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

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

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

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

7. Churina T.G., Okunishnikova E.V. Modelling Estelle specifications using Coloured Petri nets.// Joint Bulletin of the Novosibirsk Coinput-ng Center and the Institute of Informatics Systems. Ser! Computer Science. - 1998. — N 8. — P. 19-39.

8. Nepomniasciiy V.A., Alekseev G.I., Bystrov A.V., Сни-una T.G., Mylnikov S.P.,Okunishnikova E.V. Towards Verification >f Estelle-specified Communication Protocols: Coloured Petri Net Approach '/Proc. Int. Conf. on Parallel Computing in Electrical Engineering. — Bia-ystok, Poland, 1998, P. 141-147.

9. Nepomniaschy V.A., Alekseev G.I., Bystrov A.V. , Сни-rina TX3., Mylnikov S.P., Okunisiinikova E.V. EPV - Petri Net Based Estelle Protocol Verifier //Proc. 1st Internati. Workshop on the Fbr-mal Description Technique Estelle. — Evry, France, 1998. — P. 101-108.

10. 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.

11. Nepomniaschy V. A., Alekseev G. I., Bystrov A. V., Churina T. G., Mylnikov S. P., Okunisiinikova 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).

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

• РАН, Новосибирск, 1995. - С. 95-123.

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

14. Alekseev G. I., Bystrov A. V., Churina T. G., Mylnikov S. P. Petri-net based environment for the specification, analysis and simulation of concurrent systems // Specification, verification and net models of concurrent systems. — IIS, Novosibirsk, 1994. - P. 116-127.

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

Все результаты, касающиеся моделирования и валидации SDL-cne-цификаций, получены автором самостоятельно. В работах по моделированию Estelle-спецификаций, выполненных в соавторстве, Т. Г. Чурина внесла следующий вклад: в работах [7 — 14] разработано отображение в ИВТ-сети структур данных, условий'возможности Е-перехода, входных переходов, сложных переходов, а также ряда стандартных конструкций языка Estelle; разработаны основные принципы и алгоритм моделирования иерархической спецификации и шага выполнения^в работах [2,4,6] разработаны и описаны реализация алгоритма генерации сете-' вой модели по внутреннему представлению Estelle-спецификации, оптимизация сетевой модели и эксперименты с протоколом Стеннинга и ¿-протоколом. П

"//-'''т

Введение

1 Глава I

Моделирование Estelle-спецификаций без динамических конструкций посредством ИВТ-сетей

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

1.2 Сетевая модель.

1.3 Моделирование одноуровневых Estelle-спецификаций.

1.3.1 Моделирование структуры спецификации.

1.3.2 Моделирование тела модуля.

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

1.4 Моделирование иерархических Estelle-спецификаций.

1.4.1 Моделирование последовательного выполнения.

1.4.2 Моделирование параллельного выполнения.

В последние годы анализ, валидация и верификация коммуникационных протоколов становятся все более актуальными проблемами. Несмотря на значительный прогресс в теоретических исследованиях, полученные результаты не нашли еще широкого практического применения [37, 38, 54]. На практике используются два основных подхода к проблеме верификации коммуникационных протоколов. Первый состоит в применении так называемых техник формального описания (FDT), к которым относятся, главным образом, языки выполнимых спецификаций Estelle [4, 25, 39] и LOTOS [15, 52], являющиеся стандартами ISO, а также SDL [5, 61], принятый в качестве стандарта ITU. Преимущество языков Estelle и SDL — в их выразительной силе, что особенно проявляется при представлении коммуникационных протоколов [32, 63, 64, 31], однако это преимущество затрудняет их анализ и верификацию, поэтому способы анализа выполнимых спецификаций остаются предметом исследования. Полезные средства анализа и верификации Estelle-спецификаций описаны в работах Б.Алгареса [17], С.Будковского [24] и Д.П.Куртиа [29], а SDL-спецификаций — в работах Х.Туминена [67], Г.И.Холцмана [53] и Б.Алгареса [18].

Второй подход базируется на использовании таких моделей, как конечные автоматы (Р.Коэн и А.Сегал [28], Г.И.Холцман [37]), сети Петри (Н.А.Анисимов [19]) и их обобщения (Р.Лай [50]), и состоит в моделировании коммуникационных протоколов и верификации полученных моделей. Хотя, по сравнению с FDT, модели более удобны для анализа и верификации, однако при использовании данного подхода моделирование распределенных систем, как правило, выполняется отдельно для каждого примера, что приводит к необходимости верификации процесса моделирования, а это, в свою очередь, является сложной проблемой для реальных распределенных систем.

В России также велись исследования по верификации коммуникационных протоколов. Отметим в частности, работы О.Л.Бандман [1,3] — по спецификации поведения сетевых протоколов, Н.А.Анисимова [19, 20] — по ручному моделированию с использованием сетей Петри, А.Петренко [65], Н.В.Евтушенко [66], Ю.Г.Карпова [47] — по тестированию коммуникационных протоколов с помощью конечно-автоматных моделей, а В.А.Соколова и А.И.Легалова [11] — с помощью сетей Петри.

Автоматический перевод FDT-спецификаций в формальные модели, для которых существуют эффективные методы анализа и автоматические средства верификации, объединяет преимущества обоих подходов. Известны примеры трансляции FDT-спецификаций в конечно-автоматные модели (Ж.Л.Ричье, И.Сифакис и др. [62]), сети Петри (В.Димитров [30]), алгебры процессов (А.Гам-мелгард и Ж.Е.Кристенсен [34]) и темпоральные логики действий (А. Яновский, П. Яновский [41]).

Для Estelle-спецификаций в работе Ж.Л.Ричье, И.Сифакиса и др. [62] предложен метод автоматического построения конечно-автоматных моделей посредством исчерпывающей симуляции, позволяющий верифицировать некоторые свойства коммуникационных протоколов. В работах В.Димитрова [301 и Р.Лая [50] представлены методы трансляции Estelle-спецификаций в сети Петри, причем используются как ординарные [30], так и сети Петри высокого уровня (так называемые нумерические) [50]. При этом если в [30] рассматривается ограниченное подмножество Estelle-спецификаций, то в [50] — широкое подмножество, включающее динамические конструкции, но без задержек и приоритетов. Однако для адекватного представления протоколов важно рассматривать Estelle-спецификации с задержками и приоритетами. Кроме того, реализация данного метода не описана, а упомянута в [50] в качестве темы исследования. В работе Р.Лая и Т.Цанга [51] предложен метод трансляции Estelle-спецификаций с обобщенными временными конструкциями в модульные сети Петри (Communicating Time Petri Nets). Несмотря на определенное продвижение, разработка методов анализа таких сетей Петри является трудной проблемой (Г.Буччи и Е.Викарио [23]).

По сравнению с Estelle язык SDL вызывает большой интерес и широко применяется на практике. Опубликован ряд работ по трансляции SDL-специфика-ций в различные сетевые модели. Развитие методов трансляции SDL-специфи-каций осуществлялось по двум направлениям. При первом используются сети Петри высокого уровня, такие как PrT(predicate-transition)-ceTH [38, 48] и М-сети [35, 36]. Моделирование с использованием PrT-сетей в работах Кеттунена [48] и Н. Хусберга [38] не является полным моделированием всей спецификации, а осуществляется лишь для верхних уровней спецификации, в которых отражаются поток управления и связи между объектами спецификации. В работах Б.Гралмана. [35] и Н.Хусберга [38] SDL-спецификации с динамическими конструкциями транслируются в сетевые модели, в которых экземпляры процессов отображаются фишками. В работе [35] также представлена интегрированная система PEP (Programming Environment based on Petri Nets), поддерживающая моделирование и верификацию сетевых моделей. В работе [38] описана трансляция с диалекта языка SDL88 — TNSDL, а для верификации используется анализатор графа достижимости.

При втором направлении используются новые классы сетей Петри высокого уровня — SDL-сети, ориентированные на язык [33, 21]. Однако их применение требует разработки специальных методов анализа, неизбежно трудоемких в силу сложности сетей. Как в работе И.Фишера [33], так и в работе Ф.Баузе [21] описаны сетевые модели, в которых каждому экземпляру процесса соответствует подсеть, и предложены методы построения графа достижимости. В работе [21] представлена техника анализа эффективности для SDL-сетей, но для применения этих методов требуются дальнейшие исследования, поскольку графы достижимости весьма громоздки и обычные способы их обработки неэффективны.

Среди различных сетей Петри высокого уровня можно выделить раскрашенные сети Петри (РСП) [42], принятые в качестве международного стандарта, для которых разработаны и реализованы практические методы анализа [43, 44]. Кроме того, существует доступная система Design/CPN [44, 49], активно используемая в практических исследованиях. В книге Иенсена [44] поставлена проблема автоматического построения сетевых моделей SDL-спецификаций, развития средств их верификации, а также проведения экспериментов по обнаружению семантических ошибок распределенных систем с помощью этих средств. Значительный интерес представляет аналогичная проблема и для Estelle-специфи-каций.

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

Наш подход состоит в автоматическом переводе Estelle-спецификаций без динамических конструкций в эффективную сетевую модель (называемую ИВТ-сетыо), а SDL-спецификаций с динамическими конструкциями — в РСП. ИВТ-сети — иерархические временные типизированные сети — вариант раскрашенных сетей. В ИВТ-сетях используется предложенная Мерлином [22] концепция времени, близкая к семантике языка Estelle. ИВТ-сети квазибезопасны, т. е. в них все места, за исключением мест-очередей, могут содержать не более одной фишки. При моделировании SDL-спецификаций с динамическими конструкциями ИВТ-сетей недостаточно, так как экземпляры процессов мы отображаем фишками, а существование нескольких экземпляров одного процесса предполагает наличие в местах нескольких фишек. Поэтому моделирование SDL-спецификаций осуществляется посредством раскрашенных сетей Петри. Полученные сетевые модели можно исследовать в системе Design/CPN, ориентированной на их симуляцию и анализ. Следует отметить, что мы моделируем спецификации, представленные на языке SDL88. Трансляция спецификаций, представленных на языке SDL92, может решаться с использованием их автоматической трансляция в SDL88, предложенной в работе Й.Фишера и Е.Димитрова [33].

Вышеописанный подход к верификации распределенных систем начал разрабатываться с 1994 г., когда была проведена реализация первой версии системы Net.Cale [16], а также построены и изучены сетевые модели некоторых протоколов, представленных на языках Estelle и SDL. В 1995 г. разработан метод трансляции Estelle-спецификаций без задержек и приоритетов в раскрашенные сети Петри [9, 57], а также описан наш подход к верификации этих спецификаций, включающий "ручное"применение метода трансляции и использующий систему NetCalc для обнаружения семантических ошибок [56]. В 1997 г. этот метод трансляции расширен на Estelle-спецификации с задержками и приоритетами [26, 58], проведена его реализация, разработана и реализована улучшенная версия системы NetCalc, названная ESPV (Estelle SDL Protocol Verifier), а также проведены эксперименты по отладке реализации алгоритма. В 1998 г. было предложено моделирование для многоуровневых Estelle-спецификаций с задержками и приоритетами [27], описаны результаты экспериментов [7, 59] по сетевому моделированию и поиску ошибок для версий четырех известных протоколов: со скользящим окном [62, 63], кольцевого [28], соединений [55], Inres[31], В работе [60] предложена методика валидации сетевых моделей системы ESPV. Моделирование '¿-протокола описано в работе [8], а моделирование Estelle-спецификаций с динамическими конструкциями — в [10]. Паралелльно в 1997 г. начались работы по моделированию SDL-спецификаций. В 1998 г. описало построение сетевой модели для SDL-спецификаций без динамических конструкций [12]. В 1999 г. предложено моделирование динамических конструкций языка SDL [13], а в 2000 г. осуществлена генерация текстового формата сетевой модели [14], который является входным в системе Design/CPN. Следует отметить, что работы [12, 13, 14] развивались независимо от работ Б.Гралмаиа [35]и Н.Хусберга [38].

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

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

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

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

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

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

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

Реализация результатов работы. Предложенные алгоритмы перевода и методы исследования используются в системе ESPV. Материалы диссертации использовались в учебном процессе на кафедре систем информатики Новосибирского государственного университета.

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

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

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

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

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

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

1. 3rd International Conference on Parallel Computing Technologies. St.Petersburg, Russia, 1995. (Lect. Notes Comput. Sci., Vol. 964).

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.

Кроме того, полученные результаты обсуждались на семинарах лаборатории теоретического программирования ИСИ СО РАН и кафедры систем информатики НГУ.

Публикации. По теме диссертации опубликовано 14 научных работ. Из них 7 работ [8, 14, 26, 56, 57, 59, 60] — на международных конференциях, 1 работа [2] — в центральном издании и 6 работ [7, 12, 13, 9, 16, 27] — в местных изданиях.

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

3.5 Основные выводы по главе

В данной главе представлена разработанная в лаборатории теоретического программирования ПСИ СОРАН и предназначенная для проектирования и симуляции ИВТ-сетей экспериментальная система ESPV. Описаны реализация алгоритмов, генерирующих сетевые модели по Estelle- и SDL-спецификациям, методика валидации сетевых моделей в системе ESPV и эксперименты, проведенные с протоколами Стеннинга и ¿-протоколом в этой системе, а с протоколом Inres в системе Design/CPN.

В ходе экспериментов обнаружены новые эффекты поведения протоколов. Воспроизведение последовательности событий, приводящей к ошибке Каиволы в протоколе Стеннинга, приводит к ситуации Uve — lock в ¿-протоколе. Во время эксперимента с протоколом Inres была обнаружена неэффективность, состоящая в дублировании данных, передаваемых между пртокольными объектами. Эксперименты, проведенные с протоколами, подтверждают эффективность полученных сетевых моделей, а оценки их размеров приемлемы для реальных протоколов.

Заключение

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

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

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

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

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

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

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

Успешные эксперименты по обнаружению семантических ошибок в версиях трех протоколов продемонстрировали эффективность нашего подхода. Отметим, что во всех этих примерах размер результирующих сетей значительно меньше теоретических верхних оценок. Среди всех протоколов наиболее интересным является ¿-протокол, который реально используется на практике. В диссертации для этого протокола впервые показано родство типичной ошибки Каиволы, обнаруженной в протоколе скользящего окна, и live — lochia, в ¿-протоколе. В диссертации также впервые проанализирована семантическая ошибка для протокола Inres. В случае использования его спецификации с динамическими конструкциями ошибка была обнаружена методом автоматической симуляции в системе Design/CPN.

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

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

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

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

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

6. Непомнящий В.А., Алексеев Г.И., Быстрое A.B., Куртов С.А., Мыльников С.П. , Окунишникова Е.В., Чубарев П.А., Чурина Т.Г.

7. Верификация Estelle-спецификаций распределенных систем посредством раскрашенных сетей Петри. — Новосибирск, 1998. — 140 с.

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

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

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

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

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

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

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

15. 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.

16. 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.

17. 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.

18. 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.

19. 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.

20. Berthomieu B., 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.

21. 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.

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

23. 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.

24. 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.

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

26. 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.

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

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

29. Internet: http: //www. ipipan. waw.pl/~piotrd/estellespec/abraprot. stl.

30. 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.

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

32. 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).

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

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

35. 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.)

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

37. Information processing systems — Open System Interconnection — basic reference model. IS 7498, 1984.

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

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

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

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

42. Johnson S. YACC: Yet Another Compiler-Compiler: Technical Rep. No.32. — Murray Hill, N.J., Bell Laboratories, 1978.

43. Kaivola R. Using Compositional preorders in the Verification of Sliding Window Protocol // Lect. Notes Comput. Sci. 1997. - Vol. 1254. - P. 48-59.

44. 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.

45. 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.

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

47. 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.

48. 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.

49. Holzmann G.J The model checker SPIN //IEEE Transact.Software Engineering. 1997. - Vol.23, N 5,- P. 295.

50. 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.

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

52. 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.

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

54. 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.

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

56. Yifei Dong et al. Fighting livelock in the i-protocol: A comparative study of verification tools// Internet: http://www.cs.sunysb.edu/~lmc/iproto/.

57. 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.

58. Petrenko A., Yevtushenko N., Bochmann G.v. and Dssouli R. Testing in context: framework and test derivation.

59. Tuominen H. Embedding a Dialect of SDL in PROMELA //Lect. Notes Comput. Sci. 1999. - Issue 1680. - P. 245-260.