The Session Initiation Protocol (SIP) is an application layer signaling protocol used to create, manage, and terminate sessions in an\nIP based network. SIP is considered as a transactional protocol. There are two main SIP transactions, the INVITE transaction and\nthe non-INVITE transaction.The SIP INVITE transaction specification is described in an informal way in Request for Comments\n(RFC) 3261 and modified in RFC 6026. In this paper we focus on the INVITE transaction of SIP, over reliable and unreliable\ntransportmediums, which is used to initiate a session. In order to ensure the correctness of SIP, the INVITE transaction is modeled\nand verified using event-B method and its Rodin platform. The Event-B refinement concept allows an incremental development\nby defining the studied system at different levels of abstraction, and Rodin discharges almost all proof obligations at each level.\nThis interaction between modeling and proving reduces the complexity and helps in assuring that the INVITE transaction SIP\nspecification is correct, unambiguous, and easy to understand.
Loading....