For checking the validation and correctness of the SIP specification (Session Initiation Protocol) in contrast to the well-known work it is proposed in the article to describe the specifications in much expressive, well-structured and theoretically, as a formal system, a more advanced version of the language, based on the models of interacting sequential processes (п-calculus). Specifications must satisfy certain properties, which in contrast to well-known works are described formally in the language of temporal modal logic. Finding errors is proposed not by generating routes, as it was done in the prior art, and with the evidence of formal properties described in the language of modal logic. If such property is not provided, then there may be an error. Process models provide much more clear and full description and classification of error types. As a tool for finding errors is proposed to use a logic programming language PROLOG, which is more elegant, full and unfettered approach and validate the correctness of the specifications.