Modelling and Analysis of the INVITE Transaction of the Session Initiation Protocol Using Coloured Petri Nets

  • Lay G. Ding
  • Lin Liu
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5062)


The Session Initiation Protocol (SIP) is a control protocol developed by the Internet Engineering Task Force for initiating, modifying and terminating multimedia sessions over the Internet. SIP uses an INVITE transaction to initiate a session. In this paper, we create a Coloured Petri Net (CPN) model for the INVITE transaction. Then we verify the general properties of the INVITE transaction by analysing the state space of the CPN model. The analysis results show that in most cases the INVITE transaction behaves as expected. However, in some circumstances, the transaction may terminate in an undesirable state while one communication party is still waiting for a response from its peer. Hence, we propose a set of changes to the INVITE transaction to correct the above problem. The result has shown that this revised INVITE transaction satisfies the properties that we have specified, and the undesirable terminal state has been eliminated.


Session Initiation Protocol Coloured Petri Nets protocol verification 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Rosenberg, J., et al.: RFC 3261: SIP: Session Initiation Protocol. Internet Engineering Task Force (2002),
  2. 2.
    Sparks, R.: SIP: basics and beyond. Queue 5(2), 22–33 (2007)CrossRefGoogle Scholar
  3. 3.
    Holzmann, G.J.: Design and validation of computer protocols. Prentice Hall, Englewood Cliffs, New Jersey (1991)Google Scholar
  4. 4.
    Sidhu, D., Chung, A., Blumer, T.P.: Experience with formal methods in protocol development. In: ACM SIGCOMM Computer Communication Review, vol. 21(2), pp. 81–101. ACM, New York (1991)Google Scholar
  5. 5.
    Examples of Industrial Use of CP-nets,
  6. 6.
    Billington, J., Gallasch, G.E., Han, B.: Lectures on Concurrency and Petri Nets: A Coloured Petri Net Approach to Protocol Verification. In: Desel, J., Reisig, W., Rozenberg, G. (eds.) ACPN 2003. LNCS, vol. 3098, pp. 210–290. Springer, Heidelberg (2004)Google Scholar
  7. 7.
    Kristensen, L.M., Jørgensen, J.B., Jensen, K.: Application of Coloured Petri Nets in System Development. In: Desel, J., Reisig, W., Rozenberg, G. (eds.) ACPN 2003. LNCS, vol. 3098, pp. 626–685. Springer, Heidelberg (2004)Google Scholar
  8. 8.
    Turner, K.J.: Modelling SIP Services Using CRESS. In: Peled, D.A., Vardi, M.Y. (eds.) FORTE 2002. LNCS, vol. 2529, pp. 162–177. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  9. 9.
    Gehlot, V., Hayrapetyan, A.: A CPN Model of a SIP-Based Dynamic Discovery Protocol for Webservices in a Mobile Environment. In: the 7th Workshop and Tutorial on Practical Use of CPNs and the CPN Tools, University of Aarhus, Denmark (2006)Google Scholar
  10. 10.
    Wan, H., Su, G., Ma, H.: SIP for Mobile Networks and Security Model. In: Wireless Communications, Networking and Mobile Computing, pp. 1809–1812. IEEE, Los Alamitos (2007)CrossRefGoogle Scholar
  11. 11.
    Jensen, K., Kristensen, L., Wells, L.: Coloured Petri Nets and CPN Tools for modelling and validation of concurrent systems. Int. J. on Software Tools for Technology Transfer (STTT) 9(3), 213–254 (2007)CrossRefGoogle Scholar
  12. 12.
  13. 13.
    Rosenberg, J.: Bug 706 - Clarify lack of a timer for exiting proceeding state, Bugzilla (2003),
  14. 14.
    Sparks, R.: draft-sparks-sip-invfix-00: Correct transaction handling for 200 responses to Session Initiation Protocol INVITE requests. Internet Engineering Task Force (2007),

Copyright information

© Springer-Verlag Berlin Heidelberg 2008

Authors and Affiliations

  • Lay G. Ding
    • 1
  • Lin Liu
    • 1
  1. 1.School of Computer and Information ScienceUniversity of South AustraliaAustralia

Personalised recommendations