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

• Автор: Чурина, Татьяна Геннадьевна
• Шифр специальности: 05.13.11
• Научная степень: Кандидатская
• Год защиты: 2000
• Место защиты: Новосибирск
• Количество страниц: 141 с. : ил.

Содержание
Введение
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 Моделирование параллельного выполнения
1.5 Основные выводы по главе и оценка размера сети
2 Глава II
Моделирование SDL-спецификаций с динамическими конструкциями посредством раскрашенных сетей Петри
2.1 Обзор языка SDL
2.2 Раскрашенные сети Петри с временными конструкциями
2.3 Моделирование SDL-спецификаций без динамических конструкций
2.3.1 Моделирование структуры системы
2.3.2 Моделирование блока
2.3.3 Моделирование процессов
2.3.4 Моделирование перехода
2.3.5 Моделирование конструкций, нарушающих принцип FIFO-
очереди
2.4 Моделирование динамических конструкций языка SDL
2.4.1 Моделирование структуры системы и блока
2.4.2 Моделирование процессов и переходов
2.4.3 Моделирование порождения и уничтожения экземпляров
процессов
2.5 Основные выводы по главе и оценка размера сети
3 Глава III
Генерация и валидация сетевых моделей
3.1 Общая структура системы ESPV

3.2 Генерация сетевых моделей в системе ЕЭРУ
3.3 Методология валидации сетевых моделей коммуникационных протоколов
3.4 Эксперименты с коммуникационными протоколами
3.4.1 Протокол Стеннинга
3.4.2 г-протокол
3.4.3 Протокол 1пгез
3.5 Основные выводы по главе
Заключение
Литература
Приложение

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

1.4.2 Моделирование параллельного выполнения
Опишем моделирование параллельного выполнения. Если модуль описан как system— process/process, то множество переходов, которые будут выполняться на следующем такте выполнения, либо состоит из одного из готовых переходов данного модуля, либо включает по одному переходу из каждого модуля-паследника данного модуля. Все выбранные переходы выполняются в одном такте.
Для моделирования такта выполнения, аналогично предыдущему случаю, на странице, соответствующей системному модулю, создаются служебные место step и переходы pass и next_step. Кроме того, на этой странице создается столько дополнительных мест serv и out, сколько модулей-наследников класса process имеется в системном модуле. На каждой странице, представляющей тело некоторого модуля класса process, создается переход pass, два служебных места serv и out. На каждой странице, представляющей тело охватывающего модуля создается переход next,_step. На рис. 1.11 отображена иерархия страниц для спецификации В, являющейся системным модулем класса systemprocess. Этот модуль содержит модули С и D класса process. В свою очередь в описании С содержится модуль Cl, а в D — модуль D1.
Если модуль класса process имеет наследников класса activity, то для них используется схема дополнительного построения, описанная в п. 1.4.1.
Как и в предыдущем случае, место serv является входным, а место out — выходным для подсетей модулей-наследников. Отличие состоит в том, что каждый модуль-наследник имеет свое входное место serv и выходное место out. Срабатывание перехода pass передает право выбора перехода для выполнения на следующий уровень либо помещает фишку в место out, если модуль не имеет наследников. Фишка в месте out какого-нибудь модуля может появиться также в результате выполнения некоторого Е-перехода из данного модуля. Как только во всех выходных служебных местах подсетей, моделирующих наследников и имеющих одного родителя, будут фишки, может сработать служебный переход next_step. При его срабатывании фишки из этих выходных мест изымаются и появляется фишка в месте step, если родитель — системный модуль. Если родитель не системный модуль, то фишка появится в выходном служебном месте подсети, моделирующей родителя. Следующий вычислительный такт станет возможным, когда фишка появится в месте .step.
Итак, при параллельном выполнении также как и при последовательном, родительский модуль управляет вычислениями наследников с помощью контрольных мест. При этом каждый модуль-наследник класса process имеет собственное контрольное место. Фишки появляются во всех местах одновременно,