2 / 10
Протокол инициирования сеансов (Session Initiation Protocol (SIP)) —
это протокол, разработанный IETF (Internet Engineering Task Force) для
голосового интернет-протокола VOIP (Voice over Internet Protocol), а
также для передачи текста или мультимедиа данных, например, для
систем обмена мгновенными сообщениями, видео обмена, игр в реаль-
ном времени и др. Стандарт SIP описан во многих источниках [1–4].
В модели взаимодействия открытых систем SIP является сетевым
протоколом прикладного уровня. Однако документация, имеющаяся
по протоколу, плохо структурирована, неформальна и неполна, что
затрудняет ее использование как средства проверки правильности
спецификаций для конкретных приложений SIP.
В статье [2] для проверки SIP-спецификаций предлагается исполь-
зовать модель последовательностных взаимодействующих агентов, од-
нако для описания спецификаций, в отличие от работы [5], предлага-
ется применять значительно более выразительный, хорошо структу-
рированный и теоретически, как формальная система, более развитый
вариант языка, основанный на моделях взаимодействующих последо-
вательностных процессов (
π
-исчислений [6]).
Настоящая статья также посвящена проверке правильности SIP-
спецификаций по тем же принципам, которые изложены в статье
[2]. Однако в отличие от статьи [2] в настоящей статье упор делается на
изложение детальной методики перехода от процессных моделей опи-
сания SIP-спецификаций и условий их правильности, формулируемых
на языке модальной временн´ой логики, к конкретным логическим про-
граммам, реализующим проверку правильности SIP-спецификаций.
Принципы описания SIP-спецификаций графами переходов
процессов.
В настоящей статье, как и в работе [2], SIP-спецификации
создаются как множество пользовательских агентов на стороне кли-
ентов
UAC
(
User Agent Client
) и множество пользовательских агентов
на стороне серверов
UAS
(
User Agent Server
). Взаимодействие аген-
тов осуществляется с помощью обмена сообщениями. Каждый агент
является последовательностным процессом, параллельно функциони-
рующим с другими. Последовательные процессы в рамках настоящей
статьи для наглядности будем представлять графами переходов про-
цессов или процессными графами переходов, хотя, как показано в
статье [2], в случае процессов (агентов) большой размерности графо-
вое представление становится громоздким и вместо него используется
адекватное представление в виде процессных выражений.
В процессных графах переходов, описывающих SIP-спецификации,
каждое состояние графа изображается кружком, внутрь которого по-
мещается символьное обозначение состояния.
Для иллюстрации описания поведения агентов процессными гра-
фами воспользуемся парой простых агентов
UAC
и
UAS
, взятой из
108 ISSN 0236-3933. Вестник МГТУ им. Н.Э. Баумана. Сер. “Приборостроение”. 2015. № 2