Формальный логический анализ корректности спецификаций сетевых SIP-протоколов
Авторы: Девятков В.В., Мьё Т.Н.
Опубликовано в выпуске: #11(23)/2013
DOI: 10.18698/2308-6033-2013-11-999
Раздел: Информационные технологии | Рубрика: Компьютерные системы и сети
В статье для проверки правильности и корректности описания SIP-спецификаций (Session Initiation Protocol) в отличие от известных работ предлагается использовать значительно более выразительный, хорошо структурированный и как формальная система более развитой вариант языка, основанный на моделях взаимодействующих последовательностных процессов (п-исчислений). Спецификации должны удовлетворять определенным свойствам, которые описываются на языке временной модальной логики. Поиск ошибок предлагается осуществлять не с помощью генерации трасс, а с помощью доказательства наличия указанных формальных свойств. Ошибкой предлагается считать отсутствие таких свойств. Процессные модели позволяют гораздо более четко и полно классифицировать и описывать типы ошибок. В качестве инструментария для поиска ошибок предлагается использовать язык логического программирования ПРОЛОГ, что является гораздо более изящным и не имеющим ограничений подходом к проверке правильности и корректности спецификаций.
Литература
[1] Rosenberg J., Schulzrinne H., Camarillo G., Johnston A. Session Initiation Protocol (SIP). IETF Network Working Group Request. for Comments 3261, 2002
[2] Rosenberg J., Schulzrinne H. Reliability of provisional responses in Session Initiation Protocol (SIP). IETF Network Working Group Request. for Comments 3262, 2002
[3] Bishop S., Fairbairn M., Norrish M., Sewell P., Smith M., Wansbrough K. Rigorous specification and conformance testing techniques for network protocols, as applied to TCP, UDP and sockets. Proc. SIGCOMM’05. ACM, 2005, August
[4] Zave P. Understanding SIP Through Model-Checking. Proc. of the 2nd International Conference of Principles, Systems and Applications of IP Telecommunications. Springer-Verlag, 2008, vol. 5310, pp. 256-279
[5] Holzmann G.J. The Spin Model Checker: Primer and Reference Manual. Addison-Wesley, 2004, 596 p.
[6] Девятков В.В., Сидякин И.М. Мультиагентная система анализа телеметрической информации. Вестник МГТУ им. Н.Э. Баумана, Сер. Приборостроение, 2005, № 4 (61), с. 56-85
[7] Девятков В.В. Построение, оптимизация и модификация процессов. Вестник МГТУ им. Н.Э. Баумана. Сер. Приборостроение, 2012, № 4, с. 60-79
[8] Chellas B.F. Modal Logic an Introduction. The Press Syndicate of the University of Cambridge, 1980, 295 p.
[9] Gabbay D., Hodkinson I., Reynolds M. Temporal Logic: mathematical foundi-tions and computational aspects, vol. 1. Clarendon Press, Oxford, 1994