Выполнена автоматизация проверки правильности спецификаций протоколов инициирования сеансов как мультиагентной системы, представляемой процессными моделями и описанием требований их правильности на языке временной модальной логики. Автоматизацию проверки правильности спецификаций предложено осуществлять логическими программами, получаемыми с помощью предлагаемой методики перехода от процессной модели описания спецификации и требований правильности на языке модальной логики к логической программе проверки правильности на языке логического программирования ПРОЛОГ. Развиты принципы перехода от процессных моделей SIP-спецификаций к логической программе до детальной методики получения всех необходимых разделов логической программы. Методика проиллюстрирована примером логической программы для случая двух взаимодействующих агентов: пользовательского и сервисного.
