Model-based Verification of the SIP Invite Scenario

被引：0

作者：

Matetic, Sinisa ^{[1
]}

Babac, Marina Bagic ^{[1
]}

机构：

[1] Fac Elect Engn & Comp, Zagreb, Croatia

来源：

2013 36TH INTERNATIONAL CONVENTION ON INFORMATION AND COMMUNICATION TECHNOLOGY, ELECTRONICS AND MICROELECTRONICS (MIPRO) | 2013年

关键词：

COLORED PETRI NETS; PROTOCOL;

D O I：

暂无

中图分类号：

TP [自动化技术、计算机技术];

学科分类号：

0812 ;

摘要：

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.

引用

页码：841 / 846

页数：6

共 13 条

[1] Ding LG, 2008, LECT NOTES COMPUT SC, V5062, P132, DOI 10.1007/978-3-540-68746-7_12
[2] Gehlot V., 2006, P 7 WORKSHOP PRACTIC, P197
[3] JENSEN K, 1998, LECT NOTES COMPUTER, V1492, P237, DOI DOI 10.1007/3-540-65307-4_50
[4] Jensen K., 1997, MONOGRAPHS THEORETIC, V3
[5] Jensen K, 2009, COLOURED PETRI NETS: MODELLING AND VALIDATION OF CONCURRENT SYSTEMS, P1, DOI 10.1007/b95112
[6] The practitioner's guide to coloured Petri nets
Kristensen L.M.
Christensen S.
Jensen K.
[J]. International Journal on Software Tools for Technology Transfer, 1998, 2 (2) : 98 - 132
[7] Kristensen LM, 2004, LECT NOTES COMPUT SC, V3147, P248
[8] Application of coloured Petri nets in system development
Kristensen, LM
Jorgensen, JB
Jensen, K
[J]. LECTURES ON CONCURRENCY AND PETRI NETS: ADVANCES IN PETRI NETS, 2004, 3098 : 626 - 685
[9] ROSENBERG J, 2002, 3261 RFC IETF
[10] Willcock C., 2005, An Introduction to TTCN-3

← 1 2 →