/* ======================================================================== DESCRIPTION The scope of this model is one invite dialog that passes through a B2BUA with transparent behavior. This model uses a formal definition of user agents according to the basic version of SIP as documented by RFC 3261, with the single addition of Info requests. The user agents are modeled at the level of the transaction user, so 100 messages, retransmissions, and acks sent in response to invite failures are not included. ======================================================================== */ /* ======================================================================== DEFINITION OF MESSAGE TYPES Requests invite ack cancel info bye Provisional Responses prov18x (a non-reliable 180, 181, or 182 response to an initial invite) dialog183 (a non-reliable 183 response to an initial invite) Final Responses ("DVR" stands for Dialog Vanished Response) inv200 (a 200 in response to an invite) invFail (any 3xx-6xx response to an invite except 408, 481, or 491) invDVR (a 408 or 481 response to an invite) inv491 (a 491 response to a re-invite) ackTimeout (a timeout generated by waiting for ack to initial invite) canc200 (a 200 in response to a cancel) cancDVR (a 408 or 481 response to a cancel) infoDVR (a 408 or 481 response to an info) infoRsp (any other response to an info, whether successful or failing) bye200 (a 200 in response to a bye) byeDVR (a 408 or 481 response to a bye) ======================================================================== */ mtype = { /* SIP messages */ invite, ack, cancel, info, bye, prov18x, dialog183, inv200, invFail, invDVR, inv491, ackTimeout, canc200, cancDVR, infoDVR, infoRsp, bye200, byeDVR, /* SIP dialog states */ initIn, initOut, inviting, invited, confirmed, reInvting, reInvted, byeing, byeed, ended, /* SDP types */ none, offer, answer, /* media states of a UA */ noFlow, offering, offered, flow } chan left1 = [7] of {mtype,mtype}; /* these are maximum queue sizes */ chan right1 = [7] of {mtype,mtype}; chan left2 = [7] of {mtype,mtype}; chan right2 = [7] of {mtype,mtype}; #include "ua.pml" proctype B2BUA(chan in1,out1,in2,out2) { mtype st1 = initIn; mtype st2 = initOut; bool dialog2 = false; /* dialog2 == true means that dialog2 has */ /* reached either a SIP early or SIP */ /* confirmed state */ bool initAcked1 = false; bool failed1, failed2 = false; /* If both UAs fail, at about the same time, the B2BUA is in */ /* danger of hanging. These flags are used to diagnose double */ /* failure and take appropriate action. */ mtype sdp; in1?invite,sdp; out2!invite,sdp; st1 = invited; st2 = inviting; Initiated: /* possible state pairs during Initiated phase */ /* invited inviting */ /* confirmed confirmed */ /* reInvting reInvted */ /* reInvted reInvting */ do :: in1?invite,sdp; assert((st1 == confirmed && st2 == confirmed) || (st1 == reInvting && st2 == reInvted)); if :: st1 == reInvting; out1!inv491,none /* reInvite race */ :: st1 == confirmed; st1 = reInvted; st2 = reInvting; out2!invite,sdp fi :: in1?ack,sdp; initAcked1 = true; out2!ack,sdp :: in1?cancel,sdp; assert((st1 == invited && st2 == inviting) || (st1 == confirmed && st2 == confirmed) || (st1 == reInvting && st2 == reInvted)); if :: st1 == invited; out1!canc200,none; out2!cancel,none /* cancel is piecewise */ :: st1 == confirmed || st1 == reInvting; out1!canc200,none /* cancel */ fi /* race */ :: in1?info,sdp; assert(dialog2); out2!info,none :: in1?bye,sdp; st1 = byeed; st2 = byeing; out2!bye,none; goto Terminated :: in1?prov18x,sdp; assert(false) :: in1?dialog183,sdp; assert(false) :: in1?inv200,sdp; assert(st1 == reInvting && st2 == reInvted); st1 = confirmed; st2 = confirmed; out2!inv200,sdp :: in1?invFail,sdp; assert(st1 == reInvting && st2 == reInvted); st1 = confirmed; st2 = confirmed; out2!invFail,sdp :: in1?invDVR,sdp; assert(st1 == reInvting && st2 == reInvted); st1 = confirmed; st2 = confirmed; failed1 = true; out2!invDVR,none :: in1?inv491,sdp; assert(st1 == reInvting && st2 == reInvted); st1 = confirmed; st2 = confirmed; out2!inv491,none :: in1?ackTimeout,sdp; initAcked1 = true; failed1 = true; out2!ackTimeout,none :: in1?canc200,sdp; assert(false) :: in1?cancDVR,sdp; assert(false) :: in1?infoDVR,sdp; assert(dialog2); failed1 = true; out2!infoDVR,none :: in1?infoRsp,sdp; assert(dialog2); out2!infoRsp,none :: in1?bye200,sdp; assert(false) :: in1?byeDVR,sdp; assert(false) :: in2?invite,sdp; assert((st1 == confirmed && st2 == confirmed) || (st1 == reInvted && st2 == reInvting)); if :: st2 == reInvting; out2!inv491,none /* reInvite race */ :: st2 == confirmed; st1 = reInvting; st2 = reInvted; out1!invite,sdp fi :: in2?ack,sdp; out1!ack,sdp :: in2?cancel,sdp; assert(false) :: in2?info,sdp; assert(dialog2); out1!info,none :: in2?bye,sdp; st1 = byeing; st2 = byeed; out1!bye,none; goto Terminated :: in2?prov18x,sdp; assert(st1 == invited && st2 == inviting); dialog2 = true; out1!prov18x,none :: in2?dialog183,sdp; assert(st1 == invited && st2 == inviting); dialog2 = true; out1!dialog183,sdp :: in2?inv200,sdp; assert((st1 == invited && st2 == inviting) || (st1 == reInvted && st2 == reInvting)); st1 = confirmed; st2 = confirmed; dialog2 = true; out1!inv200,sdp :: in2?invFail,sdp; assert((st1 == invited && st2 == inviting) || (st1 == reInvted && st2 == reInvting)); if :: st1 == invited; st1 = ended; st2 = ended; out1!invFail,none; goto end :: st1 == reInvted; st1 = confirmed; st2 = confirmed; out1!invFail,none fi :: in2?invDVR,sdp; assert((st1 == invited && st2 == inviting) || (st1 == reInvted && st2 == reInvting)); if :: st1 == invited; st1 = ended; st2 = ended; out1!invDVR,none; goto end :: st1 == reInvted; st1 = confirmed; st2 = confirmed; failed2 = true; out1!invDVR,none fi :: in2?inv491,sdp; assert(st1 == reInvted && st2 == reInvting); st1 = confirmed; st2 = confirmed; out1!inv491,none :: in2?ackTimeout,sdp; assert(false) :: in2?canc200,sdp /* cancel is piecewise */ :: in2?cancDVR,sdp; failed2 = true /* cancel is piecewise */ :: in2?infoRsp,sdp; assert(dialog2); out1!infoRsp,none :: in2?infoDVR,sdp; assert(dialog2); failed2 = true; out1!infoDVR,none :: in2?bye200,sdp; assert(false) :: in2?byeDVR,sdp; assert(false) :: failed1 && failed2; st1 = ended; st2 = ended; goto end od; Terminated: /* possible state pairs during Terminated phase */ /* byeing byeed */ /* byeed byeing */ /* An obsolete message or redundant termination message is handled */ /* piecewise rather than being propagated end-to-end. If the two UAs */ /* reach the termination phase in independent states, i.e., not in */ /* byeed/byeing or byeing/byeed, then cleanup proceeds independently on */ /* the two UAs. */ do :: in1?invite,sdp; out1!invFail,none /* no new requests */ :: in1?ack,sdp; /* no new requests */ :: in1?cancel,sdp; assert(false) :: in1?info,sdp; out1!infoRsp,none /* no new requests */ :: in1?bye,sdp; /* no new requests */ assert(st1 == byeing && st2 == byeed); out1!bye200,none :: in1?prov18x,sdp; assert(false) :: in1?dialog183,sdp; assert(false) :: in1?inv200,sdp; out2!inv200,sdp :: in1?invFail,sdp; out2!invFail,none :: in1?invDVR,sdp; out2!invDVR,none :: in1?inv491,sdp; out2!inv491,none :: in1?ackTimeout,sdp; out2!ackTimeout,none :: in1?canc200,sdp; assert(false) :: in1?cancDVR,sdp; assert(false) :: in1?infoDVR,sdp; out2!infoDVR,none :: in1?infoRsp,sdp; out2!infoRsp,none :: in1?bye200,sdp; assert(st1 == byeing && st2 == byeed); st1 = ended; st2 = ended; out2!bye200,none; goto end :: in1?byeDVR,sdp; assert(st1 == byeing && st2 == byeed); st1 = ended; st2 = ended; out2!byeDVR,none; goto end :: in2?invite,sdp; out2!invFail,none /* no new requests */ :: in2?ack,sdp /* no new requests */ :: in2?cancel,sdp; assert(false) :: in2?info,sdp; out2!infoRsp,none /* no new requests */ :: in2?bye,sdp; /* no new requests */ assert(st1 == byeed && st2 == byeing); out2!bye200,none :: in2?prov18x,sdp /* cannot propagate */ :: in2?dialog183,sdp /* cannot propagate */ :: in2?inv200,sdp; out1!inv200,sdp :: in2?invFail,sdp; out1!invFail,none :: in2?invDVR,sdp; out1!invDVR,none :: in2?inv491,sdp; out1!inv491,none :: in2?ackTimeout,sdp; assert(false) :: in2?canc200,sdp /* piecewise */ :: in2?cancDVR,sdp /* piecewise */ :: in2?infoDVR,sdp; out1!infoDVR,none :: in2?infoRsp,sdp; out1!infoRsp,none :: in2?bye200,sdp; assert(st1 == byeed && st2 == byeing); st1 = ended; st2 = ended; out1!bye200,none; goto end :: in2?byeDVR,sdp; assert(st1 == byeed && st2 == byeing); st1 = ended; st2 = ended; out1!byeDVR,none; goto end od; end: assert(st1 == ended && st2 == ended); endAbsorb: do :: in1?invite,sdp; assert(false) :: in1?ack,sdp :: in1?cancel,sdp; out1!cancDVR,none :: in1?info,sdp; out1!infoDVR,none :: in1?bye,sdp; out1!byeDVR,none :: in1?prov18x,sdp; assert(false) :: in1?dialog183,sdp; assert(false) :: in1?inv200,sdp :: in1?invFail,sdp :: in1?invDVR,sdp :: in1?inv491,sdp :: in1?ackTimeout,sdp; out2!ackTimeout,none :: in1?infoRsp,sdp :: in1?infoDVR,sdp :: in1?canc200,sdp; assert(false) :: in1?cancDVR,sdp; assert(false) :: in1?bye200,sdp :: in1?byeDVR,sdp :: in2?invite,sdp; assert(false) :: in2?ack,sdp :: in2?cancel,sdp; assert(false) :: in2?info,sdp; assert(false) :: in2?bye,sdp; assert(false) :: in2?prov18x,sdp :: in2?dialog183,sdp :: in2?inv200,sdp :: in2?invFail,sdp :: in2?invDVR,sdp :: in2?inv491,sdp :: in2?ackTimeout,sdp; assert(false) :: in2?infoDVR,sdp :: in2?infoRsp,sdp :: in2?canc200,sdp :: in2?cancDVR,sdp :: in2?bye200,sdp :: in2?byeDVR,sdp od } init { atomic { run callerUA(left1,right1); run B2BUA(right1,left1,left2,right2); run calleeUA(right2,left2) } } /* ======================================================================== ANALYSIS Spin Version 5.1.3 -- 11 December 2007) + Partial Order Reduction Full statespace search for: never claim - (not selected) assertion violations + cycle checks - (disabled by -DSAFETY) invalid end states + State-vector 128 byte, depth reached 74917, errors: 0 24634557 states, stored 24921508 states, matched 49556065 transitions (= stored+matched) 2 atomic steps hash conflicts: 23516611 (resolved) Stats on memory usage (in Megabytes): 3664.962 equivalent memory usage for states (stored*(State-vector + overhead)) 3277.429 actual memory usage for states (compression: 89.43%) state-vector as stored = 112 byte + 28 byte overhead 256.000 memory used for hash table (-w25) 4.578 memory used for DFS stack (-m100000) 4.074 memory lost to fragmentation 3533.933 total actual memory usage ======================================================================== */