Инженерный журнал: наука и инновацииЭЛЕКТРОННОЕ НАУЧНО-ТЕХНИЧЕСКОЕ ИЗДАНИЕ
свидетельство о регистрации СМИ Эл № ФС77-53688 от 17 апреля 2013 г. ISSN 2308-6033. DOI 10.18698/2308-6033
  • Русский
  • Английский
Статья

Формальный логический анализ корректности спецификаций сетевых SIP-протоколов

Опубликовано: 18.11.2013

Авторы: Девятков В.В., Мьё Т.Н.

Опубликовано в выпуске: #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