7 / 11
как логического отрицания условий корректности. Как уже было отме-
чено, в настоящей статье изложены принципы и процедура перехода
от процессных графов переходов и полученных указанным образом
условий некорректности к логическим программам на языке VISUAL
PROLOG, позволяющим осуществлять проверку некорректностей. Та-
кую процедуру перехода рассмотрим на примере единственной некор-
ректности, называемой затенением. Для остальных некорректностей
процедуры перехода, за исключением несущественных отличий, ана-
логичны.
В работе [1] на языке модальной логики простейшее условие (пра-
вило), выполнение которого гарантирует отсутствие затенения пакета
p
, имеет вид
[(?
p
∧
!
accept
)
⊃ ¬♦
(?
p
∧
!
drop
)]
.
Смысл этого правила следующий: всегда, когда в каком-либо те-
кущем состоянии осуществляется восприятие пакета
p
, над которым
совершается действие !
accept
, тогда не должно быть достижимого из
этого состояния другого состояния, в которое процесс переходит в ре-
зультате восприятия того же пакета
p
, над которым совершается дей-
ствие
drop
. Наличие хотя бы одного затенения означает истинность
формулы
¬
( [(?
p
∧
!
accept
)
⊃ ¬♦
(?
p
∧
!
drop
)])
≡
♦¬
[(?
p
∧
!
accept
)
⊃ ¬♦
(?
p
∧
!
drop
)]
≡
♦
[
¬
((?
p
∧
!
accept
)
⊃ ¬♦
(?
p
∧
!
drop
))]
≡
♦
[
¬
(
¬
(?
p
∧
!
accept
)
∨ ¬♦
(?
p
∧
!
drop
))]
≡
♦
[(?
p
∧
!
accept
)
∧ ♦
(?
p
∧
!
drop
)]
,
т.е. в некотором текущем состоянии возможно восприятие пакета
p
,
над которым совершается действие
!
accept
, и в достижимом из этого
состояния другом состоянии, в которое процесс переходит в результате
восприятия того же пакета
p
, совершается действие
drop
.
По отношению к процессному графу это означает следующее: име-
ются два состояния
b
2 и
b
3, достижимые из начального состояния
b
1,
одно из которых, например
b
3, достижимо из состояния
b
2 и при
этом существуют переходы
(
b
2
,
?
p.
!
accept, b
i
)
,
(
b
3
,
?
p.
!
drop, b
j
)
. Такая
ситуация является, скорей всего, ошибкой, поскольку непонятно, чем
руководствовался автор процессного графа, указав, что на пути из на-
чального состояния в состояние
b
3 сначала можно попасть в состояние
b
2, при переходе из которого разрешено принять пакет
p
, а затем по-
пасть в состояние
b
3, при переходе из которого этот пакет принимать
запрещено.
Рассмотренное условие некорректности
♦
[(?
p
∧
!
accept
)
∧ ♦
(?
p
∧
!
drop
)]
сформулировано для одного и того же пакета. Именно
поэтому оно названо простейшим. На самом деле затенения могут
быть более сложными. Например, несколько пакетов могут затенять
106 ISSN 0236-3933. Вестник МГТУ им. Н.Э. Баумана. Сер. “Приборостроение”. 2015. № 1