Дубинин В.Н., Зинкин С.А. Языки логического программирования в проектировании вычислительных систем и сетей

Подождите немного. Документ загружается.

arc(S,i_reply(I),S1):-

remove([idle(I,H),request(J,I,O)],S,S2),

others(I,J),max(H,O,K),

insert([ack(I,J),idle(I,K)],S2,S3),

shift(S3,S1).

arc(S,w_reply(I),S1):-

remove([waiting(I,OI,H),request(J,I,OJ)],S,S2),

others(I,J),max(H,OJ,K),priority(OJ,OI,J,I),

insert([ack(I,J),waiting(I,OI,K)],S2,S3),

shift(S3,S1).

Клозы, определяющие временную трансформацию для каждой позиции:

transfo(idle(I,suc(H)),idle(I,H)).

transfo(request(I,J,suc(H)),request(I,J,H)).

transfo(waiting(I,suc(H),suc(H)),waiting(I,H,H)).

transfo(ack(I,J),ack(I,J)).

transfo(critical(I,suc(H)),critical(I,H)).

Графическое представление рассмотренной сетевой модели приведено на

рис. 2.8. Начальная маркировка данной сетевой модели определяется

следующим фактом:

init([idle(site_a,h),idle(site_b,h)]).

Рис.2.8.Сетевая модель алгоритма взаимного исключения

При использовании приведенных в разд. 1.4 клозов, будут получены

следующие выходные данные, определяющие ГДС:

о достигнутых состояниях (база данных rstate):

0 [idle(site_a,h),idle(site_b,h)]

1 [request(site_a,site_b,suc(h)),waiting(site_a,suc(h),suc(h)),

idle(site_b,h)]

2 [request(site_b,site_a,h),waiting(site_b,h,h),

request(site_a,site_b,h),waiting(site_a,h,h)]

3 [ack(site_b,site_a),waiting(site_b,h,h),request(site_b,site_a,h),

waiting(site_a,h,h)]

4 [critical(site_a,h),waiting(site_b,h,h),request(site_b,site_a,h)]

5 [idle(site_a,h),waiting(site_b,h,h),request(site_b,site_a,h)]

6 [request(site_a,site_b,suc(h)),waiting(site_a,suc(h),suc(h)),

waiting(site_b,h,h),request(site_b,site_a,h)]

7 [ack(site_a,site_b),waiting(site_a,suc(h),suc(h)),

request(site_a,site_b,suc(h)),waiting(site_b,h,h)]

8 [critical(site_b,h),waiting(site_a,suc(h),suc(h)),

request(site_a,site_b,suc(h))]

9 [ack(site_a,site_b),idle(site_a,h),waiting(site_b,h,h)]

10 [critical(site_b,h),idle(site_a,h)]

11 [ack(site_b,site_a),idle(site_b,h),waiting(site_a,h,h)]

12 [request(site_b,site_a,suc(h)),waiting(site_b,suc(h),suc(h)),

ack(site_b,site_a),waiting(site_a,h,h)]

13 [critical(site_a,h),request(site_b,site_a,suc(h)),

waiting(site_b,suc(h),suc(h))]

14 [idle(site_a,h),request(site_b,site_a,suc(h)),

waiting(site_b,suc(h),suc(h))]

15 [critical(site_a,h),idle(site_b,h)]

о дугах ГДС (база данных gds):

0 send(site_a) 1

1 send(site_b) 2

2 w_reply(site_b) 3

3 receive(site_a) 4

4 release(site_a) 5

5 send(site_a) 6

6 w_reply(site_a) 7

7 receive(site_b) 8

8 release(site_b) 1

5 i_reply(site_a) 9

9 send(site_a) 7

9 receive(site_b) 10

10 send(site_a) 8

10 release(site_b) 0

1 i_reply(site_b) 11

11 send(site_b) 12

12 receive(site_a) 13

13 release(site_a) 14

14 send(site_a) 2

14 i_reply(site_a) 9

11 receive(site_a) 15

15 send(site_b) 13

15 release(site_a) 0

0 send(site_b) 14

Графическое представление данного ГДС приведено на рис. 2.9. После

того, как конечно-автоматная модель, представленная графом достижимых

