Pamela,
This sounds interesting. I just skimmed the referenced web pages, and
didn't take time to understand the details of the formalism, so I
apologize if I have drawn the wrong conclusions.
I don't understand if the intent of this work is theoretical, or if it
is intended as basis for a real implementation. If the latter, then some
of the simplifying assumptions of your models probably need to be removed.
Of note, in many cases 3261 is less than clear, and some after the fact
interpretation of the intent has had to be done. (You may consider this
either discerning the intent of the Founders, or Judicial Activism, as
you prefer.) One area where this has been done is around dialogs. It
isn't entirely obvious, but is implicit in 3261+3265+3515 that you can
have both an invite + a subscription, or multiple subscriptions sharing
a dialog. RFC 5057 discusses this. In retrospect many people think it
was a mistake to allow this, but it *is* used, in some limited ways, and
probably cannot be removed. So in general you must be prepared to handle
this. (Though you might be able to avoid it in some limited scope
servers.) My fundamental is the introduction of the term "dialog usage"
and its refinements: "invite dialog usage" and "subscribe dialog usage",
and the partitioning of these from the notion of "dialog" which they
share. I would think you should have the same partitioning in your models.
I then looked at your notes. I found it very interesting that through
formal means you have identified a number of race conditions. I gather
you are not aware of:
http://www.ietf.org/internet-drafts/draft-ietf-sipping-race-examples-06.txt
That document has been done without benefit of formal models. But it
appears that there is substantial agreement about the set of race
conditions. (I wish you had been around when we did that work.) That
document is largely done, so it is likely impractical to get your input
into it. But take a look. It has resolutions to most of the races. If
you find any errors, please speak up.
Thanks,
Paul
Pamela Zave wrote:
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
_______________________________________________
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
