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

fYear

2011

Firstpage

1

Lastpage

5

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;

fLanguage

English

Publisher

ieee

Conference_Titel

Wireless Communications, Networking and Mobile Computing (WiCOM), 2011 7th International Conference on

Conference_Location

Wuhan

ISSN

2161-9646

Print_ISBN

978-1-4244-6250-6

Type

conf

DOI

10.1109/wicom.2011.6040445

Filename

6040445