Описание работы протокола

Система передачи данных, реализуемая с помощью протокола, состоит из трех подсистем: отправитель, получатель и сеть, по которой в одну сторону передается сообщение, а в обратную сторону - подтверждение о приеме сообщения получателем («квитанция»).

По сети передается сообщение, разбитое на N фрагментов, называемых пакетами. Каждый пакет состоит из номера (целое число типа integer с временной меткой) и текстовой части (типа string). Первоначально все N пакетов находятся в позиции Р1. Целью работы системы является передача всех пакетов получателю в позицию Р2 с сохранением последовательности их номеров. Кроме того, отправитель должен получить «квитанции» о передаче всех пакетов, и эти«квитанции» с пометкой о времени передачи помещаются в P1.

Позиции РЗ, Р4 моделируют, соответственно, условия начала и конца передачи пакетов, а позиции Р8, Р 7 моделируют условия начала и конца передачи «квитанций».

Позиции Р5, Рб являются счетчиками, т.е. хранят номера отправленных и принятых пакетов.

Переход t, моделирует начало передачи очередного пакета, переходы t₂ и t₅ - прохождение, соответственно, пакета и «квитанции» через сеть, переход t₃ - прием и анализ очередного пакета, переход t₄ - прием и анализ очередной «квитанции».

2_< Формальное описание CPN, моделирующей протокол.

Ниже приведено формальное описание сети на рисунке 2.25 в сокращенном виде.

Множество цветов:

type color INT - integer timed;

type color DATA = string ;

type color PACKET = produrt INT x DATA timed ;

Var n, k: соlor INT \ Var d : color DATA;

• Множества позиций Р = {Р1,...,Р8) и переходов T = (tl,...,t5) показаны непосредственно на рисунке.

• Цветовая функция имеет вид

color PACKET if {P1,P2,P3,P4}

C(p)=

color INT otherwise

•Выражения на дугах Е(а) показаны непосредственно на рисунке. Обратим внимание на дуги t2 to P4 и t5 to P7. Выражения на этих дугах зависят от датчика случайного кода Рr, который с определенной вероятностью вырабатывает значение true или false. Прохождение сигнала по этим дугам рассмотрено ниже.

• Функции на переходах G(t), определяющие временные задержки при срабатывании переходов, (т.е. передаче сообщений), показаны на рисунке.

•Функция инициализации имеет вид (рис. 2.25) m₀{Pl)= 1’(1," раск1’’);1’(2," pack2");...;1’(N," packN") - иными словами, в начальный момент времени (Θ= 0 ,τ = 0) в позиции P1 находится N подлежащих передаче пакетов, структура которых определена типом color PACKET;

т_о{Р5)=т_о(Рб) = 1’1 - начальный номер передаваемого пакета.

т_о (Р2) = т₀ (Р3)= т₀ (Р4) = т₀ (Р7) = т₀ {Р8) = Ø .