Formal Verification And Analysis Of SIP Protocol Using Timed Coloured Petri Net

Session Initiation Protocol(SIP), with its seamless, flexible and scalable features,meet the needs of technical development. It has been play an important role in many ways, while it’s working field continue to expand with the development of Next Generation Network(NGN). In order to conform with the needs of a variety of network environments,the extension,modify and further refinement of SIP must be adopted.However, the complex protocol development increase the difficulty of any adjust in its errors and defects. How to find the shortage of protocol in earlier stage, therefore decrease the costs of application development and maintenance is a subject worthy of studyModeling and analyzing the specification using formal methods can help achieve this goal. It is help to assure that the contents of RFC3261(SIP) are correct unambiguous,and easy to understand. Moreover. From the perspective of protocol engineering, verification is also an important step of the life-cycle of protocol development, a well-defined and verified specification will reduce the cost for implementation and maintenance. Timed Colored Petri Nets(TCPN) make the model more accurate and easy to conduct in-depth analysis as the formal modeling and analyzing technique, because tokens in timed CPN carry time stamp which model protocol time restrictions. Currently, area of SIP research is rarely concentrated on the formal verification and model analysis, Not to mention analyzing it using TCPN.In this thesis, first of all,we proposed a hierarchy modeling method using TCPN, guiding the modeling of SIP. the generating model accurately describe the main functional behavior of protocol. Besides, we verify the time constraints of SIP, Ensuring accurate portrait of the model on the details of the RFC’S time constraints.Further more, analysis is given in the different abstract levels using integration method which combine formulation,state space analysis and model checking, it verify that model satisfy the SIP requirement. Finally, making data mining in the model using regular expression, the result indicate that SIP has deadlock under certain conditions, and then we make recommendations to avoid such situation and suggestions to improve the SIP.