/* ======================================================================== 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, canceling, 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 */ /* ended canceling */ /* 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; /* cancel is piecewise */ st1 = ended; st2 = canceling; out1!canc200,none; out1!invFail,none; out2!cancel,none :: 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) || (st1 == ended && st2 == canceling)); dialog2 = true; if :: st1 == invited; out1!prov18x,none :: else fi :: in2?dialog183,sdp; assert((st1 == invited && st2 == inviting) || (st1 == ended && st2 == canceling)); dialog2 = true; if :: st1 == invited; out1!dialog183,none :: else fi :: in2?inv200,sdp; assert((st1 == invited && st2 == inviting) || (st1==ended && st2==canceling) || (st1==reInvted && st2==reInvting)); if :: st2 == canceling; st2 = byeing; /* cancel race */ if :: sdp == answer; out2!ack,none :: sdp == offer; out2!ack,answer fi; out2!bye,none; goto Terminated :: st2 != canceling; st1 = confirmed; st2 = confirmed; dialog2 = true; out1!inv200,sdp fi :: in2?invFail,sdp; assert( (st1 == invited && st2 == inviting) || (st1 == ended && st2 == canceling) || (st1 == reInvted && st2 == reInvting)); if :: st1 == invited; st1 = ended; st2 = ended; out1!invFail,none; goto end :: st1 == ended; st2 = ended; goto end /* cancel is piecewise */ :: st1 == reInvted; st1 = confirmed; st2 = confirmed; out1!invFail,none fi :: in2?invDVR,sdp; assert( (st1 == invited && st2 == inviting) || (st1 == ended && st2 == canceling) || (st1 == reInvted && st2 == reInvting)); if :: st1 == invited; st1 = ended; st2 = ended; out1!invDVR,none; goto end :: st1 == ended; st2 = ended; goto end /* cancel is piecewise */ :: 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; /* cancel is piecewise */ assert(st1 == ended); if :: dialog2; st2 = byeing; out2!bye,none; goto Terminated :: else fi :: 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 */ /* ended 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 != byeed); if :: st1 == byeing; out1!bye200,none :: st1 == ended; out1!byeDVR,none fi :: 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; /* independent cleanup */ assert(st1 != byeed); if :: st1 == byeing && st2 == byeed; st1 = ended; st2 = ended; out2!bye200,none; goto end :: st1 == ended && st2 == byeing fi :: in1?byeDVR,sdp; /* independent cleanup */ assert(st1 != byeed); if :: st1 == byeing && st2 == byeed; st1 = ended; st2 = ended; out2!byeDVR,none; goto end :: st1 == ended && st2 == byeing fi :: 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(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; /* independent cleanup */ assert(st2 != byeed); if :: st1 == byeed && st2 == byeing; st1 = ended; st2 = ended; out1!bye200,none; goto end :: st1 == ended && st2 == byeing; st2 = ended; goto end fi :: in2?byeDVR,sdp; /* independent cleanup */ assert(st2 != byeed); if :: st1 == byeed && st2 == byeing; st1 = ended; st2 = ended; out1!byeDVR,none; goto end :: st1 == ended && st2 == byeing; st2 = ended; goto end fi 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 76162, errors: 0 24567400 states, stored 24399175 states, matched 48966575 transitions (= stored+matched) 2 atomic steps hash conflicts: 23228967 (resolved) Stats on memory usage (in Megabytes): 3654.971 equivalent memory usage for states (stored*(State-vector + overhead)) 3268.715 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.051 memory lost to fragmentation 3525.242 total actual memory usage ======================================================================== */