Часть X

10.2. Модель и спецификация протокольного автомата

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

a) спецификации сервиса протокола или его абстрактного интерфейса,

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

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

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

    Другим важным достоинством модели сервиса является то, что в ней заложен подход к определению семантики переносимых сервисными примитивами данных через описание типов и значений параметров. В частности, именно, через механизм параметров осуществляется реализация отображения (N+1)-протокольных блоков данных в (N)-сервисные блоки данных, рассмотренного в предыдущей главе (рис. 9.3).

    Используя отмеченные выше решения, рассмотрим некоторые элементы теории сетевых протоколов, к центральным задачам которой относятся:

• разработка средств и методов формальной спецификации сетевых протоколов и сервисов;
• разработка метод верификации и анализа функционирования реализаций сетевых протоколов;
• разработка средств и методов автоматизации тестирования реализаций сетевых протоколов;
• автоматизация программирования реализаций сетевых протоколов и пр.

    Начнем знакомство с этой теории с рассмотрения вопросов формальной спецификации протоколов и сервисов.

10.2.1 Машина с конечным числом состояний как модель протокольной сущности

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

    Дадим наиболее общее определение машины с конечным числом состояний, применяемой при моделировании поведения протокольных сущностей.

    Машина с конечным числом состояний (Finite-State Machine - FSM), описывающая поведение протокольной сущности, представляет собой следующую пятерку: M = (I, O, S, D, L), где I - входной алфавит, включает сервисные примитивы request/response (Abstract Service Primitives - ASPs), исходящие от пользователя, и набор блоков PDU, исходящих от протокольного автомата того же уровня (peer-entity), партнера по взаимодействию. O - выходной алфавит, включает сервисные примитивы indication/confirmation (ASPs), направляемые пользователю, и набор блоков PDU, направляемых партнеру по взаимодействию (peer-entity). S - набор состояний, где s из S - начальное состояние, F - непустое подмножество состояний, интерпретируемых как конечные состояния. D: I*S -> S - функция перехода в новое состояние. L: I*S -> O - функция вывода.

    Для представления функций переходов и вывода FSM используются, как правило,

• таблицы состояний или
• диаграммы состояний.

    Эти способы представления функций FSM рассмотрим на примере протокола ABP.

10.2.2 Спецификация протокола ABP

    Для примера спецификации сетевых протоколов рассмотрим простой протокол канального уровня, использующий схему нумерации пакетов по модулю два (Altering Bit Protocol - ABP). Данный протокол предназначен для обеспечения надежной однонаправленной передачи сообщений от пользователя-источника к пользователю-получателю, причем передача данных может осуществляться через ненадежную среду передачи.

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

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

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

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

    Если пакет подтверждения принимается с искажением (ошибка передачи или значение бита в подтверждении не совпадает со значением номера последнего переданного пакета), то передатчик повторяет передачу запомненной копии пакета.

    Сущность-приемник (RECEIVER), приняв пакет, прежде всего, проверяет, не искажен ли пакет средой. Если пакет искажен или значение номера пакета равно значению номера предыдущего пакета, то приемник уничтожает принятый пакет, в противном случае он выделяет из пакета сообщение и передает его пользователю-получателю. В любом случае приемник формирует пакет-подтверждение, содержащего значение номера последнего правильно принятого пакета.

    Архитектура протокола ABP представлена на рис. 10.5, где используются следующие обозначения:

    n - PhSAP, u - LDSAP - точки доступа к сервису в подсистемах SENDER и RECEIVER. Имена точек n и u далее будут использоваться как префиксы примитивов.

Рис. 10.5. Архитектура протокола ABP

    Используя данное выше определение машины с конечным числом состояний, построим спецификацию поведения протокольной сущности SENDER на основе этого понятия.

    Определим входной и выходной алфавиты для конечного автомата, описывающего поведение сущности SENDER.

    Состав абстрактных сервисных примитивов ASPs для сущности SENDER следующий:

• Send_request (или для краткости Send_req), инициируется пользователем сущности SENDER в точке u.
• Send_confirm (или для краткости Send_conf), инициируется сущностью SENDER в точке u.

    Блоками данных PDU, пересылаемых от сущности SENDER к сущности RECEIVER, являются:

• DT0 - четный пакет данных, будем считать, что инициируется сущностью SENDER в точке n, т.к. между пакетами и примитивами физического уровня может быть установлено взаимнооднозначное соответствие.
• DT1- нечетный пакет данных, инициируется сущностью SENDER в точке n с учетом таких же замечаний, как и для блока DT0.

    К блокам данных PDU, пересылаемым от сущности RECEIVER к сущности SENDER, относятся:

