Modeling of Session Initiation Protocol Invite Transaction using Colored Petri Nets

Wireless mobile communications have experienced the phenomenal growth through last decades. The advances in wireless mobile technologies have brought about a demand for high quality multimedia applications and services. For such applications and services to work, signaling protocol is required for establishing, maintaining and tearing down multimedia sessions. The Session Initiation Protocol (SIP) is an application layer signaling protocols, based on request/response transaction model. This paper considers SIP INVITE transaction over an unreliable medium, since it has been recently modified in Request for Comments (RFC) 6026. In order to help in assuring that the functional correctness of this modification is achieved, the SIP INVITE transaction is modeled and analyzed using Colored Petri Nets (CPNs). Based on the model analysis, it is concluded that the SIP INVITE transaction is free of livelocks and dead codes, and in the same time it has both desirable and undesirable deadlocks. Therefore, SIP INVITE transaction should be subjected for additional updates in order to eliminate undesirable deadlocks. In order to reduce the cost of implementation and maintenance of SIP, additional remodeling of the SIP INVITE transaction is recommended.




References:
[1] M. Grayson, K. Shatzkamer, and K. Wierenga, Building the Mobile
Internet. Cisco Press, 2011.
[2] J. Rosenberg, et al., "SIP: Session Initiation Protocol," Technical Report
RFC 3261, Internet Engineering Task Force (IETF), June 2002.
[3] R. Sparks and T. Zourzouvillys, "Correct Transaction Handling for 2xx
Responses to Session Initiation Protocol INVITE Request," Technical
Report RFC 6026, Internet Engineering Task Force (IETF), Sep. 2010.
[4] Home Page of the CPN Tools, http://cpntools.org/. Accessed on Sep
20th, 2011.
[5] L. G. Ding and L. Liu, "Modelling and Analysis of the INVITE
Transaction of the Session Initiation Protocol Using Coloured Petri
Nets," Lecture Notes in Computer Science, Springer, 2008, pp. 132-151.
[6] L. Liu, "Verification of the SIP Transaction Using Coloured Petri Nets,"
in Proc. of the 32nd Australasian Computer Science Conference,
Wellington, New Zealand, Jan. 2009.
[7] S. K─▒zmaz and M. K─▒rc─▒, "Verification of Session Initiation Protocol
Using Timed Colored Petri Net," International Journal of
Communication, Network and System Sciences, vol. 4, pp. 170-179,
Mar. 2011.
[8] Y. Ding, G. Su, and H. Wan, "SIP Modeling and Simulation," SIP
Handbook: Services, Technologies, and Security of Session Initiation
Protocol, CRC Press, Taylor & Francis Group, USA, 2009, pp. 373-396.
[9] J. I. Agbinya, IP Communications and Services for NGN. Aurebach
Publications, CRC Press, Taylor & Francis Group, USA, 2010.
[10] V. Gehlot and C. Nigro, "An Introduction to Systems Modeling and
Simulation with Colored Petri Nets," in Proc. of Winter Simulation
Conference, Baltimore, Maryland, USA, Dec. 2010, pp. 104-118.
[11] Y. Xu and X. Xie, "Modeling and Analysis of Security Protocols Using
Colored Petri Nets," Journal of Computers, vol. 6, no. 1, pp. 19-27, Jan.
2011.
[12] K. Jensen, L. Kristensen, and L. Wells, "Coloured Petri Nets and CPN
Tools for Modelling and Validation of Concurrent Systems,"
International Journal on Software Tools for Technology Transfer, vol. 9,
no. 3, pp. 213-254, 2007.