Title :
Petri Net Model of Session Initiation Protocol and its Verification
Author :
Yang Peng ; Yuan Zhanting ; Wang Jizeng
Author_Institution :
Coll. of Electr. & Inf. Eng., Lanzhou Univ. of Tech., Lanzhou
Abstract :
On the basis of the process of session initiation protocol´s service, Petri net model of SIP was established. In terms of properties of Petri net and the analysis of reachability tree, the protocol was proved to be boundedness, deadlock free and liveness. Moreover, considering the protocol´s repetitiveness and conservativeness, the analysis of reachability and invariant was given to verify the correctness of the protocol, which lessened the risk in the design of protocol as well as was of great value to solve the problem of SIP´s application.
Keywords :
Petri nets; reachability analysis; signalling protocols; trees (mathematics); Petri net model; SIP; protocol conservativeness; protocol design; protocol repetitiveness; reachability tree; session initiation protocol; Educational institutions; Network servers; Next generation networking; Payloads; Performance analysis; Risk analysis; Signal analysis; Stability; System recovery; Transport protocols;
Conference_Titel :
Wireless Communications, Networking and Mobile Computing, 2007. WiCom 2007. International Conference on
Conference_Location :
Shanghai
Print_ISBN :
978-1-4244-1311-9
DOI :
10.1109/WICOM.2007.466