• ACK0 - подтверждение о принятии четного пакета
• ACK1 - подтверждение о принятии нечетного пакета.

    Таким образом, для сущности SENDER протокола ABP имеем:

I(SENDER)={u.Send_req, n.ACK0, n.ACK1}

O(SENDER)={u.Send_conf, n.DT0, n.DT1}.

    Начальное состояние сущности SENDER - Ready.

    Когда сущность SENDER находится в состоянии Ready, она может принять на вход только одно событие u.Send_req. В этом случае значениями функций L и D будут:

L(u.Send_req,Ready) = n.DT0

D(u.Send_req,Ready) = WFACK0.

    Эти значения интерпретируются следующим образом: сущность SENDER продуцирует на выходе в точке n четный блок данных DT0 (событие n.DT0) и переходит в состояние WFACK0 - состояние ожидания поступления в точку n блока данных ACK0 (подтверждения правильного приема сущностью RECEIVER блока данных DT0).

    Кроме присваивания нового значения переменной, определяющей текущее состояние протокольного автомата, функция D может выполнять дополнительные семантические действия, связанные с реализацией протокольных функций, например, установку таймера для контроля ситуации, когда время ожидания события n.ACK0 будет исчерпано.

    Находясь в состоянии WFACK0, сущность SENDER протокола ABP может получить два входных события n.ACK0 и n.ACK1, свидетельствующих о поступлении подтверждений ACK0 и ACK1 соответственно. В принципе, чтобы сделать наш протокол более защищенным от ошибок передачи на физическом уровне, было бы целесообразно ввести в протокол аппарат таймеров. Тогда к возможным входным событиям для состояния WFACK0 добавилось бы событие, связанное с приходом сигнала от таймера, извещающего об исчерпании времени ожидания подтверждения передачи. Для упрощения рассматриваемой модели протокола ABP такой аппарат вводиться нами не будет, хотя к обсуждению этого вопроса мы еще вернемся.

    При получении события n.ACK0 сущность SENDER перейдет в состояние Ready1, продуцируя при этом в точке u для своего пользователя сервисный примитив подтверждения Send_conf (событие u.Send_conf). В новом состоянии сущность SENDER будет готова к обслуживанию очередного запроса на передачу сообщения от пользователя посредством передачи нечетного блока данных (DT1).

    При получении события n.ACK1 сущность SENDER останется в состоянии WFACK0 и повторит передачу своему партнеру блока DT0. При этом семантическое действие, обрабатывающее данную ситуацию может включать подсчет числа повторов передачи блока данных и вызывать действия по обработке ситуации, связанной с исчерпанием максимального числа повторов передачи.

    Таким образом, функции L и D для состояния WFACK0 будут иметь следующие возможные значения:

L(n.ACK0, WFACK0) = u.Send_conf

D(n.ACK0, WFACK0) = Ready1

L(n.ACK1, WFACK0) = n.DT0

D(n.ACK1, WFACK0) = WFACK0.

    В состоянии Ready1 функции L и D определяются следующим образом:

L(u.Send_req,Ready1) = n.DT1

D(u.Send_req,Ready1) = WFACK1.

    В состоянии WFACK1 сущность SENDER ожидает подтверждения передачи пакета DT1 (событие n.ACK1), после поступления которого осуществит переход в состояние Ready0 и выдаст в точке u для своего пользователя сервисный примитив подтверждения Send_conf (событие u.Send_conf).

    При получении события n.ACK0 (отрицательное подтверждение) сущность SENDER останется в состоянии WFACK1 и повторит передачу блока DT1.

    Таким образом, в состоянии WFACK0 функции L и D определяются следующим образом:

L(n.ACK1, WFACK1) = u.Send_conf

D(n.ACK1, WFACK1) = Ready

L(n.ACK0, WFACK1) = n.DT1