состояний, построена, проверяются три фундаментальные свойства

рассматриваемого алгоритма взаимного исключения:

- взаимное исключение;

- отсутствие оттеснений (умираний);

- отсутствие тупиков.

Рис.2.9.Граф достижимости состояний сетевой модели алгоритма взаимного

исключения

Следует заметить, что проверка данных свойств на основе визуального

анализа затруднена и данные свойства неочевидны. В подразделе 3.3 будет

проведена проверка данных свойств с использованием временной логики.

2.5. Альтернативно-битовый протокол

Неформальное описание

В качестве примера протокола для исследования выбран простой

протокол "с нумерацией по модулю 2", хорошо известный также под

названием альтернативно-битового протокола (АБ-протокола) [26,27]. В

соответствии с моделью ВОС АБ-протокол относится к канальному

уровню. Модель уровня АБ-протокола представлена на рис.2.10. Канальные

сервисные блоки данных в дальнейшем будем называть кадрами, а сетевые

сервисные блоки данных - сообщениями. Синтаксис АБ-протокола

несложен и представляет собой определение форматов кадров для данных и

подтверждений. В поле управления кадра имеется бит четности кадра,

принимающий значение 0 или 1. Для кадра данных обозначим его через FP, а

для кадра подтверждения - через АР. Значения бита четности в

последовательно передаваемых кадрах данных чередуются. После того как

по логическому каналу передан кадр данных с битом четности 0, следующий

кадр данных по этому же каналу будет передаваться с битом четности 1, но

только после того, как принято подтверждение о принятии предыдущего

кадра.

Пользователи верхнего (сетевого) уровня обмениваются с уровнем АБ-

протокола сообщениями, а среда (физический уровень) передает кадры.

Среда может задерживать, искажать и терять кадры, но не может их

переупорядочивать и дублировать. Среда обеспечивает двунаправленную

передачу кадров. На рис.2.10 через X и Y обозначены точки доступа к

сервису, предоставляемому АБ-протоколом, а α, β, γ, δ - точки доступа к

сервису, используемому АБ-протоколом. Примитивы ПРД, ПРН, "передать",

"принять" играют только синхронизирующую роль, поэтому информация

должна помещаться в точки доступа и извлекаться из них явным способом.

Примитивы ПРД и ПРН могут выполняться только совместно с объектом

верхнего уровня, а "передать" и "принять" - совместно со средой.

Рис.2.10.Модель уровня альтернативно-битового протокола

В структуру объекта-передатчика входят : буфер для переданного, но не

подтвержденного кадра, таймер (часы) для реализации механизма тайм-

аутов, бит-переменная ТР - четность передатчика (рис.2.10).

В структуру объекта-приемника входит переменная RP - четность

приемника, используемая для контроля правильности последовательности

битов четности кадров.

Семантика АБ-протокола состоит в действиях по передаче и приему

кадров. Определим семантику АБ-протокола в форме словесного описания.

Получив требуемое для передачи сообщение, объект-передатчик

формирует из него кадр данных и устанавливает бит четности кадра, равный

четности передатчика. Сформированный таким образом кадр передается в

среду, а его копия сохраняется в буфере передатчика. После этого

передатчик дожидается поступления кадра подтверждения, содержащего бит

четности, значение которого равно значению четности последнего

переданного кадра данных. Если кадр подтверждения принимается с

искажениями или бит четности в подтверждении не сов падает со значением

бита четности последнего переданного кадра данных, то передатчик

повторно передает запоминаемую копию. Иначе останавливается таймер,

освобождается буфер, значение бита четности меняется на

противоположное.

Если таймер выдал сигнал окончания тайм-аута, то передатчик повторно

передает помещенную в буфер передатчика копию кадра. Окончание тайм-

аута свидетельствует (если исключить из рассмотрения сбои аппаратуры) о

потере или кадра данных, или кадра подтверждения. При потере кадра

подтверждения при повторной передаче кадра данных произойдет нарушение

правильности последовательности битов четности, что обнаружится

приемником, и дублирующий кадр будет отброшен.

Объект-приемник, приняв кадр, проверяет, не искажен ли кадр средой.

