Формальный логический анализ корректности спецификаций сетевых SIP-протоколов
3
Настоящая статья организована следующим образом. В разделе 1
дается краткое описание модели последовательностных взаимодей-
ствующих процессов, используемой для SIP-спецификаций. Раздел 2
посвящен принципам процессного описания спецификаций. Раздел 3
представляет принципы перехода от процессного описания специфи-
каций к описанию на языке ПРОЛОГ и поиск ошибок в SIP-
спецификациях по описанию на этом языке.
1. Процессные модели.
Каждый процесс имеет алфавит восприя-
тий и реакций
A
= {
a
1
,
a
2
, ...,
a
m
}. Каждый символ
a
этого алфавита
именует некоторый объект, либо получаемый (воспринимаемый)
процессом из внешней среды (восприятие процесса), либо выдавае-
мый им во внешнюю среду (внешняя реакция процесса), либо ис-
пользуемый для внутренних нужд (внутренняя реакция процесса).
Процессы действуют, воспринимая, порождая для внутреннего упо-
требления или выдавая наружу объекты с соответствующими имена-
ми. Для того чтобы различать типы действий, будем использовать
следующие обозначения:
?
a
— для восприятий; !
a
— для внешних
реакций;
b
— для внутренних реакций.
Нитью
*
a
будем называть кортеж (конечный или бесконечный)
действий
* 0 1 2
2 1
...
.
m m
a a a a a a
− −
=
Выполнением нити процессом
P
называется определенная последовательность выполнения ее дей-
ствий слева направо. Символом
е
обозначается
пустое действие
.
Нить, состоящая из единственного пустого действия, называется
пу-
стой нитью. Процессом
P
называется множество нитей
S
, которые
он может выполнять, а
поведением процесса
P
— порядок выполне-
ния множества этих нитей.
Введем следующие обозначения:
?
A
— множество всех восприятий некоторого процесса
P
, вклю-
чая пустое восприятие
?
e
;
!
A
— конечное множество всех внешних реакций процесса
P
,
включая пустую внешнюю реакцию
!
e
;
S
— множество всех нитей, выполняемых процессом
P
, таких что
*
? !
S А A
⊆ ×
, где
*
?
A
— множество всех нитей
*
?
a
в алфавите
?
A
(
*
?
a
— нить, состоящая только из восприятий (нить восприятий)
процесса
P
);
*
ϕ
— функция на множестве
*
?
A
, которая ставит в соответствие
каждой нити
*
*
? ?
a А
∈
внешнюю реакцию из множества
! .
A
Процесс
P
, выполняющий множество нитей
* *
*
? (? ) ,
a a S
ϕ ∈
бу-
дем обозначать
( ).
P S
Значение функции
*
ϕ
на тех нитях множества
*
? ,
А
на которых эта функция не определена, и на тех нитях, кото-
