В.В. Девятков, Т.Н. Мьё
2
мые для того или иного протокола соответствующие формальные си-
стемы и методы доказательства корректности. Недостатки такого
подхода широко известны, в частности, из работ по искусственному
интеллекту: это трудноразрешимость или даже неразрешимость, вы-
числительная сложность, необходимость соответствующей квалифи-
кации пользователя, сложность описания функционирования прило-
жений и др.
Практически во всех описаниях протокола SIP его функциониро-
вание представляют как множество последовательностных парал-
лельно взаимодействующих процессов (агентов). При таком описа-
нии как пользовательский агент
UAC
на стороне клиента (user agent
on the client side), так и пользовательский агент
UAS
на стороне сер-
вера (user agent on the server side) моделируются своим последова-
тельностным процессом.
В ряде других работ предлагаются более простые модели описа-
ния взаимодействующих агентов. Так, в [4] для этой цели предлага-
ется использовать язык Promela. Авторы указанной работы полагают,
что этот язык удобен для спецификации SIP-приложений по двум
причинам. Во-первых, выразительные возможности языка в
наибольшей степени соответствуют описанию функционирования
как множества последовательностных параллельно взаимодейству-
ющих агентов, принятому в SIP. Во-вторых, описание на языке
Promela можно проверить на правильность с помощью специальных
программ проверки Spin [5].
В настоящей статье для проверки SIP-спецификаций также пред-
лагается использовать модель последовательностных взаимодей-
ствующих агентов, однако для описания спецификаций в отличие от
работы [4] предлагается применять значительно более выразитель-
ный, хорошо структурированный и теоретически, как формальная
система, более развитой вариант языка, основанный на моделях вза-
имодействующих последовательностных процессов (π-исчислении
[6]). Спецификации должны удовлетворять определенным свойствам,
описанным на языке временной модальной логики. Поиск ошибок
предлагается осуществлять не с помощью генерации трасс, как это
делается в работе [4], а с помощью доказательства наличия описан-
ных формальных свойств [6, 7]. Ошибкой предлагается считать от-
сутствие таких свойств. Процессные модели в дальнейшем будем
называть просто процессами. Процессы позволяют гораздо более
четко и полно классифицировать и описывать типы ошибок. В каче-
стве инструментария для поиска ошибок будем использовать язык
логического программирования ПРОЛОГ, что является гораздо более
изящным и не имеющим ограничений подходом к проверке правиль-
ности и корректности спецификаций.
