научная статья по теме МОДЕЛИРОВАНИЕ И ВЕРИФИКАЦИЯ КОММУНИКАЦИОННЫХ ПРОТОКОЛОВ, ПРЕДСТАВЛЕННЫХ НА ЯЗЫКЕ SDL, С ПОМОЩЬЮ СЕТЕЙ ПЕТРИ ВЫСОКОГО УРОВНЯ Математика

Текст научной статьи на тему «МОДЕЛИРОВАНИЕ И ВЕРИФИКАЦИЯ КОММУНИКАЦИОННЫХ ПРОТОКОЛОВ, ПРЕДСТАВЛЕННЫХ НА ЯЗЫКЕ SDL, С ПОМОЩЬЮ СЕТЕЙ ПЕТРИ ВЫСОКОГО УРОВНЯ»

ТЕСТИРОВАНИЕ, ВЕРИФИКАЦИЯ И ВАЛИДАЦИЯ ПРОГРАММ

УДК 21.22

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

© 2008 г. В. А. Непомнящий12, В. С. Аргиров1, Д. М. Белоглазов1, А. В. Быстров1'2, Е. А. Четвертаков1, Т. Г. Чурина1'2

1 Институт систем информатики им. А.П. Ершова СО РАН 630090 Новосибирск, проспект Академика Лаврентьева, 6 2Новосибирский государственный университет 630090 Новосибирск, ул. Пирогова, 2 E-mail: vnep@iis.nsk.su Поступила в редакцию 17.04.2008 г.

С целью упрощения моделирования и верификации коммуникационных протоколов, представленных на языке SDL, вводятся так называемые иерархические временные типизированные сети Петри (ИВТ-сети), которые являются существенной модификацией раскрашенных сетей Петри. Описан метод трансляции языка SDL в ИВТ-сети. Представлен программный комплекс SPV (SDL Protocol Verifier), который включает транслятор из SDL в ИВТ-сети, а также средства для редактирования, симуляции, визуализации и верификации этих сетевых моделей. Для верификации используется метод проверки моделей относительно свойств, представленных формулами мю-исчисления. Описаны эксперименты по применению комплекса SPV для моделирования и верификации двух кольцевых протоколов (RE-протокола и ATMR-протокола), оптимизированной версии протокола скользящего окна (i-протокола), а также динамической версии протокола InRes.

1. ВВЕДЕНИЕ

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

* Данная работа частично поддержана грантом Российского фонда фундаментальных исследований 07-07-00173.

Естественный подход для преодоления этих трудностей состоит в использовании таких моделей, как конечные автоматы, сети Петри и их обобщения. Среди этих моделей можно выделить раскрашенные сети Петри (РСП) [2], так как они имеют значительную выразительную силу, большой опыт применения и для них реализованы мощные средства анализа [3, 4]. Однако ручное построение моделей используемых на практике коммуникационных протоколов часто приводит к серьезным ошибкам. Поэтому возникает задача автоматического построения сетевых моделей для протоколов, представленных на SDL.

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

35

3*

лами и охранными условиями для переходов, описана в [5]. Трансляция из SDL в сети Петри высокого уровня, названные М-сетями, описана в [6]. Практический метод трансляции из SDL в так называемые Pr/T-сети описан в [7]. Заметим, что все перечисленные сетевые модели существенно отличаются от РСП.

Различные программные системы были реализованы для анализа, моделирования и верификации этих сетевых моделей. Среди них следует упомянуть SITE [5], PEP [8], Emma [9], Maria [7], Design/CPN [з], CPN Tools [4]. Отметим, что для верификации сетевых моделей системы PEP, Emma и Maria используют метод проверки моделей.

С целью упрощения трудоемкого процесса моделирования и верификации протоколов мы вводим так называемые иерархические временные типизированные сети (ИВТ-сети), которые являются существенной модификацией РСП, и предлагаем метод трансляции SDL в ИВТ-сети. Этот метод реализован в программном комплексе SPV (SDL Protocol Verifier), который включает также средства для редактирования, моделирования, визуализации и верификации этих сетевых моделей.

Результаты данной работы были представлены на конференции CSR 2007 [10].

Данная статья состоит из шести разделов. ИВТ-сети представлены в разделе 2. Методу трансляции SDL в ИВТ-сети посвящен раздел

3. Программный комплекс SPV описан в разделе

4. Результаты экспериментов по моделированию и верификации коммуникационных протоколов приведены в разделе 5. В разделе 6 обсуждаются достоинства и перспективы нашего подхода.

2. ИВТ-СЕТИ

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

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

В отличие от ординарных сетей Петри каждая фишка в раскрашенной сети обладает индивидуальностью - значением некоторого типа, которое называется цветом. Неиерархическая раскрашенная сеть состоит из трех частей: структуры сети, деклараций и пометки сети. Декларации состоят из описания множеств цветов (типов) и объявления переменных, каждая из которых принимает значения из некоторого множества цветов. Декларации также могут содержать определение операций и функций. Декларации сети будем изображать курсивным шрифтом. В раскрашенных сетях определены четыре базовых множества цветов, соответствующие стандартным типам: целый, вещественный, строковый и булевский. Базовым также является специальное множество цветов, состоящее из одного элемента, который не несет информации: color Char = withe. Фишка со значением e называется ординарной или бесцветной. Множество цветов может описываться путем перечисления всех возможных значений.

В ИВТ-сетях допускается тип массив и запись. Кроме того, в сети могут присутствовать места-очереди, способные хранить неограничен-

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

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

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

нимают значения из множества цветов, приписанного месту, инцидентному дуге. На рисунках декларации могут опускаться.

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

Для дальнейшего прочтения статьи необходимо приобрести полный текст. Статьи высылаются в формате PDF на указанную при оплате почту. Время доставки составляет менее 10 минут. Стоимость одной статьи — 150 рублей.

Показать целиком