D(n.ACK0, WFACK1) = WFACK1

    На рис.10.6 иллюстрируется способ спецификации поведения протокольной сущности SENDER, использующий диаграмму состояний соответствующего абстрактного автомата.

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

    Еще раз анализирую семантику протокола ABP, легко увидеть, что даже для описания такого простого протокола, каким является ABP, чисто автоматная модель описания его динамики функционирования представляется ограниченной, хотя такая модель и позволяет описать основные логические аспекты функционирования протокола. Поэтому на практике используются различного рода расширения описательных возможностей конечных автоматов. Такие расширения предпринимаются в следующих направлениях: введения глобальной памяти или глобальных переменных, называемых также переменными истории, замену функции D на процедурную семантику с возможность анализа условий и выбора альтернативных решений, использования аппарата таймаутов, структуризации состояний автомата, расширения функций автомата внешней схемой управления (управляющими предикатами) и пр. Все эти расширения повышают удобство спецификации сетевых протоколов, делая эти спецификации более компактными и адекватными семантике протоколов.

Рис. 10.6. Диаграмма состояний для протокола ABP

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

    Во-первых, в нашу модель мы введем следующие глобальные переменные истории: RECEIVER_STATE, BUFFER, и H_PN.

    Первая из них будет определять текущее состояние рассматриваемой сущности.

    Вторая - будет служить входным буфером и хранить содержимое полученного от физического уровня пакета (DT0 или DT1).

    Третья предназначена для хранения номера текущего принятого и обрабатываемого сущностью RECEIVER пакета.

    Допустим, также, что начальное значение переменных истории H_PN и RECEIVER_STATE будет установлено в 0 и Ready, соответственно.

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

    В-третьих, такое же расширение, какое мы допустили для функции D, мы допустим и для функции L.

    В-четвертых, введем в язык описания семантики протоколов следующие встроенные функции:

? - функция ввода входного события (из точки u или из точки n в зависимости от префикса события или контекста)

! - функция вывода выходного события (в точку u или в точку n в зависимости от префикса события или контекста)

NUM() - функция определения номера последнего принятого пакета, хранящегося в переменной BUFFER.

    Остальное все будет аналогично тому, что мы делали для сущности SENDER.

    Состав абстрактных сервисных примитивов ASPs для сущности RECEIVER следующий:

• Rec_indication (или для краткости Rec_ind), инициируется сущностью RECEIVER в точке u.
• Rec_respond (или для краткости Rec_res), инициируется пользователем сущности RECEIVER в точке u.

    Блоки данных PDU, пересылаемые между сущностями SENDER и RECEIVER, такие же, как рассматривались выше, к ним относятся пакеты: DT0, DT1, ACK0, ACK1.

    Таким образом, для сущности RECEIVER протокола ABP имеем:

I(RECEIVER)={u.Rec_res, n.DT0, n.DT1}

O(RECEIVER)={u.Rec_ind, n.ACK0, n.ACK1}.

    Когда сущность RECEIVER находится в состоянии Ready, она может принять в начальный момент только одно событие n.DT0. Использую введенные выше расширения, параметризуем это состояния таким образом, чтобы его можно было бы использовать и для получения не только начального пакета, но и других пакетов, следующих в последовательности, т.е. придадим этому событию свойство универсального средства приема пакетов как DT0, так и DT1. В этом случае потребуется еще одно состояние, в котором сущность RECEIVER будет ожидать поступления события с ответом пользователя (u.Rec_res), и по прибытии этого события будет выдавать в среду пакет, подтверждающий прием последнего переданного пакета.

    В этом случае функции примут следующий вид L и D:

a) в случае состояния Ready и поступления событий n.DT0 или n.DT1

D_and_L_Ready()=

{

?BUFFER; //чтение нового пакета в переменную BUFFER

if H_PN= NUM() //пришел пакет с ожидаемым номером

then {!u.Rec_ind, //доставка пакета пользователю через событие u.Rec_ind

RECEIVER_STATE=RWR //перевод автомата в состояние RWR}

else

if H_PN=0 //выдача в точку n некорректного подтверждения

then !ACK1

else !ACK0

}

b) в случае состояния RWR и поступления u.Rec_res

D_and_L_RWR()=

{

? u.Rec_res; //ожидание и ввод события u.Rec_res

RECEIVER_STATE=Ready //перевод автомата в состояние приема пакетов}

if H_PN=0 //выдача в точку n подтверждения

then !ACK0

else !ACK1

}

    Полученное описание представляет собой набор семантических подпрограмм (D_and_L_Ready() и D_and_L_RWR()), вызываемых при возникновении в некотором состоянии автомата некоторого события.

    Общая логика работы такого автомата может быть задана таблицей состояние/входное событие, возможная форма которой приведена на рис.10.8.

    Рис. 10.8. Таблица состояний для протокола ABP

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

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