Формальный логический анализ корректности спецификаций сетевых SIP-протоколов
1
УДК 004.413
Формальный логический анализ корректности
спецификаций сетевых SIP-протоколов
© В.В. Девятков, Т.Н. Мьё
МГТУ им. Н.Э. Баумана, Москва, 105005, Россия
В статье для проверки правильности и корректности описания SIP-спецификаций
(Session Initiation Protocol) в отличие от известных работ предлагается использо-
вать значительно более выразительный, хорошо структурированный и как фор-
мальная система более развитой вариант языка, основанный на моделях взаимо-
действующих последовательностных процессов (
π
-исчислений). Спецификации
должны удовлетворять определенным свойствам, которые описываются на языке
временной модальной логики. Поиск ошибок предлагается осуществлять не с по-
мощью генерации трасс, а с помощью доказательства наличия указанных фор-
мальных свойств. Ошибкой предлагается считать отсутствие таких свойств.
Процессные модели позволяют гораздо более четко и полно классифицировать и
описывать типы ошибок. В качестве инструментария для поиска ошибок предла-
гается использовать язык логического программирования ПРОЛОГ, что является
гораздо более изящным и не имеющим ограничений подходом к проверке правиль-
ности и корректности спецификаций.
Ключевые слова:
последовательностный процесс, пользовательский агент, язык
временной модальной логики, протокол инициирования сеанса, язык логического
программирования ПРОЛОГ.
Введение.
В последние годы протокол SIP (Session Initiation
Protocol) стал широко применяться для IP-мультимедиауслуг, вклю-
чая обмен мультимедийным содержимым (видео- и аудиоконферен-
ции, мгновенные сообщения, онлайн-игры). Стандарт SIP описан во
многих источниках [1, 2]. В модели взаимодействия открытых систем
SIP является сетевым протоколом прикладного уровня. Однако до-
кументация, имеющаяся по протоколу, плохо структурирована, не-
формальна и неполна, что затрудняет ее использование как средства
проверки корректности конкретных приложений SIP.
Для выхода из этой ситуации необходимо формализовать описа-
ние функционирования приложений с помощью соответствующих
моделей, позволяющих проводить формально проверку корректности
(правильности) функционирования. Имеется достаточно много работ,
посвященных решению этой проблемы.
Так, в работе [3] для формальной спецификации протоколов TCP,
UDP и их приложений предлагается использовать
язык логики преди-
катов высоких порядков
, порождая на основе этого языка необходи-
