Формальный логический анализ корректности спецификаций сетевых 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, наоборот <...>
** - вычисляется автоматически, возможны погрешности
Похожие документы:
РУАЭСТ (RUAEST)