Previous Page  9 / 18 Next Page
Information
Show Menu
Previous Page 9 / 18 Next Page
Page Background

Метод построения абстрактных моделей, используемых для верификации протоколов…

ISSN 0236-3933. Вестник МГТУ им. Н.Э. Баумана. Сер. Приборостроение. 2017. № 1

57

няется истиной. Если

1

2,1 2,2

3

,

,

C C c c

C

то

с

остается неизменным, иначе

с

заменяется истиной.

Абстрактные преобразования элементов множеств

.

i

Comm

Преобразо-

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

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

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

множества

.

AP

V

Однако для возможности проведения верификации на практи-

ке необходимо ограничивать емкость каналов и их число небольшими значени-

ями (3–4), что приводит к удалению некоторых операторов, изменяющих состо-

яние переменных из множества

.

AP

V

Соответственно, преобразование коммуникационных действий исходит из

следующих соображений. Если оператор приема сообщения не изменяет помет-

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

торов отправки сообщений. Если удаляется оператор отправки сообщения,

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

ку, то необходимы дополнительные меры. Разработанные преобразования и

принятые меры приведены в таблице.

Преобразование коммуникационных действий

Оператор в исходной модели

Оператор в абстрактной модели

Для

1

c C

 

!

c v v dom c

! ,

c v

если оператор находится в графах

1

,

PG

2

;

PG

,

если оператор находится в графе

3

PG

 

 

?

,

c x x Var dom x dom c

Недетерминированный выбор

Для

2

c C

 

!

c v v dom c

! ,

c v

если

2,1

c c

или

2,2

;

c c

,

если

2 2,1 2,2

\

,

c C c c

 

 

?

,

c x x Var dom x dom c

? ,

c x

если

2,1

c c

или

2,2

;

c c

,

если

2 2,1 2,2

\

,

c C c c

Для

3

c C

 

!

c v v dom c

!

c v

 

 

?

,

c x x Var dom x dom c

?

c x

Рассмотрим замену недетерминированным выбором. Если оператор

atomic

{

guard_abs -> c?x;

} находится в

0

,

PG

то он заменяется оператором неде-

терминированного выбора

if

:: atomic { guard_abs -> c?x; }

:: atomic { m.opc = opc

1

;

m.id

= ABS; }

:: atomic { m.opc = opc

k

;

m.id

= ABS; }

fi;