Verification of Session Initiation Protocol Using Timed Colored Petri Net
- 1
- 2
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.
- J. Rosenberg, et al., “RFC 3261: SIP: Session Initiation Protocol,” Internet Engineering Task Force, 2002. http://www.faqs.org/rfcs/rfc3261.html
- R. Arora, “Voice over IP: Protocols and Standards,” Student Reports, CSE of Ohio-State University, Columbus, November 1999.
- R. Sparks, “SIP: Basics and Beyond,” Queue, Vol. 5, No. 2, 2007, pp. 22-33. doi:10.1145/1229899.1229909
- G. J. Holzmann, “Design and Validation of Computer Protocols,” Prentice Hall, Englewood Cliffs, 1991.
- 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
- J. Wang, “Timed Petri Nets Theory: An Application,” Kluwer Academic Publishers, Norwell, 1998.
- 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.
- 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.
- 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.
- G. J. Holzmann, “Design and Validation of Computer Protocols,” Prentice Hall, Englewood Cliffs, 1991.
- 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.
- 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.
- S. Ahson and M. Ilyas, “SIP Handbook: Services, Technologies, and Security of Session Initiation Protocol,” CRC Press, Boca Raton, 2009.
- K. Jensen, “Coloured Petri Nets,” Vol. 2, Springer, New York, 1995.