РУсскоязычный Архив Электронных СТатей периодических изданий
Инженерный журнал: наука и инновации/2013/№ 11/

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

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

Авторы
Тэги
Тематические рубрики
Предметные рубрики
В этом же номере:
Резюме по документу**
Формальный логический анализ корректности спецификаций сетевых SIP-протоколов УДК 004.413 Формальный логический анализ корректности спецификаций сетевых SIP-протоколов В.В. Девятков, Т.Н. Мьё МГТУ им. <...> Спецификации должны удовлетворять определенным свойствам, которые описываются на языке временной модальной логики. <...> В качестве инструментария для поиска ошибок предлагается использовать язык логического программирования ПРОЛОГ, что является гораздо более изящным и не имеющим ограничений подходом к проверке правильности и корректности спецификаций. <...> Ключевые слова: последовательностный процесс, пользовательский агент, язык временной модальной логики, протокол инициирования сеанса, язык логического программирования ПРОЛОГ. <...> При таком описании как пользовательский агент UAC на стороне клиента (user agent on the client side), так и пользовательский агент UAS на стороне сервера (user agent on the server side) моделируются своим последовательностным процессом. <...> 2 Формальный логический анализ корректности спецификаций сетевых SIP-протоколов Настоящая статья организована следующим образом. <...> 4 Формальный логический анализ корректности спецификаций сетевых SIP-протоколов Так, для графа переходов, приведенного на рис. <...> В настоящей статье, как и в работе [2], модели могут содержать множество пользовательских агентов на стороне клиентов UAC и множество пользовательских агентов на стороне серверов UAS. <...> Для иллюстрации описания поведения простой процессной модели воспользуемся парой агентов UAC и UAS, взятой из работы [2], и сначала опишем их поведение на языке графов, а затем на языке процессных выражений. <...> Агенты являются параллельно выполняющимися последовательностными процессами UAC и UAS, образующими в совокупности процесс PUAC UAS . <...> Процессы UAC и UAS взаимодействуют по 10 каналам, имена которых ackc, brpc, irpc, reqc, sakc, acks, brps, irps, reqs, saks. <...> Каналы ackc, brpc, irpc, reqc, sakc являются входными для процесса UAС и выходными для процесса UAS, а каналы acks, brps, irps, reqs, saks, наоборот <...>
** - вычисляется автоматически, возможны погрешности

Похожие документы: