Операции над протоколами

 

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

s, t, u - протоколы,

S, Т, U - множества протоколов,

f, g, h – функции.

 

Конкатенация

Наиболее важной операцией над протоколами является конкатенация s^t, которая строит новый протокол из пары протоколов s и t, просто соединяя их в указанном порядке. Например,

< мон, шок >^< мон > = < мон, шок, мон >.

Самые важные свойства конкатенации — это ее ассоциативность и то, что пустой протокол <> служит для нее единицей:

L1. s ^<> = <>^ s.

L2. s ^(t^u) = (s ^ t) ^u.

Пусть f — функция, отображающая протоколы в протоколы. Она называется строгой, если отображает пустой протокол в пустой протокол: f (<>) = <>.

Будем говорить, что функция f дистрибутивна, если f (s ^ t) = f (s)^ f (t).

Все дистрибутивные функции являются строгими.

Если n — натуральное число, то tⁿ будет обозначать конкатенацию n копий протокола t. Отсюда следует:

L3. t^{n +1}= t^tⁿ.

L4. (s^t) ^{n +1} = s^(t^s)ⁿ^t.

Сужение

Выражение (tА) обозначает протокол t, суженный на множество символов А; он строится из t отбрасыванием всех символов, не принадлежащих А.

Сужение дистрибутивно и поэтому строго.

L1. <> A = <>.

L2. (s ^ t) A = (sA)^(tA).

Эффект сужения на одноэлементных последовательностях очевиден:

LЗ. < х > А =< х >, если х А.

L4. < y > А =<>,если y А.

Приведенные ниже законы раскрывают взаимосвязь суженияи операций над множествами.

L5. s {} = <>.

L6. (sA) B = s (A B).

Голова и хвост

Если s — непустая последовательность, обозначим ее первый элемент s ₀, а результат, полученный после его удаления — s ’. Например, < x, y, х >₀ = x,< х, у, х >’ = y. Обе эти операции не определены для пустой последовательности.

L1. (< x >^ s)₀ = х.

L2. (< x >^ s)’ = s.

L3. s = (< s ₀>^ s ’), если s <>.

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

L4. s = t º (s = t = <> OR (s ₀ = t ₀ AND s’ = t’)).

Звёздочка

Множество А * — это набор всех конечных протоколов (включая <>), составленных из элементов множества А. После сужения на А такие протоколы остаются неизменными, Отсюда следует простое определение:

А* = { s | (sA) = s }.

Приведенные ниже законы являются следствиями этого определения:

L1. <> А*.

L2. < x > А* º x А.

L3. (s ^ t) А* ºs А* AND t А*.

Они обладают достаточной мощностью, чтобы определить, принадлежит ли протокол множеству А *. Например, если х А, а y А, то

<x, y> А*º (< x >^< y >) А*

º( <x> А*) AND ( <y> А*) по L 3

º T AND F = F по L 2.

Порядок

Если s — копия начального отрезка t, то можно найти такое продолжение и последовательности s, что s^и = t. Определим отношение порядка

s t = ($ u.s^и = t)

и будем говорить, что s является префиксом t. Например:< х, у > < х, у, z >. Отношение является частичным упорядочением и имеет своим наименьшим элементом <>. Об этом говорят законы

L 1. <> s наименьший элемент.

L 2. s s рефлексивность.

L 3. s t AND t s t = s антисимметричность.

L 4. s t AND t u s u транзитивность.

Следующий закон вместе с L 1 позволяет определить, является ли справедливым отношение s t:

L 5. (<x>^ s) t ºt <> AND x= t ₀ AND s t’.

Будем говорить, что функция f из множества протоколов во множество протоколов монотонна, если она сохраняет отношение порядка , т. е. f (s) f (t) всякий раз, когда s t.

Длина

Длину протокола t будем обозначать # t. Например, #< х, у, z > = 3.

Следующие законы определяют операцию #:

L 1. #<> = 0.

L 2. #<x> = 1.

L 3. #(s ^ t) = # s + # t.

Число вхождений символа х в протокол s определяется как:

s ¯ х = #(s { х }).

 

Протоколы процесса

 

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

Пример 3.11. Единственным протоколом процесса СТОП является <>:

протоколы (СТОП) = {<>}.

