Протокол инициирования сеансов связи является протоколом
сигнализации и предназначен для организации, модификации и
завершения сеансов связи. Для управления соединением в протоколе
используются транзакции. В статье рассмотрено функционирование
протокола SIP на уровне транзакций. Построена модель процедуры
управления соединением в SIP в форме раскрашенных сетей Петри и
выполнена её декомпозиция на функциональные подсети. Для
верификации корректности работы модели использованы инварианты
сетей Петри. Получено значительное ускорение вычислений инвариантов
при использовании метода декопмозиции.