11 / 18
Метод построения абстрактных моделей, используемых для верификации протоколов…
ISSN 0236-3933. Вестник МГТУ им. Н.Э. Баумана. Сер. Приборостроение. 2017. № 1
59
Элемент множества правил абстрактной системы
{ |0 3}
abstract
i
Rulesi
ria i
имеет вид
:
0
3
1
0
3
,
|
,
( )
, , , , ,
,
( )
, , , , ,
,
abs abs
abs
g
i
i
abs abs
abs
i
m
i
abs abs
m
i
abs abs
l
l
g
ria
f s
l
l
l
f s
l
l
l
где
,
.
abs
abs abs
Effect
Рассмотрим функцию
:
.
concrete
abstract
Transi Rulesi
Rulesi
Абстрактные пре-
образования построены так, что
,
0,1, 2,
i
i
Transi ric ria i
3
1
, 2
) ( ,
i
m
m
Transi ric ria i
L s
L s
1
, 2
) ( .
i
m
m
Transi ric
i
L s
L s
Покажем, что если посылка правила системы
CS
выполнима, то посылка
соответствующего правила системы
abs
CS
также выполнима.
В исходной системе имеем условие
,
,
g
причем согласно ограничени-
ям на модель в
g
не входят логические утверждения относительно каналов. В
соответствии с индуктивной гипотезой в состоянии
m
f s
выполняется
:
.
AP abs
abs
v V
v
v dom v
(4)
В то же время, защиту
g
можно представить в виде конъюнкции
1
2
,
g A A
где
1
,
,
AP
A Cond V C
2
,
.
AP
A Cond V C
В соответствии с абстрактными пре-
образованиями
1
abs
g
A true
, т. е. часть
2
,
AP
A Cond V C
заменена истиной.
Таким образом, защита
abs
g
является логическим следствием защиты
.
g
С учетом
вида
,
g
abs
g
и соотношения (4) следует, что
(( , ) |
) (( ,
) |
).
abs abs
abs
g
g
Действие
может быть присваиванием или выражением. Если
— при-
сваивание, то в соответствии с абстрактными преобразованиями получим:
–
,
abs
если
1
( ) ( ),
m
m
L s
L s
т. е. имеем соответствующий переход
1
abs
m
m
f s
f s
в абстрактной системе, вследствие чего
1
abs
m
L f s
1
.
m
L s
–
,
abs
если
1
( ) ( )
m
m
L s
L s
, т. е. в абстрактной системе два состояния
исходной системы
1
m
s
и
m
s
с одинаковыми пометками объединяются в одно.
Заключаем, что в
abs
TS
достижимо состояние
1
.
m
m
f s
f s
Если
— выражение, то применение соответствующего правила не изменя-
ет пометку состояния (что имеет место и в исходной системе), а дает переход в
системе
abs
TS
с более слабым условием, поскольку
,
abs
a
аналогично защи-
там
g
и
.
abs
g
Случай 2.
Получение значения по каналу
,
0
c Chan cap c
и присваивание
его переменной
.
x
Случай 2.1:
1
.
c C
Элемент множества правил исходной системы
1
{ |0
}
concrete
i
Rulesr
rrc
i n
имеет вид