/* ======================================================================== FIFO MODEL OF INVITE DIALOGS IN SIP, WITH ALL ASSERTIONS Copyright AT&T Laboratories, Inc., 2008. For complete documentation of this model, see the paper "Understanding SIP Through Model-Checking," Pamela Zave, submitted for publication, 2008. DEFINITION OF MESSAGE TYPES Requests invite prack update ack (ack in response to a invSucc) cancel info bye Provisional Responses unProv (any unreliable 1xx in response to an invite) relProv (any reliable 1xx in response to an invite) Final Responses invSucc (any 2xx in response to an invite) invFail (any 3xx-6xx message in response to an invite) prackRsp (200(OK) in response to a prack) updSucc (200(OK) in response to an update) updFail (491 in response to an update) infoRsp (200(OK) in response to an info) byeRsp (200(OK) in response to a bye) MODEL CHECKING of fiforaw.pml For purposes of model-checking only, ... a UAS is limited to one unreliable provisional response, ... a UA is limited to one info request. (Spin Version 5.1.3 -- 11 December 2007) + Partial Order Reduction + Compression Full statespace search for: never claim - (not selected) assertion violations + cycle checks - (disabled by -DSAFETY) invalid end states + State-vector 88 byte, depth reached 1068, errors: 0 5494684 states, stored 3549171 states, matched 9043855 transitions (= stored+matched) 1 atomic steps hash conflicts: 6534429 (resolved) Stats on memory usage (in Megabytes): 607.856 equivalent memory usage for states (stored*(State-vector + overhead)) 243.856 actual memory usage for states (compression: 40.12%) state-vector as stored = 19 byte + 28 byte overhead 64.000 memory used for hash table (-w23) 0.458 memory used for DFS stack (-m10000) 308.188 total actual memory usage nr of templates: [ globals chans procs ] collapse counts: [ 274250 2365 5689 2 ] pan: elapsed time 38.2 seconds pan: rate 143877.56 states/second pan: avg transition delay 4.2228e-06 usec real 38.2 user 37.8 sys 0.3 ======================================================================== */ mtype = { /* SIP messages */ invite, prack, update, ack, cancel, info, bye, unProv, relProv, invSucc, invFail, prackRsp, updSucc, updFail, infoRsp, byeRsp, /* SDP types needed */ none, offer, answer, /* media states of a UA */ noFlow, offering, offered, flow } chan c2s = [7] of {mtype,mtype}; /* maximal queue length */ chan s2c = [8] of {mtype,mtype}; /* maximal queue length */ proctype UAC() { /* media state */ mtype media = noFlow; mtype sdp, bufsdp; /* state relevant to the inviting phase */ bool dialog = false; /* state relevant to the confirmed phase (at most one is true) */ bool reInviting = false; bool reInvited = false; /* state of acknowledgments */ bool prackRsped = true; bool updRsped = true; bool acked = true; bool infoRsped = true; /* should be Diff, but infos limited to one */ /* state for limiting numbers of messages */ bool infoSent = false; do :: c2s!invite,offer; media = offering; goto inviting :: c2s!invite,none; goto inviting od; inviting: do :: s2c?invite,sdp; assert(false) :: s2c?update,sdp; assert(dialog && sdp == offer); if :: media == offering; c2s!updFail,none :: media == flow; c2s!updSucc,answer :: media == noFlow || media == offered; assert(false) fi :: s2c?info,none; assert(dialog); c2s!infoRsp,none :: s2c?bye,none; assert(false) :: s2c?unProv,none; dialog = true :: s2c?relProv,sdp; dialog = true; if :: (media == noFlow || media == flow) && sdp != none; assert(sdp == offer); c2s!prack,answer; prackRsped = false; media = flow :: media == offering && sdp != none; assert(prackRsped); if :: !updRsped; assert(sdp == offer); /* SIP problem 5 */ c2s!prack,answer; prackRsped = false; media = flow :: updRsped; assert(sdp == answer); if :: true; c2s!prack,offer; prackRsped = false; media = offering :: true; c2s!prack,none; prackRsped = false; media = flow fi fi :: media == offered && sdp != none; assert(false) :: sdp == none; c2s!prack,none; prackRsped = false fi :: s2c?prackRsp,sdp; assert(dialog && !prackRsped); prackRsped = true; if :: media == offering && sdp != none; assert(sdp == answer); media = flow :: media == offering && sdp == none; assert(true) :: media != offering; assert(sdp == none) fi; :: s2c?updSucc,sdp; assert(dialog && !updRsped && sdp == answer && media == offering); media = flow; updRsped = true :: s2c?updFail,none; assert(dialog && !updRsped); updRsped = true; if :: media == offering; media = flow :: else fi :: s2c?invFail,none; goto end :: s2c?invSucc,sdp; dialog = true; if :: media == noFlow; assert(sdp == offer); c2s!ack,answer; media = flow :: media == flow; assert(sdp == none); c2s!ack,none :: media == offering && sdp == none; c2s!ack,none :: media == offering && sdp != none; assert(sdp == answer); c2s!ack,none; media = flow :: media == offered; assert(false) fi; goto confirmed :: s2c?ack,sdp; assert(false) :: s2c?infoRsp,none; assert(dialog && !infoRsped); infoRsped = true :: s2c?byeRsp,none; assert(false) :: dialog && media == flow && updRsped; c2s!update,offer; media = offering; updRsped = false :: dialog; c2s!cancel,none; goto canceling :: dialog && !infoSent; c2s!info,none; infoSent = true; infoRsped = false od; confirmed: do :: s2c?invite,sdp; assert(!reInvited); if :: reInviting; c2s!invFail,none :: !reInviting; assert(media == flow); reInvited = true; if :: sdp != none; assert(sdp == offer); media = offered :: sdp == none; assert(true) fi fi :: s2c?update,sdp; assert(false) :: s2c?info,none; c2s!infoRsp,none :: s2c?bye,none; c2s!byeRsp,none; goto end :: s2c?unProv,none; assert(false) :: s2c?relProv,sdp; assert(false) :: s2c?prackRsp,sdp; assert(false) :: s2c?updSucc,sdp; assert(!reInviting && !reInvited && !updRsped && sdp == answer && media == offering); media = flow; updRsped = true; :: s2c?updFail,none; assert(false) :: s2c?invFail,none; assert(reInviting && !reInvited); reInviting = false; if :: media == offering; media = flow :: else fi :: s2c?invSucc,sdp; assert(reInviting && !reInvited && sdp != none); reInviting = false; if :: media == flow; assert(sdp == offer); c2s!ack,answer :: media == offering; assert(sdp == answer); c2s!ack,none; media = flow :: media == noFlow || media == offered; assert(false) fi :: s2c?ack,sdp; assert(!reInviting && !acked); acked = true; if :: sdp != none; assert(!reInvited && media == offering && sdp == answer); media = flow :: sdp == none; assert(true) fi; :: s2c?infoRsp,none; assert(dialog && !infoRsped); infoRsped = true :: s2c?byeRsp,none; assert(false) :: !infoSent; c2s!info,none; infoSent = true; infoRsped = false :: !reInviting && !reInvited && acked && updRsped; c2s!invite,offer; reInviting = true; media = offering :: !reInviting && !reInvited && acked && updRsped; c2s!invite,none; reInviting = true :: reInvited; reInvited = false; acked = false; if :: media == flow; c2s!invSucc,offer; media = offering :: media == offered; c2s!invSucc,answer; media = flow :: media == noFlow || media == offering; assert(false) fi :: c2s!bye,none; goto byeing od; canceling: do :: s2c?invite,sdp; assert(false) :: s2c?update,sdp; assert(true) :: s2c?info,none; assert(true) :: s2c?bye,none; assert(false) :: s2c?unProv,none; assert(true) :: s2c?relProv,sdp; assert(true) :: s2c?prackRsp,sdp; assert(!prackRsped); prackRsped = true :: s2c?updSucc,sdp; assert(!updRsped); updRsped = true :: s2c?updFail,sdp; assert(!updRsped); updRsped = true :: s2c?invFail,none; goto end :: s2c?invSucc,sdp; c2s!bye,none; goto byeing :: s2c?ack,sdp; assert(false) :: s2c?infoRsp,none; assert(!infoRsped); infoRsped = true :: s2c?byeRsp,none; assert(false) od; byeing: do :: s2c?invite,sdp; assert(true) :: s2c?update,sdp; assert(false) :: s2c?info,none; assert(true) :: s2c?bye,none; c2s!byeRsp,none :: s2c?unProv,none; assert(false) :: s2c?relProv,sdp; assert(false) :: s2c?prackRsp,sdp; assert(false) :: s2c?updSucc,sdp; assert(!updRsped); updRsped = true :: s2c?updFail,sdp; assert(false) :: s2c?invFail,none; assert(true) :: s2c?invSucc,sdp; assert(true) :: s2c?ack,sdp; assert(!acked); acked = true :: s2c?infoRsp,none; assert(!infoRsped); infoRsped = true :: s2c?byeRsp,none; goto end od; end: do :: s2c?invite,sdp; assert(false) :: s2c?update,sdp; assert(false) :: s2c?info,none; assert(false) :: s2c?bye,none; assert(false) :: s2c?unProv,none; assert(false) :: s2c?relProv,sdp; assert(false) :: s2c?prackRsp,sdp; assert(false) :: s2c?updSucc,sdp; assert(false) :: s2c?updFail,sdp; assert(false) :: s2c?invFail,none; assert(false) :: s2c?invSucc,sdp; assert(false) :: s2c?ack,sdp; assert(false) :: s2c?infoRsp,none; assert(false) :: s2c?byeRsp,none; assert(false) od } proctype UAS() { /* media state */ mtype media = noFlow; mtype sdp; /* state relevant to the invited phase */ bool dialog = false; bool relOut = false; /* relOut => dialog */ bool canSucc = true; /* !relOut => canSucc */ /* state relevant to the completed phase */ bool confirmed = false; /* state relevant to the confirmed phase (at most one is true) */ bool reInviting = false; bool reInvited = false; /* state of acknowledgments */ bool updRsped = true; bool acked = true; bool infoRsped = true; /* should be Diff, but infos limited to one */ /* state for limiting numbers of messages */ bool unProvSent = false; bool infoSent = false; c2s?invite,sdp; if :: sdp != none; assert(sdp == offer); media = offered :: sdp == none; assert(true) fi; invited: do :: c2s?invite,sdp; assert(false) :: c2s?prack,sdp; assert(dialog && relOut); relOut = false; canSucc = true; if :: media == flow && sdp != none; assert(sdp == offer); s2c!prackRsp,answer :: media == offering && sdp != none; assert(sdp == answer); s2c!prackRsp,none; media = flow :: (media == noFlow || media == offered) && sdp != none; assert(false) :: sdp == none; s2c!prackRsp,none fi; :: c2s?update,sdp; assert(dialog && sdp == offer); if :: media == offering && !canSucc; assert(updRsped); s2c!updFail,none /* SIP problem 5 */ :: media == offering && !updRsped; assert(canSucc); s2c!updFail,none :: media == flow; s2c!updSucc,answer :: media == noFlow || media == offered; assert(false) fi :: c2s?info,none; assert(dialog); s2c!infoRsp,none :: c2s?bye,none; assert(false) :: c2s?cancel,none; assert(dialog); s2c!invFail,none; goto end :: c2s?updSucc,sdp; assert(dialog && canSucc && !updRsped && sdp == answer && media == offering); media = flow; updRsped = true :: c2s?updFail,none; assert(dialog && canSucc && !updRsped && media == offering); media = flow; updRsped = true :: c2s?invFail,none; assert(false) :: c2s?invSucc,sdp; assert(false) :: c2s?ack,sdp; assert(false) :: c2s?infoRsp,none; assert(!infoRsped); infoRsped = true :: c2s?byeRsp,none; assert(false) :: !unProvSent; s2c!unProv,none; dialog = true; unProvSent = true :: !relOut; if :: media == noFlow; s2c!relProv,offer; media = offering; dialog = true; relOut = true; canSucc = false :: media == offered; s2c!relProv,answer; media = flow; dialog = true; relOut = true; canSucc = false :: media == flow; s2c!relProv,offer; media = offering; dialog = true; relOut = true; canSucc = false :: (media==flow || media==offered || media==offering); s2c!relProv,none; dialog = true; relOut = true fi :: dialog && media == flow && canSucc; s2c!update,offer; media = offering; updRsped = false :: s2c!invFail,none; goto end :: canSucc && media == noFlow; s2c!invSucc,offer; media = offering; acked = false; goto completed :: canSucc && media == offered; s2c!invSucc,answer; media = flow; acked = false; goto completed :: canSucc && media == flow; s2c!invSucc,none; acked = false; goto completed :: dialog && !infoSent; s2c!info,none; infoSent = true; infoRsped = false od; completed: do :: c2s?invite,sdp; assert(!reInvited); if :: reInviting; s2c!invFail,none :: !reInviting; assert(media == flow); reInvited = true; if :: sdp != none; assert(sdp == offer); media = offered :: sdp == none; assert(true) fi fi :: c2s?prack,sdp; assert(sdp == none) :: c2s?update,sdp; assert(!reInviting && !reInvited && sdp == offer && media == flow); s2c!updSucc,answer :: c2s?info,none; s2c!infoRsp,none :: c2s?bye,none; s2c!byeRsp,none; goto end :: c2s?cancel,none; assert(true) :: c2s?updSucc,sdp; assert(false) :: c2s?updFail,none; assert(false) :: c2s?invFail,none; assert(reInviting && !reInvited); reInviting = false; if :: media == offering; media = flow :: else fi; :: c2s?invSucc,sdp; assert(reInviting && !reInvited); reInviting = false; if :: media == flow; assert(sdp == offer); s2c!ack,answer :: media == offering; assert(sdp == answer); s2c!ack,none; media = flow :: media == noFlow || media == offered; assert(false) fi :: c2s?ack,sdp; assert(!reInviting && !acked); acked = true; if :: !confirmed; confirmed = true :: else fi; if :: media == offering && sdp != none; assert(sdp == answer && !reInvited); media = flow :: media == offering && sdp == none; assert(true) :: media == flow || media == offered; assert(sdp == none); :: media == noFlow; assert(false) fi; :: c2s?infoRsp,none; assert(!infoRsped); infoRsped = true :: c2s?byeRsp,none; assert(false) :: !infoSent; s2c!info,none; infoSent = true; infoRsped = false :: !reInviting && !reInvited && acked; assert(confirmed && media == flow); s2c!invite,offer; reInviting = true; media = offering :: !reInviting && !reInvited && acked; assert(confirmed && media == flow); s2c!invite,none; reInviting = true :: reInvited; assert(!reInviting); reInvited = false; acked = false; if :: media == flow; s2c!invSucc,offer; media = offering :: media == offered; s2c!invSucc,answer; media = flow :: media == noFlow || media == offering; assert(false) fi :: confirmed; s2c!bye,none; goto byeing /* SIP note 1 */ od; byeing: do :: c2s?invite,sdp; assert(true) :: c2s?prack,sdp; assert(false) :: c2s?update,sdp; assert(false) :: c2s?info,none; assert(true) :: c2s?bye,none; s2c!byeRsp,none :: c2s?cancel,none; assert(false) :: c2s?updSucc,sdp; assert(false) :: c2s?updFail,sdp; assert(false) :: c2s?invFail,none; assert(true) :: c2s?invSucc,sdp; assert(true) :: c2s?ack,sdp; assert(!acked); acked = true :: c2s?infoRsp,none; assert(!infoRsped); infoRsped = true :: c2s?byeRsp,none; goto end od; end: do :: c2s?invite,sdp; assert(false) :: c2s?prack,sdp; assert(true) :: c2s?update,sdp; assert(true) :: c2s?info,none; assert(true) :: c2s?bye,none; assert(false) :: c2s?cancel,none; assert(true) :: c2s?updSucc,sdp; assert(!updRsped); updRsped = true :: c2s?updFail,sdp; assert(!updRsped); updRsped = true :: c2s?invFail,none; assert(false) :: c2s?invSucc,sdp; assert(false) :: c2s?ack,sdp; assert(false) :: c2s?infoRsp,none; assert(!infoRsped); infoRsped = true :: c2s?byeRsp,none; assert(false) od } init { atomic { run UAC(); run UAS() } }