15 / 18
Метод построения абстрактных моделей, используемых для верификации протоколов…
ISSN 0236-3933. Вестник МГТУ им. Н.Э. Баумана. Сер. Приборостроение. 2017. № 1
63
Отображение
2
2
2
:
concrete
abstract
Transs Ruless
Ruless
определено следующим
образом:
2
0
0
2,1 2,2
,
,
,
Transs rsc rsa c c c
2
0
2 2,1 2,2
,
\
,
.
Transs rsc
c C c c
Таким образом,
Α
,
i
i
если
i
и порождено действием
2,1
!
c v
или
i
и порождено действием
2,2
! ,
c v
Α
i
в противном случае.
В соответствии с абстрактными преобразованиями, отображение
2
2
2
:
concrete
abstract
Transr Rulesr
Rulesr
такое, что, во-первых,
2
,
i
i
Transr rrc rra
1, 2.
i
Выполнимость посылок правил абстрактной системы при выполнимо-
сти посылок соответствующих правил исходной системы показывается анало-
гично, как и в случае 2.1. Во-вторых,
2
,
2.
i
Transr rrc
i
Для случая
2
i
правило в исходной системе описывает переход между двумя состояниями с
одинаковыми пометками (переменная
х
является локальной переменной графа
i
PG
системы
CS
:
),
i
x Vstate
которые в абстрактной системе объединяются в
одно. Это означает, что значение переменной
х
в состоянии
1
( )
m
f s
является
таким же, как и значение
х
в состоянии
1
,
m
s
в тех случаях, когда
x
входит в
множество
.
AP
V
Случай 2.3:
3
.
c C
Элемент множества правил исходной системы
3
{ |0
}
concrete
i
Rulesr
rrc
i n
имеет вид (5). Элемент множества правил абстракт-
ной системы
3
|0 3 :
abstract
i
Rulesr
rra i
: ?
1
0
3
0
3
,
|
( ( ))
0
( ) ... ,
, , , , ,
,
, , , , ,
,
abs
g c x
i
i
abs abs
abs
abs
abs
k
i
i
abs abs
i
abs abs
l
l
g
len c k
c v v
rra
l
l
l
l
l
l
где
1
:
abs
abs
x v
и
2
:
.
abs
abs
k
c v v
Выполнимость условия
1
0
abs
abs
k
len
c
k
c v v
в абстракт-
ной модели следует из выполнимости соответствующего условия исходной мо-
дели, так как переход, помеченный оператором отправки сообщения по этому
каналу от единственного отправителя, также присутствует и в абстрактной мо-
дели, и выполнение этого условия осуществимо только при возможности такого
перехода. Это доказывается рассмотрением для случая отправки сообщения по
каналу
3
c C
функции из множества правил исходной системы во множество
правил абстрактной системы (аналогично случаям 2.1 и 2.2).
Отображение
3
3
:
concrete
abstract
Transr Rulesr
Rulesr
определено следующим об-
разом:
3
,
0,1,2,
i
i
Transr rrc rra i
3
3
, 2.
i
Transr rrc rra i
Следовательно, пе-
реходу исходной системы, порожденному считыванием сообщения из канала
3
,
c C
в абстрактной системе всегда соответствует переход, порожденный анало-
гичным считыванием, и значение переменной
х
в состоянии
1
( )
m
f s
является та-
ким же, как и значение
х
в состоянии
1
,
m
s
в тех случаях, когда
x
входит в
.
AP
V
Отметим, что переходы, вызванные наличием в графах программ ребер с мет-
ками
goto
и их эквивалентами, не изменяют пометку состояния и сохраняются в
графах программ абстрактной системы. Таким образом, для всех возможных видов