Если кадр искажен или значение бита четности принятого кадра данных не

равно значению бита четности приемника, то приемник уничтожает

принятый кадр, в противном случае он выделяет из кадра сообщение и

передает его пользователю-получателю. В любом случае приемник

формирует кадр подтверждения, значение бита четности в котором

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

Заметим, что первоначальные значения четности приемника и четности

передатчика устанавливаются равными друг другу. В литературе [26,27]

описывается АБ-протокол, в котором первоначальные значения четности

передатчика и приемника не совпадают, что в конечном счете не

принципиально.

Следует отметить, что для формального описания семантики АБ-

протокола применимы все средства и методы формального описания,

перечисленные в начале данной главы. Каждый из методов имеет свои

преимущества и недостатки. Предпочтение тому или иному методу может

быть отдано в зависимости от целей дальнейшего использования

формального описания: для верификации, оценки качества

функционирования протокола и выбора параметров протокола или для

реализации. В [26] АБ-протокол описан с использованием диаграмм

состояний и в виде программы, в [33] - с использованием сети "предикат-

переход", в [27] - с использованием временной логики, языков

LOTOS,ESTELLE и OCA.

Формально семантика АБ-протокола может описываться в виде

программы, приведенной ниже.

ПЕРЕДАТЧИК

Посылка нового кадра

ПРИЕМНИК

Прием кадра

ЕСЛИ TS = "готова",

ТО

{TS:= "занята";

Выбрать кадр со входа

передатчика и поместить

в буфер;

FP:=TP;

Передать кадр;

Запустить таймер;}

ЕСЛИ нет ошибок и FP=RP,

ТО

{ Передать принятый кадр

на верхний уровень;

RP:=(FP+1)mod2; }

AP:=FP;

Послать подтверждение;

Прием подтверждения

Окончание тайм-аута

ЕСЛИ нет ошибок и AP=TP, Повторная передача;

{Удалить кадр из буфера;

Повторная передача

Остановить таймер;

TP:=(TP+1)mod2;

TS:= "готова"; }

ИНАЧЕ

Повторная передача;

FP:=TP;

Передать кадр;

Повторный запуск таймера;

Здесь приняты следующие обозначения: RP - четность приемника; TP -

четность передатчика; FP - четность кадра; AP - четность подтверждения; TS

- состояние передатчика. Начальные условия системы: RP=TP; TS="готова".

Сетевая модель

Для целей верификации АБ-протокол удобно представить в виде

предикатной сети (рис.2.11). Следует отметить, что в представленной

модели считается, что любое искажение кадра распознаваемо и не приводит к

появлению действительных кадров. В сетевой модели не рассматриваются

следующие ситуации: 1) прием подтверждения, четность которого не равна

четности посланного кадра; 2) прием искаженного подтверждения (данная

ситуация моделируется ситуацией потери подтверждения). На принятом

уровне абстракции не рассматривается явно работа таймера.

Ðèñ.2.11.Ñåòåâàÿ ìîäåëü àëüòåðíàòèâíî-áèòîâîãî ïðîòîêîëà

Существует три типа меток, циркулирующих в рассматриваемой сетевой

модели: 1) метки, циркулирующие по позициям, определяющим состояние

передатчика (psend и wait) и приемника (prec); 2) метки, циркулирующие по

позициям, представляющим тракт передачи (send, receive); 3) метки,

представляющие признаки.

Метки первого типа имеют один атрибут - четность (0 или 1). Метки

второго типа имеют следующую структуру: 1-й атрибут - идентификатор

(адрес) передающей стороны; 2-й атрибут - идентификатор (адрес)

принимающей стороны; 3-й атрибут - тип сообщения; 4-й атрибут - четность

сообщения.

Домен идентификаторов передающей или принимающей стороны -

множество {se,re}, причем se соответствует передатчику, а re -приемнику.

Следует заметить, что как приемник, так и передатчик могут выполнять

роль как приемной, так и передающей сторон. Кадр в АБ- протоколе может

быть двух типов: информационным кадром (кодируется как mes) и

подтверждением (кодируется как ack). Четность кадра может принимать

значение zero (ноль) или one (единица). Вместо zero и one иногда будем

