4 / 10
Рис. 2. Процессный граф переходов процесса
UAS
reqs!invite
и восприятия
uac?start
или, иными словами, переход со-
вершается в результате выполнения условия
reqs!invite.uac?start
. Если
процессный граф
UAC
находится в состоянии
Inviting
, то при вы-
полнении условия
brps!byersp.invalidc?assertf
он остается в том же
состоянии, при выполнении условия
irps!invsucc.ackc?ack
переходит
в состояние
Confirming
, а при выполнении условий
irps!invfail
или
reqs!bye.brpc?byersp
переходит в состояние
PreEnding
. Описания пере-
ходов из остальных состояний графа переходов на рис. 1 и 2 аналогич-
ны приведенному описанию переходов для состояний
Uас
и
Inviting
.
Условия правильного поведения агентов, представленных про-
цессными графами переходов.
В работе [2] для проверки правильно-
сти SIP-спецификаций, представленных агентами, предлагается сна-
чала задать их процессными графами переходов или процессными
выражениями, а затем сначала сформулировать условия правильности
SIP-спецификаций как высказывания на языке временн ´ой модальной
логики, а затем — для реализации проверки правильности перейти к
логической программе на языке VISUAL PROLOG. В настоящей ста-
тье упор делается на принципы и процедуру перехода от процессных
графов переходов и полученных указанным образом условий правиль-
ности к логическим программам на языке VISUAL PROLOG, позво-
ляющим осуществлять проверку правильности. Всю эту процедуру
перехода к логической программе в настоящей статье изложим на
110 ISSN 0236-3933. Вестник МГТУ им. Н.Э. Баумана. Сер. “Приборостроение”. 2015. № 2