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