Формальный логический анализ корректности спецификаций сетевых SIP-протоколов
7
процесс
Inviting
(подпроцесс процесса
UAC
). Это означает, что могут
выполняться следующие нити:
•
.
?
!
Inviting brps byeRsp assertF
процесса
Inviting
;
•
.
?
!
irps invSucc.ac
Inviti g
kc
n
ack
процесса
Confirming
;
•
Inviting.irps
?
invFail
,
.
?
!
reqs bye.brpc
In
b
viting
yeRsp
процесса
PreEnding
.
Inviting
reqc!invite
irps?invFail reqs?bye.brpc!byeRsp
|
irps?invSucc.ackc!ack
brps?byeRsp.invalid!assertF
Сonfirming
Byeing
reqs?bye.brpc!byeRsp
reqc!bye
irps?invFail
!
.invalid assertF
|
|
.invalid assertF
irps?invSucc
!
reqs?bye.brpc!byeRsp
brps?byeRsp
Ending
!endUac
PreEnding
irps?invFail!assertF
|
|
|
assertT
sp
assertF
irps?invSucc!
bye.brpc!byeR brps?byeRsp.
UAC
?startUac
irps?invFail.invalid!assertF|irps?invSucc.invalid
!assertF|brps?byeRsp.invalid!assertF
Рис. 2.
Граф переходов процесса
UAC
Проверка на выполнимость осуществляется в порядке записи ни-
тей в процессных выражениях слева направо. Если будет выполнена
нить процесса
Inviting
, то процесс проверки названных нитей начина-
ется сначала. Если будет выполнена какая-либо из нитей другого про-
цесса, то процесс
Inviting
прекращает свое выполнение и начинает вы-
полняться процесс, которому принадлежит выполнившаяся нить, и все
повторяется сначала, но уже для другого процесса.
Графы процессов не задают порядок выполнения нитей процессов.
Проверку выполнимости нитей в случае описания агентов графами пе-
реходов можно осуществлять либо в любом порядке, помня при этом,
что поведение агентов может быть неоднозначным, либо в порядке, все-
таки как-то заданном, например, за счет ортогональности выполнения
нитей. В рамках настоящей статьи будем полагать, что имеющиеся про-
цессные выражения всегда задают порядок выполнения нитей.
