сервиса верхнего уровня протокол должен выполнять ряд задач низкого уровня –
синхронизации, распознавания и коррекции ошибок. То, как протокол выполняет эти задачи,
зависит от свойств среды его исполнения.
Словарь допустимых сообщений и их кодировка также связаны с предположениями о
среде исполнения протокола – среде передачи данных. Вероятность возникновения битовых
ошибок и средняя длина
поля последовательности битовых ошибок влияют на набор, формат
и кодировку сообщений протокола, а также выбор алгоритма распознавания или коррекции
ошибок.
1.7.3.4. Определение протокола через "связанные конечные автоматы"
На низком уровне абстракции протокол можно представить в виде конечных
автоматов. В своей монографии [3] Хольцман предлагает так называемую модель связанных
конечных автоматов для формализованного
описания протокола. В этом случае задачи
разработки, формальной верификации и проверки на совместимость сводятся к нахождению
желаемых/нежелаемых состояний и переходов. Каждый из связанных конечных автоматов
может получать символы на вход, осуществлять переход в новое состояние и генерировать
символьную информацию на выходе. Отдельные конечные автоматы связываются между
собой посредством ограниченных FIFO
очередей, через которые выходной сигнал одного
автомата поступает на вход другого. Так моделируется асинхронная связь, характерная для
большинства коммуникационных систем.
Определение очереди: очередь сообщений (символов) представляется тройкой (S, N,
C), где S - ограниченное множество определяющее словарь очереди, N - целое число позиций
в очереди, C - упорядоченное множество элементов из S. S и С: множества сообщений. Если
модель системы требует
наличия нескольких очередей, то их словари должны образовывать
непересекающиеся множества. Если M множество всех системных очередей, индекс
|
нумерует очереди, а
|1 Mm ≤≤
Nn
1
позиции внутри очереди, - n-ный символ в m-той
очереди. Системный словарь тогда выражается через словари каждой из очередей и нулевой
символ
m
n
C
: . В [3] дается определение связанных конечных автоматов как набора
(Q,
, M, T), где Q - конечное непустое множество состояний, - элемент Q - начальное
состояние, M - множество символьных очередей, определенных выше, T - отношение
перехода. T имеет два аргумента T(q, a), где q текущее состояние и a - действие (одно из:
ввод, вывод, пустое действие). Реализация перехода с действиями типа ввод/вывод зависит
от состояния символьных очередей. При их реализации изменяется состояние одной из
очередей. Отношение перехода T задает множество (которое может
быть пустым) всех
ε
ΥΥ
mM
m
SV
||
1=
=
0
q
0
q
13