Моделирование и валидация коммуникационных протоколов, представленных на языках Estelle и SDL, с помощью сетей Петри высокого уровня тема диссертации и автореферата по ВАК РФ 05.13.11, кандидат физико-математических наук Чурина, Татьяна Геннадьевна

• Чурина, Татьяна Геннадьевна
• кандидат физико-математических наук
• 2000

Оглавление диссертации кандидат физико-математических наук Чурина, Татьяна Геннадьевна

Введение

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 Моделирование параллельного выполнения.

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

В последние годы анализ, валидация и верификация коммуникационных протоколов становятся все более актуальными проблемами. Несмотря на значительный прогресс в теоретических исследованиях, полученные результаты не нашли еще широкого практического применения [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.

Список литературы диссертационного исследования кандидат физико-математических наук Чурина, Татьяна Геннадьевна, 2000 год

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.