[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Sip] INVITE dialogs

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 sip-implementors at cs.columbia.edu for questions on current sip
Use sipping at ietf.org for new developments on the application of sip