Understanding SIP through Model-Checking

"Understanding SIP through model-checking" (Pamela Zave; 2nd International Conference on Principles, Systems and Applications of IP Telecommunications, LNCS 5310, 2008) reports on an early project to build Promela models of SIP, and to verify them with the Spin model checker. These are the first formal models of this important application protocol. The following models and analysis results are an updated and corrected version of the models and results presented in the paper:

• basicraw.pml is a basic model of invite dialogs in SIP, with some restrictions in scope.
• transraw.pml is a model of invite dialogs in SIP, assuming exactly one TCP connection for transactions initiated by the caller UA, and exactly one for transactions initiated by the callee UA.
• fiforaw.pml is like the basic model, except that signaling is constrained to be FIFO (in other words, there is exactly one TCP connection per invite dialog).
• basicread.pml, transread.pml, and fiforead.pml are more readable versions of their respective raw models. Unreachable code and assertions used only to check reachability have been removed.
• basiccheck.txt, transcheck.txt, and fifocheck.txt are analytic results for their respective models. They contain the output of the Spin model checker.
• summary.txt summarizes the analytic results in a table, so that the models can be compared.
• notes.txt contains notes referred to in the models.

More recently, in "Specification and evaluation of transparent behavior for SIP back-to-back user agents" (Gregory Bond, Eric Cheung, Thomas Smith, and Pamela Zave; 4th International Conference on Principles, Systems and Applications of IP Telecommunications, ACM SIGCOMM, 2010), we developed a new model of invite dialogs and a model of transparent B2BUA behavior. This important property of SIP servers has never been defined before. In addition to verifying these models with Spin, we also altered Spin to generate comprehensive test suites automatically. The paper is based on the following models:

• ua.pml is an improved model of invite dialogs in SIP. It is more complete than the previous model in that it includes UA failures, and less complete than the previous model in that it does not include update requests and reliable provisional responses.
• The model above is not executable by itself. The executable driver is rundialog.pml, which includes ua.pml.
• b2bua.pml is a model of a transparent B2BUA, running in the context of two UAs.
• modb2bua.pml is a modified version that is more compatible with the behaviors of some SIP Servlet containers, as explained in the paper.