Title :
Formal Modeling and Analysis of SIP Using Colored Petri Nets
Author :
Bai, Yunli ; Ye, Xinming ; Ma, Yuanfei
Author_Institution :
Coll. of Comput. Sci., Inner Mongolia Univ., Hohhot, China
Abstract :
The Session Initiation Protocol (SIP), which is wildly used for IP-based multimedia communication, is an application-layer protocol to handle sessions between two points. SIP is implemented on the top of user datagram protocol (UDP) or transmission control protocol (TCP). This study proposed a Colored Petri Nets (CPN) based formal model of the INVITE transaction of SIP over reliable and unreliable transport channel. Then, simulation and state space analysis are utilized to validate the model and verify some higher functional properties of SIP. The proposed formal model could not only be served as an unambiguous and visual formal specification of SIP, but also facilitate protocol behavior simulation and properties analysis.
Keywords :
IP networks; Petri nets; formal specification; multimedia communication; signalling protocols; state-space methods; transport protocols; INVITE transaction; IP-based multimedia communication; TCP; application-layer protocol; colored Petri nets; formal modeling; protocol behavior simulation; protocol properties analysis; session initiation protocol; state space analysis; transmission control protocol; transport channel; unambiguous formal specification; user datagram protocol; visual formal specification; Analytical models; Data models; Petri nets; Protocols; Reactive power; Reliability; Servers;
Conference_Titel :
Wireless Communications, Networking and Mobile Computing (WiCOM), 2011 7th International Conference on
Conference_Location :
Wuhan
Print_ISBN :
978-1-4244-6250-6
DOI :
10.1109/wicom.2011.6040445
