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