Кафедра ИУ3
27 мая 2014, 14:00

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

Докладчик: Наунг М. Т.

Организация: МГТУ им. Н. Э. Баумана

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