5 / 10
примере проверки единственного условия правильности, называемого
условием правильного окончания. Для остальных условий проверки
правильности процедуры перехода, за исключением несущественных
отличий, аналогичны.
На языке модальной логики условие правильного окончания вы-
глядит следующим образом:
tu
[
ϕ
uac
(
x
1
s
!
y
1
.uac
?
startuac
)
⊃ ♦
ξ
uac
(
v
1
s
!
w
1
.uac
?
enduac
)
∧
,
ϕ
uas
(
x
2
s
?
y
2
.uas
?
startuas
)
⊃ ♦
ξ
uas
(
v
2
s
?
w
1
.uas
!
enduas
)
∧
,
ϕ
uac
(
p
1
s
!
q
1
. r
1
c
?
t
1
)
⊃
ϕ
uas
(
p
1
s
?
q
1
. r
2
c
!
t
2
)
∧
,
ϕ
uas
(
r
2
c
?
t
2
.u
1
s
!
s
1
)
⊃
ϕ
uac
(
u
1
s
?
s
1
. r
3
c
?
t
3
)]
.
Здесь
ϕ
uac
(
x
1
s
!
y
1
.uac
?
startuac
)
, ξ
uac
(
v
1
s
!
w
1
.uac
?
enduac
)
,
ϕ
uas
(
x
2
s
?
y
2
.uas
?
startuas
)
, ξ
uas
(
v
2
s
?
w
1
.uas
!
enduas
)
,
ϕ
uac
(
p
1
s
!
q
1
. r
1
c
?
t
1
)
, ϕ
uas
(
p
1
s
?
q
1
. r
2
c
!
t
2
)
,
ϕ
uas
(
r
2
c
?
t
2
.u
1
s
!
s
1
)
, ϕ
uac
(
u
1
s
?
s
1
. r
3
c
?
t
3
)
— предикаты, истинные, если в каналы
startuac, enduac, startuas,
enduas
поступают соответствующие восприятия или реакции и кана-
лы
reqc, reqs, irps,brps,brpc
правильно взаимодействуют.
Далее на примере условия правильного окончания рассмотрим, как
формируется на языке VISUAL PROLOG конкретная логическая про-
грамма его проверки.
Переходом из состояния
b
i
в состояние
b
j
в результате выполнения
условия перехода
c
1
?
a.c
2
!
a
называется тройка (
b
i
, c
1
?
a.c
2
!
a, b
j
). Путем
на графе, ведущем из состояния
b
i
в coстояние
b
j
, называется по-
следовательность переходов, ведущих из состояния
b
i
в состояние
b
j
.
Если из состояния
b
i
ведет какой-либо путь в состояние
b
j
, то будем
говорить, что состояние
b
j
достижимо из состояния
b
i
этим путем.
Состояние
b
i
, с которого начинается выполнение процесса, предста-
вленного тем или иным процессным графом переходов, называется
начальным состоянием графа, а состояние
b
j
, в котором выполнение
процесса завершается, называется конечным состоянием.
Переход от процессного графа переходов и условий правильно-
сти SIP-спецификаций к логической программе в языке VISUAL
PROLOG.
Анализ правильности SIP-спецификаций описания прото-
колов с помощью логических программ на языке логического програм-
мирования VISUAL PROLOG сводится к поиску свойств процессных
графов переходов, наличие которых гарантирует правильность SIP-
спецификаций. Например, это может быть наличие путей, которые
должны иметь свойства определенного рода, исключающиe некоррект-
ности.
В синтаксисе VISUAL PROLOG каждое состояние
b
i
представляет-
ся константой
bi
. Переменные, областью значений которых являются
ISSN 0236-3933. Вестник МГТУ им. Н.Э. Баумана. Сер. “Приборостроение”. 2015. № 2 111