Пример 3.12. протоколы (ЧАСЫ) = {<>, < тик >, < тик, тик >,…} = { тик }^*. Здесь множество протоколов бесконечно.

Законы

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

L 1. протоколы (СТОП) = { t | t = <>} = {<>}.

Протокол процесса (с Р) может быть пустым, поскольку <> является протоколом поведения любого процесса до момента наступления его первого события.

L 2. протоколы (с Р) = { t | t = <> OR (t ₀ = c AND t' протоколы (Р))}

= {<> {< c >^ t | t протоколы (Р)}.

Эти два закона можно объединить в один общий закон, которому подчиняется конструкция выбора:

L 3. протоколы (x: B Р (x)) =

= { t | t = <> OR (t ₀ В AND t' протоколы (Р (t₀)))}.

Несколько сложнее найти множество протоколов рекурсивно определенного процесса, который является решением уравнения Х = F (Х).

L 4. протоколы (m Х: А.F (Х)) = _{n ³0} протоколы (Fⁿ (СТОП_A)).

Пример 3.13. протоколы (ТАП) = _{n ³0} { s | s < мон, шок > ⁿ }.

Доказательство.

1) Согласно предположению индукции

протоколы (Fⁿ (ТAП)) = { t | t < мон, шок > ⁿ },

где F (X) = (мон шок X).

2) протоколы (F ⁰(СТОП)) = {<>} = {s | s < мон, шок >⁰}, для n = 0 предположение выполняется.

3) Покажем, что предположение также справедливо для n +1:

протоколы (F^{n +1}(СТОП)) = протоколы (мон шок Fⁿ (СТОП)) =

= {<>, < мон >} {< мон, шок >^ t | t протоколы (Fⁿ (СТОП))} =

= {<>, {< мон >} {< мон, шок >^ t | t < мон, шок > ⁿ } =

= { s | s = <> OR s = < мон > OR $ t. s = < мон, шок >^ t AND t < мон, шок > ⁿ }

= { s | s < мон, шок > ^{n +1}}.

Справедливо, что <> является протоколом любого процесса до момента наступления его первого события. Кроме того, если (s ^ t) – протокол процесса до некоторого момента, то s должен быть протоколом того же процесса до некоторого более раннего момента времени. Наконец, каждое происходящее событие должно содержаться в алфавите процесса. Три этих факта находят свое формальное выражение в следующих законах:

L 5. <> протоколы (P).

L 6. s ^ t протоколы (P) s протоколы (P).

L 7. протоколы (P) {a P }^*.

После

Если s протоколы (P), то P/s (P после s) – это процесс, ведущий себя так, как ведет себя Р с момента завершения всех действий, записанных в протоколе s. Если s не является протоколом P, то P/s не определено.

Пример 3.14.( ТАП / <мон>) = (шок → ТАП).

Спецификации

 

Спецификация изделия – это описание его предполагаемого поведения. Это описание представляет собой предикат, содержащий свободные переменные, каждая из которых соответствует некоторому обозримому аспекту поведения изделия.

Например, спецификация электронного усилителя с входным диапазоном в один вольт и с усилением входного напряжения приблизительно в 10 раз задается предикатом

УСИЛ 10 = (0 v 1 | v ' - 10 v | 1).

В этой спецификации v обозначает входное, а v' - выходное напряжения.

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

Пример 3.15. Владелец торгового автомата не желает терпеть убытков. Поэтому он оговаривает, что число выданных шоколадок не должно превышать числа опущенных монет:

НЕУБЫТ = (#(пр { шок }) #(пр { мон })) = пр ¯ шок пр ¯ мон.

Пользователь автомата хочет быть уверенным в том, что машина не будет поглощать монеты, пока не выдаст уже оплаченный шоколад:

ЧЕСТН = (пр ¯ мон (пр ¯ шок + 1)).

Изготовитель торгового автомата должен учесть требования, как владельца, так и клиента:

ТАПВЗАИМ = ТАПНЕУБЫТ AND ЧЕСТН = (0 (пр ¯ мон – пр ¯ шок) 1).

---

Дата добавления: 2015-12-20; просмотров: 26; Мы поможем в написании вашей работы!

Поделиться с друзьями:

---

---

Мы поможем в написании ваших работ!