писать 1 и 0 соответственно.

Метки третьего типа не имеют атрибутов.

Интерпретация позиций сетевой модели следующая (интерпретация

приводится для маркированных позиций):

psend - готовность передатчика послать новый кадр. Четность

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

метки;

wait - ожидание приема подтверждения;

send - посылка передатчиком кадра;

receive - прием кадра приемником;

prec - готовность приемника принять кадр. Четность приемника

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

Ниже представлена конфигурация переходов сетевой модели и дана их

интерпретация.

1. Переход tsend(B) - "Посылка передатчиком нового кадра и переход из

состояния готовности в состояние ожидания подтверждения".

Пре-условия: psend(B).

Пост-условия: wait(B), send(se,re,mes,B).

2. Переход recack(B) - "Прием подтверждения передатчиком, переход из

состояния ожидания в состояние готовности, изменение четности

передатчика".

Пре-условия: wait(B),receive(re,se,ack,B).

Пост-условия: psend(BB).

Преобразования в переходе: comp(B,BB).

3. Переход repeatm(B) - "Повторная передача кадра".

Пре-условия: wait(B), ploss.

Пост-условия: wait(B), send(se,re,mes,B).

4. Переход propagate(M) - "Передача сообщения по каналу передачи".

Пре-условия: send(X,Y,T,M).

Пост-условия: receive (X,Y,T,M).

5. Переход loss - "Потеря сообщения".

Пре-условия: send(X,Y,T,M).

Пост-условия: ploss.

6. Переход reception(B) -"Принять кадр и изменить четность

приемника".

Пре-условия: receive(X,re,mes,B), prec(B).

Пост-условия: prec(BB), send(re,X,ack,B).

Преобразования в переходе: comp(B,BB).

7. Переход repeata(B) - "Повторная передача подтверждения".

Пре-условия: receive(X,re,mes,BB), prec(B).

Пост-условия: prec(B), send(re,X,ack,BB).

Условия по данным: comp(B,BB).

Предикат comp определяется с помощью фактов следующим образом:

comp(zero,one).

comp(one,zero).

Cледует заметить, что утверждение comp(B,BB) используется как условие

в случае, когда обе переменные B и BB конкретизированы, так и для

реализации операции "сложение по модулю 2", в этом случае BB=B ⊕1.

Клозы, определяющие переходы данной сетевой модели, имеют

следующий вид:

arc(S,tsend(B),S1):-

remove([psend(B)],S,S2),

insert([send(se,re,mes,B),wait(B)],S2,S1).

arc(S,loss,S1):-

remove([send(X,Y,T,M)],S,S2),

insert([ploss],S2,S1).

arc(S,propagate(M),S1):-

remove([send(X,Y,T,M)],S,S2),

insert([receive(X,Y,T,M)],S2,S1).

arc(S,recack(B),S1):-

remove([receive(re,se,ack,B),wait(B)],S,S2),

comp(B,BB),

insert([psend(BB)],S2,S1).

arc(S,repeatm(B),S1):-

remove([wait(B),ploss],S,S2),

insert([wait(B),send(se,re,mes,B)],S2,S1).

arc(S,repeata(B),S1):-

remove([receive(X,re,mes,BB),prec(B)],S,S2),

comp(B,BB),

insert([prec(B),send(re,X,ack,BB)],S2,S1).

arc(S,reception(B),S1):-

remove([receive(X,re,mes,B),prec(B)],S,S2),

comp(B,BB),

insert([prec(BB),send(re,X,ack,B)],S2,S1).

Начальная маркировка сетевой модели определяется следующим

фактом:

init([psend(zero),prec(zero)]).

При использовании приведенных в разд. 1.4 клозов получаются

следующие выходные данные, определяющие ГДС:

о достигнутых состояниях (база данных rstate):

0 [psend(zero),prec(zero)]

1 [send(se,re,mes,zero),wait(zero),prec(zero)]

2 [ploss,wait(zero),prec(zero)]

3 [receive(se,re,mes,zero),wait(zero),prec(zero)]

4 [prec(one),send(re,se,ack,zero),wait(zero)]

5 [ploss,prec(one),wait(zero)]