Model-based verification of the SIP invite scenario

Author

Matetic, Sinisa ; Babac, Marina Bagic

Author_Institution

Fac. of Electr. Eng. & Comput., Univ. of Zagreb, Zagreb, Croatia

fYear

2013

fDate

20-24 May 2013

Firstpage

841

Lastpage

846

Abstract

The Session Initiation Protocol (SIP) is a signaling protocol for multimedia control over the Internet. It is used for initiating, maintaining and terminating multimedia sessions. In this paper we have carried out the verification of the SIP Invite scenario with Coloured Petri nets (CP-nets or CPNs). First, we have specified and verified the protocol model using a simulation tool. Then, we have verified the scenario using a state space analysis tool. We have concluded that the SIP Invite transaction is free of livelocks, and has only desirable deadlocks. Therefore, no additional remodeling for the protocol Invite transaction is needed.

Keywords

Internet; Petri nets; multimedia communication; signalling protocols; Internet; SIP invite scenario; coloured Petri nets; model based verification; multimedia control; multimedia sessions; protocol invite transaction; protocol model; session initiation protocol; signaling protocol; simulation tool; state space analysis tool; Analytical models; Payloads; Protocols; Radiation detectors; Receivers; Reliability; Servers;

fLanguage

English

Publisher

ieee

Conference_Titel

Information & Communication Technology Electronics & Microelectronics (MIPRO), 2013 36th International Convention on

Conference_Location

Opatija

Print_ISBN

978-953-233-076-2

Type

conf

Filename

6596374