A Mechanically Proved and an Incremental Development of the Session Initiation Protocol INVITE Transaction
The Session Initiation Protocol (SIP) is an application layer signaling protocol used to create, manage, and terminate sessions in an IP based network. SIP is considered as a transactional protocol. There are two main SIP transactions, the INVITE transaction and the non-INVITE transaction. The SIP I...
Saved in:
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Wiley
2014-01-01
|
| Series: | Journal of Computer Networks and Communications |
| Online Access: | http://dx.doi.org/10.1155/2014/352071 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1832555905637416960 |
|---|---|
| author | Rajaa Filali Mohamed Bouhdadi |
| author_facet | Rajaa Filali Mohamed Bouhdadi |
| author_sort | Rajaa Filali |
| collection | DOAJ |
| description | The Session Initiation Protocol (SIP) is an application layer signaling protocol used to create, manage, and terminate sessions in an IP based network. SIP is considered as a transactional protocol. There are two main SIP transactions, the INVITE transaction and the non-INVITE transaction. The SIP INVITE transaction specification is described in an informal way in Request for Comments (RFC) 3261 and modified in RFC 6026. In this paper we focus on the INVITE transaction of SIP, over reliable and unreliable transport mediums, which is used to initiate a session. In order to ensure the correctness of SIP, the INVITE transaction is modeled and verified using event-B method and its Rodin platform. The Event-B refinement concept allows an incremental development by defining the studied system at different levels of abstraction, and Rodin discharges almost all proof obligations at each level. This interaction between modeling and proving reduces the complexity and helps in assuring that the INVITE transaction SIP specification is correct, unambiguous, and easy to understand. |
| format | Article |
| id | doaj-art-13ec27083d6a4015a889d56fc75b77d2 |
| institution | Kabale University |
| issn | 2090-7141 2090-715X |
| language | English |
| publishDate | 2014-01-01 |
| publisher | Wiley |
| record_format | Article |
| series | Journal of Computer Networks and Communications |
| spelling | doaj-art-13ec27083d6a4015a889d56fc75b77d22025-02-03T05:46:46ZengWileyJournal of Computer Networks and Communications2090-71412090-715X2014-01-01201410.1155/2014/352071352071A Mechanically Proved and an Incremental Development of the Session Initiation Protocol INVITE TransactionRajaa Filali0Mohamed Bouhdadi1LMPHE laboratory, Faculty of sciences, University of Mohammed V, 4 Street Ibn Batouta, PB 1014 RP Rabat, MoroccoLMPHE laboratory, Faculty of sciences, University of Mohammed V, 4 Street Ibn Batouta, PB 1014 RP Rabat, MoroccoThe Session Initiation Protocol (SIP) is an application layer signaling protocol used to create, manage, and terminate sessions in an IP based network. SIP is considered as a transactional protocol. There are two main SIP transactions, the INVITE transaction and the non-INVITE transaction. The SIP INVITE transaction specification is described in an informal way in Request for Comments (RFC) 3261 and modified in RFC 6026. In this paper we focus on the INVITE transaction of SIP, over reliable and unreliable transport mediums, which is used to initiate a session. In order to ensure the correctness of SIP, the INVITE transaction is modeled and verified using event-B method and its Rodin platform. The Event-B refinement concept allows an incremental development by defining the studied system at different levels of abstraction, and Rodin discharges almost all proof obligations at each level. This interaction between modeling and proving reduces the complexity and helps in assuring that the INVITE transaction SIP specification is correct, unambiguous, and easy to understand.http://dx.doi.org/10.1155/2014/352071 |
| spellingShingle | Rajaa Filali Mohamed Bouhdadi A Mechanically Proved and an Incremental Development of the Session Initiation Protocol INVITE Transaction Journal of Computer Networks and Communications |
| title | A Mechanically Proved and an Incremental Development of the Session Initiation Protocol INVITE Transaction |
| title_full | A Mechanically Proved and an Incremental Development of the Session Initiation Protocol INVITE Transaction |
| title_fullStr | A Mechanically Proved and an Incremental Development of the Session Initiation Protocol INVITE Transaction |
| title_full_unstemmed | A Mechanically Proved and an Incremental Development of the Session Initiation Protocol INVITE Transaction |
| title_short | A Mechanically Proved and an Incremental Development of the Session Initiation Protocol INVITE Transaction |
| title_sort | mechanically proved and an incremental development of the session initiation protocol invite transaction |
| url | http://dx.doi.org/10.1155/2014/352071 |
| work_keys_str_mv | AT rajaafilali amechanicallyprovedandanincrementaldevelopmentofthesessioninitiationprotocolinvitetransaction AT mohamedbouhdadi amechanicallyprovedandanincrementaldevelopmentofthesessioninitiationprotocolinvitetransaction AT rajaafilali mechanicallyprovedandanincrementaldevelopmentofthesessioninitiationprotocolinvitetransaction AT mohamedbouhdadi mechanicallyprovedandanincrementaldevelopmentofthesessioninitiationprotocolinvitetransaction |