I have created a formal model of invite dialogs in SIP. The primary purpose of this model is to bring together information from multiple RFCs in a document that is centralized, unambiguous, and analyzable.
The formal language, Promela, is the input language for the model-checker Spin. The UAC and UAS are two finite-state machines sending messages to each other through queues. Promela is used in a straightforward style that is easy to understand. http://www.research.att.com/~pamela/sip.html contains three versions of the model and a paper "Understanding SIP through model-checking" that explains the work in detail. The page also contains the results of analysis. The accompanying notes explain 6 small problems in the RFCs and the workarounds I have used. This material is made freely available for the benefit of the SIP community. Questions, comments, corrections and other feedback are welcomed. Pamela Zave
_______________________________________________ Sip mailing list https://www.ietf.org/mailman/listinfo/sip This list is for NEW development of the core SIP Protocol Use [EMAIL PROTECTED] for questions on current sip Use [EMAIL PROTECTED] for new developments on the application of sip
