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.
[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.
[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.
@article{"International Journal of Information, Control and Computer Sciences:50056", author = "Sabina Baraković and Dragan Jevtić and Jasmina Baraković Husić", title = "Modeling of Session Initiation Protocol Invite Transaction using Colored Petri Nets", abstract = "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.", keywords = "Colored Petri Nets, SIP INVITE, state space, dead
marking", volume = "6", number = "1", pages = "6-8", }