Герб МГТУ им. Н.Э. БауманаНаучно-техническая библиотека МГТУ им. Н.Э. Баумана
Калужский филиал

Подробное описание документа

   Статья в журнале

Девятков В. В., Мьё Т. Н.
   Формальный логический анализ корректности спецификаций сетевых SIP-протоколов / Девятков В. В., Мьё Т. Н. - DOI 10.18698/2308-6033-2013-11-999 // Инженерный журнал: наука и инновации. - 2013. - № 11. - П.Н. 55.

library.bmstu.ru/Catalog/Details/599559

В статье для проверки правильности и корректности описания SIP-спецификаций (Session Initiation Protocol) в отличие от известных работ предлагается использовать значительно более выразительный, хорошо структурированный и как формальная система более развитой вариант языка, основанный на моделях взаимодействующих последовательностных процессов (п-исчислений). Спецификации должны удовлетворять определенным свойствам, которые описываются на языке временной модальной логики. Поиск ошибок предлагается осуществлять не с помощью генерации трасс, а с помощью доказательства наличия указанных формальных свойств. Ошибкой предлагается считать отсутствие таких свойств. Процессные модели позволяют гораздо более четко и полно классифицировать и описывать типы ошибок. В качестве инструментария для поиска ошибок предлагается использовать язык логического программирования ПРОЛОГ, что является гораздо более изящным и не имеющим ограничений подходом к проверке правильности и корректности спецификаций.