Verification of Session Initiation Protocol Using Timed Colored Petri Net

Safiye Kızmaz, Mürvet Kırcı
DOI: 10.4236/ijcns.2011.43021                

Abstract

In this work, Session Initiation Protocol model is established by using Timed Colored Petri Nets (TCPN). SIP (Session Initiation Protocol) is a protocol developed to assist in providing advanced telephony services across the Internet. The Session Initiation Protocol (SIP) has become the quasi-standard for Voiceover-Internet Protocol (VoIP) communications. SIP is based on a client–server infrastructure in which user agents represent the end-terminals as clients, proxy servers handle SIP message routing between the user agents, and registrar servers store the client’s contact information into a location service. By use of timed color set and useful time attributes in tokens defined in CPN tools, timer and time-related problems of SIP are modeled and analyzed. Timer is an important part for SIP, especially the INVITE transaction.

Keywords

Session Initiation Protocol, Timed Colored Petri Nets, Protocol Verification, CPN Tool

Conflicts of Interest

The authors declare no conflicts of interest.

References

[1]	J. Rosenberg, et al., “RFC 3261: SIP: Session Initiation Protocol,” Internet Engineering Task Force, 2002. http://www.faqs.org/rfcs/rfc3261.html
[2]	R. Arora, “Voice over IP: Protocols and Standards,” Student Reports, CSE of Ohio-State University, Columbus, November 1999.
[3]	R. Sparks, “SIP: Basics and Beyond,” Queue, Vol. 5, No. 2, 2007, pp. 22-33. doi:10.1145/1229899.1229909
[4]	G. J. Holzmann, “Design and Validation of Computer Protocols,” Prentice Hall, Englewood Cliffs, 1991.
[5]	D. Sidhu, A. Chung and T. P. Blumer, “Experience with Formal Methods in Protocol Development,” ACM SIGCOMM Computer Communication Review, Vol. 21, No. 2, 1991, pp. 81-101. doi:10.1145/122419.122425
[6]	J. Wang, “Timed Petri Nets Theory: An Application,” Kluwer Academic Publishers, Norwell, 1998.
[7]	L. G. Ding and L. Liu, “Modelling and Analysis of the INVITE Transaction of the Session Initiation Protocol Using Coloured Petri Nets,” Proceedings of the 29th International Conference on Applications and Theory of Petri Nets and Other Models of Concurrency, Xi’an, Vol. 5062, 23-27 June 2008, pp. 132-151.
[8]	L. Liu, “Verification of SIP Transaction Using Coloured Petri Nets,” In: B. Mans, Ed., Proceedings of 32nd Australasian Computer Science Conference, Wellington, 19-23 January 2009, pp. 63-72.
[9]	V. Gehlot and A. Hayrapetyan, “A CPN Model of a SIP-Based Dynamic Discovery Protocol for Webservices in a Mobile Environment,” Proceedings 7th Workshop and Tutorial on Practical Use of Coloured Petri Nets and the CPN Tools, Aarhus, 24-26 October 2006, pp. 1-20.
[10]	G. J. Holzmann, “Design and Validation of Computer Protocols,” Prentice Hall, Englewood Cliffs, 1991.
[11]	Y. Peng, Z. Yuan and J. Wang, “Petri Net Model of Session Initiation Protocol and Its Verification,” Proceedings of the IEEE International Conference on Wireless Communications, Networking and Mobile Computing, Shanghai, 21-25 September 2007, pp. 1861-1864.
[12]	H. Wan, G. Su and H. Ma, “SIP for Mobile Networks and Security Model,” Proceedings of the IEEE International Conference on Wireless Communications, Networking and Mobile Computing, Shanghai, 21-25 September 2007, pp. 1809-1812.
[13]	S. Ahson and M. Ilyas, “SIP Handbook: Services, Technologies, and Security of Session Initiation Protocol,” CRC Press, Boca Raton, 2009.
[14]	K. Jensen, “Coloured Petri Nets,” Vol. 2, Springer, New York, 1995.
[15]	M. Bago, N. Peric and S. Marijan, “Modeling Wire Train Bus Communication Using Timed Colored Petri Nets,” Proceedings of SICE Annual Conference, Tokyo, 20-22 August 2008, pp. 2905-2910. doi:10.1109/SICE.2008.4655160
[16]	Y.-S. Huang, T.-H. Chung and J.-H. Lin, “A Timed Coloured Petri Net Supervisor for Urban Traffic Networks,” IMACS Multiconference on Computational Engineering in Systems Applications, Beijing, Vol. 2, 4-6 October 2006, pp. 2151-2156.
[17]	Homepage of the CPN Tools, 2009. http://wiki.daimi.au.dk/cpntools/cpntools.wiki
[18]	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, 2007, pp. 213-254. doi:10.1007/s10009-007-0038-x
[19]	R. Sparks, “draft-sparks-sip-invfix-00: Correct Transaction Handling for 200 Responses to Session Initiation Protocol INVITE Requests,” Internet Engineering Task Force, 2007. http://tools.ietf.org/id/draft-sparks-sip-invfix-00.txt